From 850be44c02a872f973c94ab28fe9830c6500db4e Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 24 Apr 2018 23:59:00 -0400 Subject: [PATCH] fix indentation in univalenceAlt --- examples/univalence.ctt | 52 ++++++++++++++++++++--------------------- 1 file changed, 25 insertions(+), 27 deletions(-) diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 4c46d8a..92dfeb9 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -85,36 +85,34 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A -- inlined). The formalization is due to Fabian Ruch. univalenceAlt (B : U) : isContr ((X : U) * equiv X B) = ((B,idEquiv B) - ,\(w : (X : U) * equiv X B) - -> let GlueB : U = Glue B [(i=0) -> (B,idEquiv B), (i=1) -> w] - unglueB (g : GlueB) : B = - unglue g [(i=0) -> (B,idEquiv B) - ,(i=1) -> w] - in (GlueB - ,unglueB - ,\(b : B) - -> let center : fiber GlueB B unglueB b - = (glue (comp ( B) b [(i=0) -> b + ,\(w : (X : U) * equiv X B) -> + let GlueB : U = Glue B [(i=0) -> (B,idEquiv B) + ,(i=1) -> w] + unglueB (g : GlueB) : B = unglue g [(i=0) -> (B,idEquiv B) + ,(i=1) -> w] + unglueEquiv : isEquiv GlueB B unglueB = + \(b : B)-> let ctr : fiber GlueB B unglueB b = + (glue (comp ( B) b [(i=0) -> b ,(i=1) -> (w.2.2 b).1.2]) - [(i=0) -> b - ,(i=1) -> (w.2.2 b).1.1] + [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.1] ,fill ( B) b [(i=0) -> b ,(i=1) -> (w.2.2 b).1.2]) - contr (v : fiber GlueB B unglueB b) - : Path (fiber GlueB B unglueB b) center v - = (glue (comp ( B) b [(i=0) -> v.2 @ (j /\ k) - ,(i=1) -> ((w.2.2 b).2 v @ j).2 - ,(j=0) -> fill ( B) b [(i=0) -> b - ,(i=1) -> (w.2.2 b).1.2] - ,(j=1) -> v.2]) - [(i=0) -> v.2 @ j - ,(i=1) -> ((w.2.2 b).2 v @ j).1] - ,fill ( B) b [(i=0) -> v.2 @ (j /\ l) - ,(i=1) -> ((w.2.2 b).2 v @ j).2 - ,(j=0) -> fill ( B) b [(i=0) -> b - ,(i=1) -> (w.2.2 b).1.2] - ,(j=1) -> v.2]) - in (center,contr))) + contr (v : fiber GlueB B unglueB b) : Path (fiber GlueB B unglueB b) ctr v = + (glue (comp ( B) b [(i=0) -> v.2 @ j /\ k + ,(i=1) -> ((w.2.2 b).2 v @ j).2 + ,(j=0) -> fill ( B) b [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.2] + ,(j=1) -> v.2]) + [(i=0) -> v.2 @ j + ,(i=1) -> ((w.2.2 b).2 v @ j).1] + ,fill ( B) b [(i=0) -> v.2 @ j /\ l + ,(i=1) -> ((w.2.2 b).2 v @ j).2 + ,(j=0) -> fill ( B) b [(i=0) -> b + ,(i=1) -> (w.2.2 b).1.2] + ,(j=1) -> v.2]) + in (ctr,contr) + in (GlueB,unglueB,unglueEquiv)) contrSingl' (A : U) (a b : A) (p : Path A a b) : Path ((x:A) * Path A x b) (b,refl A b) (a,p) = (p @ -i, p @ -i\/j) -- 2.34.1