allprim.txt

Id   : (A : U) (a b : A) -> U

refl : (A : U) (a : A) -> Id A a a

funExt : (A : U) (B : (a : A) -> U) (f g : (a : A) -> B a)
         (p : ((x : A) -> (Id (B x) (f x) (g x)))) -> Id ((y : A) -> B y) f g

fiber : (A B : U) (f : A -> B) (y : B) -> U
fiber A B f y = (x : A) * Id B (f x) y

id : (A : U) -> A -> A
id A a = a

pathTo : (A:U) -> A -> U
pathTo A = fiber A A (id A)

singl : (A:U) -> A -> U
singl A a = Sigma A (Id A a)

contrSingl :  (A : U) (a b:A) (p:Id A a b) -> Id (singl A a) (a, refl A a) (b, p)

equivEq : (A B : U) (f : A -> B) (s : (y : B) -> fiber A B f y)
            (t : (y : B) -> (v : fiber A B f y) -> Id (fiber A B f y) (s y) v) ->
            Id U A B

transport : (A B : U) -> Id U A B -> A -> B

transpInv : (A B : U) -> Id U A B -> B -> A

transportRef : (A : U) (a : A) -> Id A a (transport A A (refl U A) a)

equivEqRef : (A : U) -> (s : (y : A) -> pathTo A y) -> 
             (t : (y : A) -> (v : pathTo A y) -> Id (pathTo A y) (s y) v) ->
             Id (Id U A A) (refl U A) (equivEq A A (id A) s t)

transpEquivEq : (A B : U) -> (f : A -> B) (s : (y : B) -> fiber A B f y) -> 
                (t : (y : B) -> (v : fiber A B f y) -> Id (fiber A B f y) (s y) v) ->
                (a : A) -> Id B (f a) (transport A B (equivEq A B f s t) a)

mapOnPath : (A B : U) (f : A -> B) (a b : A) (p : Id A a b) -> Id B (f a) (f b)

appOnPath : (A B : U) (f g : A -> B) (a b : A) (q:Id (A->B) f g) (p : Id A a b) -> Id B (f a) (g b)

IdP : (A B :U) -> Id U A B -> A -> B -> U

IdS : (A:U) (F:A -> U) (a0 a1:A) (p:Id A a0 a1) -> F a0 -> F a1 -> U
IdS A F a0 a1 p = IdP (F a0) (F a1) (mapOnPath A U F a0 a1 p)

mapOnPathD : (A : U) (F : A -> U) (f : (x : A) -> F x) (a0 a1 : A) (p : Id A a0 a1) ->
             IdS A F a0 a1 p  (f a0) (f a1)

mapOnPathS : (A:U)(F:A -> U) (C:U) (f: (x:A) -> F x -> C) (a0 a1 : A) (p:Id A a0 a1)
             (b0:F a0) (b1:F a1) (q : IdS A F a0 a1 p b0 b1) -> Id C (f a0 b0) (f a1 b1)