From: Anders Mörtberg Date: Wed, 6 Dec 2017 16:27:11 +0000 (-0500) Subject: proof relating function part of transEquiv to transEquivDirect X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=682e9f66ce16daf166549c1a16dd3a110894a8ea;p=cubicaltt.git proof relating function part of transEquiv to transEquivDirect --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index 60fd32c..dc2f405 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -108,7 +108,7 @@ secEq (A B:U) (w:equiv A B) (x:A) : Path A (invEq A B w (w.1 x)) x = transEquivDirect (A B:U) (p:Path U A B) : equiv A B = (f,p) where - f (x:A) : B = comp p x [] + f (x:A) : B = trans A B p x g (y:B) : A = comp (p@-i) y [] lem1 (x:A) : PathP p x (f x) = comp (p@(i/\j)) x [(i=0) -> x] lem2 (y:B) : PathP p (g y) y = comp (p@(i\/-j)) y [(i=1) -> y] @@ -131,8 +131,15 @@ lemSinglContr (A:U) (a:A) : isContr ((x:A) * Path A a x) = idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A) -transEquiv (A X:U) (p:Path U A X) : equiv A X = - subst U (equiv A) A X p (idEquiv A) +transEquiv (A B : U) (p : Path U A B) : equiv A B = + subst U (equiv A) A B p (idEquiv A) + +compf (A B C : U) (f : B -> C) (g : A -> B) : A -> C = + \(a : A) -> f (g a) + +transEquivEq (A B : U) (p : Path U A B) : + Path (A -> B) (transEquiv A B p).1 (compf A A B (trans A B p) (trans A A (<_> A))) = + <_> (transEquiv A B p).1 transDelta (A:U) : equiv A A = transEquiv A A (A)