From: Anders Mörtberg Date: Mon, 20 Nov 2017 23:42:11 +0000 (-0500) Subject: improve uaret X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7a6d2ea8ff1d1ad168a837e4c6ee87fb9ae234d3;p=cubicaltt.git improve uaret --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index 81d063f..60fd32c 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -84,9 +84,10 @@ propIsEquivDirect' (A B : U) (f : A -> B) : prop (isEquiv A B f) = , (j = 1) -> x ] @ k) ] in (sq1 @ i @ j,sq2 @ i @ j)) +-- Using propIsEquivDirect here makes this a lot faster to use later equivLemma (A B : U) : (v w : equiv A B) -> Path (A -> B) v.1 w.1 -> Path (equiv A B) v w - = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) + = lemSig (A -> B) (isEquiv A B) (propIsEquivDirect A B) idIsEquiv (A : U) : isEquiv A A (idfun A) = \(a : A) -> ((a, refl A a) @@ -131,7 +132,7 @@ 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 = - substTrans U (equiv A) A X p (idEquiv A) + subst U (equiv A) A X p (idEquiv A) transDelta (A:U) : equiv A A = transEquiv A A (A) diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 70bf026..a8f0e0e 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -207,31 +207,28 @@ ua (A B : U) (e : equiv A B) : Path U A B = -- have been the identity function (i.e. if the computation rule for J -- would be definitional) this proof would be trivial. uabeta (A B : U) (e : equiv A B) : Path (A -> B) (trans A B (ua A B e)) e.1 = - \(a : A) -> - let b : B = trans B B (<_> B) (e.1 a) - rem1 : Path B b (e.1 a) = fill (<_> B) (e.1 a) [] @ -i - rem2 : Path B (trans B B (<_> B) b) b = fill (<_> B) b [] @ -i - goal : Path B (trans B B (<_> B) b) (e.1 a) = - compPath B (trans B B (<_> B) b) b (e.1 a) rem2 rem1 - in goal @ i + \(a : A) -> fill (<_> B) (fill (<_> B) (e.1 a) [] @ -i) [] @ -i -- uabeta implies that equiv A B is a retract of Path U A B -uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquivDirect A B) = - \(e : equiv A B) -> - equivLemma A B (transEquivDirect A B (ua A B e)) e (uabeta A B e) +-- We don't have to use transEquivDirect: +-- uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquivDirect A B) = +-- \(e : equiv A B) -> +-- equivLemma A B (transEquivDirect A B (ua A B e)) e (uabeta A B e) --- So (B:U) x equiv A B is a retract of (B:U) x Path U A B -opaque uaret +uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquiv A B) = + \(e : equiv A B) -> + let rem (a : A) : Path B ((transEquiv A B (ua A B e)).1 a) (e.1 a) = + fill (<_> B) (fill (<_> B) (e.1 (fill (<_> A) a [] @ -i)) [] @ -i) [] @ -i + in equivLemma A B (transEquiv A B (ua A B e)) e ( \(a : A) -> rem a @ i) +-- So (B:U) x equiv A B is a retract of (B:U) x Path U A B f1 (A : U) (p : (B : U) * equiv A B) : ((B : U) * Path U A B) = (p.1,ua A p.1 p.2) -f2 (A : U) (p : (B : U) * Path U A B) : ((B : U) * equiv A B) = (p.1,transEquivDirect A p.1 p.2) +f2 (A : U) (p : (B : U) * Path U A B) : ((B : U) * equiv A B) = (p.1,transEquiv A p.1 p.2) uaretsig (A : U) : retract ((B : U) * equiv A B) ((B : U) * Path U A B) (f1 A) (f2 A) = \(p : (B : U) * equiv A B) -> (p.1,uaret A p.1 p.2 @ i) -transparent uaret - -- But (B : U) x Path U A B is contractible isContrPath (A : U) : isContr ((B : U) * Path U A B) = let ctr : (B : U) * Path U A B = (A,<_> A)