From: Simon Huber Date: Mon, 14 Sep 2015 12:59:00 +0000 (+0200) Subject: Some experiments with Eq X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f46bf2a644a196876074f8703a88e7ebd00a93a5;p=cubicaltt.git Some experiments with Eq --- diff --git a/examples/eq.ctt b/examples/eq.ctt new file mode 100644 index 0000000..34f0ea6 --- /dev/null +++ b/examples/eq.ctt @@ -0,0 +1,81 @@ +module eq where + +import prelude + +refEq (A : U) (a : A) : Eq A a a = + eqC ( a) [ -> a ] + +JJ (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a)) + (x : A) (p : Eq A a x) : C x p + = eqJ A a C d x p + +JJref (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a)) + : C a (refEq A a) + = eqJ A a C d a (refEq A a) + +JJEq (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a)) + : Eq (C a (refEq A a)) d (JJ A a C d a (refEq A a)) + = refEq (C a (refEq A a)) d + +substEq (A : U) (F : A -> U) (a b : A) (p : Eq A a b) (e : F a) : F b = + JJ A a (\ (x : A) (_ : Eq A a x) -> F x) e b p + +substEqRef (A : U) (F : A -> U) (a : A) (e : F a) : F a = + substEq A F a a (refEq A a) e + +transEq (A : U) (a b c : A) (p : Eq A a b) (q : Eq A b c) : Eq A a c = + substEq A (\ (z : A) -> Eq A a z) b c q p + +transEqRef (A : U) (a b : A) (p : Eq A a b): Eq A a b = + transEq A a a b (refEq A a) p + +eqToId (A : U) (a b : A) (p : Eq A a b) : Id A a b = + eqJ A a (\ (b : A) (p : Eq A a b) -> Id A a b) + ( a) b p + +idToEq (A : U) (a b : A) (p : Id A a b) : Eq A a b = +-- eqC p [] + J A a (\ (b : A) (p : Id A a b) -> Eq A a b) + (refEq A a) b p + +idToEqRef (A : U) (a : A) : Id (Eq A a a) (refEq A a) (idToEq A a a (<_> a)) = + JEq A a (\ (b : A) (p : Id A a b) -> Eq A a b) (refEq A a) + +eqToIdRef (A : U) (a : A) : Id (Id A a a) (<_> a) (eqToId A a a (refEq A a)) = + a + + +idToEqToId (A : U) (a b : A) (p : Id A a b) : + Id (Id A a b) p (eqToId A a b (idToEq A a b p)) = + J A a (\ (b : A) (p : Id A a b) -> + Id (Id A a b) p (eqToId A a b (idToEq A a b p))) + ( eqToId A a a (idToEqRef A a @ j)) b p + +lem (A : U) (a : A) : + Id (Eq A a a) (refEq A a) (idToEq A a a (eqToId A a a (refEq A a))) = + compId (Eq A a a) + (refEq A a) (idToEq A a a (<_> a)) (idToEq A a a (eqToId A a a (refEq A a))) + (idToEqRef A a) ( idToEq A a a (eqToIdRef A a @ k)) + +eqToIdToEq (A : U) (a b : A) (p : Eq A a b) : + Id (Eq A a b) p (idToEq A a b (eqToId A a b p)) = + eqJ A a (\ (b : A) (p : Eq A a b) -> + Id (Eq A a b) p (idToEq A a b (eqToId A a b p))) + (lem A a) b p + + +-------------------------------------------------------------------------------- +-- Some tests + +mop (A B : U) (f : A -> B) (u v : A) (p : Eq A u v) : Eq B (f u) (f v) = + JJ A u (\ (v : A) (p : Eq A u v) -> Eq B (f u) (f v)) + (refEq B (f u)) v p + +mopComp (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Eq A u v) + : Eq C (g (f u)) (g (f v)) = mop A C (\ (x : A) -> g (f x)) u v p + +mopComp' (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Eq A u v) + : Eq C (g (f u)) (g (f v)) = mop B C g (f u) (f v) (mop A B f u v p) + +superMop (A B : U) (f : A -> B) (u v : A) (p : Id A u v) : Eq B (f u) (f v) = + eqC ( f (p @ i)) [ ]