zraffer

module MySum

record ADepType : Type where
  MkADepType : 
    (dtBase : Type) -> 
    (dtFiber : dtBase -> Type) ->
    ADepType

record ADepSum : ADepType -> Type where
  MkADepSum : 

zraffer

Monoid_Unit : Type -> Type
Monoid_Unit carrier = carrier

data TypeUnit : (Monoid_Unit Type) where
  MkTypeUnit : TypeUnit

zraffer

infixr 1 ~>

Relation_Arrow : Type -> Type
Relation_Arrow ob = (source, target: ob) -> Type

class RelationClass (ob: Type) where
  (~>) : Relation_Arrow ob

record RelationRecord : Type where
  MkRelation : (recOb: Type) -> (recInst: RelationClass recOb) -> RelationRecord

zraffer

mutual
  data T1 : Type where
    Mk1 : T1
    Mk2 : T2 Mk1 -> T1
  data T2 : T1 -> Type where
    Mk0 : T2 Mk1

zraffer

module Auto where
mutual
  data T1 : Set where
    Mk1 : T1
    Mk2 : T2 Mk1 -> T1
  data T2 : T1 -> Set where
    Mk0 : T2 Mk1

zraffer

module iterY

total
iter : Nat->(x->x)->(x->x)
iter Z f = id
iter (S n) f = f . (iter n f)

partial
inf : Nat
inf = S inf

zraffer

module noInfinity

%default total

data T2 = Mk1 | Mk2

Mk1neqMk2 : Not (Mk1 = Mk2)
Mk1neqMk2 Refl impossible

Mk2neqMk1 : Not (Mk2 = Mk1)

zraffer

λ(sh : ∀(Shadow : *) → ∀(ShadowOk : Shadow → *) → ∀(ShadowEqu : Shadow → Shadow → *) → ∀(ShadowRefl : ∀(s : Shadow) → ShadowEqu s s) → ∀(ShadowTrans : ∀(s1 : Shadow) → ∀(s2 : Shadow) → ∀(s3 : Shadow) → ShadowEqu s1 s2 → ShadowEqu s2 s3 → ShadowEqu s1 s3) → ∀(ShadowSym : ∀(s1 : Shadow) → ∀(s2 : Shadow) → ShadowEqu s1 s2 → ShadowEqu s2 s1) → ∀(Mk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → Shadow) → ∀(MkOk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → ShadowOk (Mk A AOk AEqu ARefl ATrans ASym)) → ∀(MkIsoEqu : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1

zraffer

-- #AND: #Prop -> #Prop -> #Prop
\(A: #Prop )-> \(B: #Prop )-> 
\/(AND: #Prop )->
\/(Intro: A -> B -> AND)->
AND

zraffer

~/github/groupoid/om $ mad dep com plan sh |& tee log
==> dependency: "git://github.com/synrc/active" tag: {tag,"1.9"}
==> dependency: "git://github.com/synrc/mad" tag: {tag,"1.9"}
==> dependency: "git://github.com/synrc/sh" tag: {tag,"1.9"}
==> dependency: "git://github.com/synrc/fs" tag: {tag,"1.9"}
==> "active"
==> "mad"
==> "sh"
==> "fs"
==> "/home/user/github/groupoid/om"