cubical-0.2.0: examples/primitives.cub

module primitives where

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

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

primitive inh : U -> U

primitive inc : (A : U) -> A -> inh A

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

primitive squash : (A : U) -> prop (inh A)

primitive inhrec : (A : U) (B : U) (p : prop B) (f : A -> B) (a : inh A) -> B

Sigma : (A : U) (B : A -> U) -> U
Sigma A B = (x : A) * B x

fiber : (A B : U) (f : A -> B) (y : B) -> U
fiber A B f y = Sigma A (\x -> 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)

sId : (A : U) (a : A) -> pathTo A a
sId A a = (a, refl A a)

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

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

primitive 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

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

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

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

primitive 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)

primitive 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)

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

primitive 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)

primitive 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)

primitive 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)

primitive 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)

primitive funHExt : (A : U) (B : A -> U) (f g : (a : A) -> B a) ->
                    ((x y : A) -> (p : Id A x y) -> IdS A B x y p (f x) (g y)) ->
                    Id ((y : A) -> B y) f g

-- The circle.
primitive S1 : U

primitive base : S1

primitive loop : Id S1 base base

primitive S1rec : (F : S1 -> U) (b : F base)
                  (l : IdS S1 F base base loop b b) (x : S1) -> F x

-- The interval.
primitive I : U

primitive I0 : I

primitive I1 : I

primitive line : Id I I0 I1

primitive intrec : (F : I -> U) (s : F I0) (e : F I1)
                   (l : IdS I F I0 I1 line s e) (x : I) -> F x