From: Anders Mörtberg Date: Sat, 23 Jan 2016 17:51:36 +0000 (-0500) Subject: cleaning X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=30b6e14f5c9356dfa9bdc52d98d11d60710a2830;p=cubicaltt.git cleaning --- diff --git a/Eval.hs b/Eval.hs index 1bc9055..028789b 100644 --- a/Eval.hs +++ b/Eval.hs @@ -274,11 +274,10 @@ v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral." (VPath i u) @@@ j = u `swap` (i,j) v @@@ j = VAppFormula v (toFormula j) + ------------------------------------------------------------------------------- -- Composition and filling - - comp :: Name -> Val -> Val -> System Val -> Val comp i a u ts | eps `member` ts = (ts ! eps) `face` (i ~> 1) comp i a u ts = case a of @@ -431,7 +430,6 @@ transpHIT i a@(Ter (HSum _ _ nass) env) u = VPath j $ transpHIT j (aij `face` alpha) (vAlpha @@ j)) vs _ -> error $ "transpHIT: neutral " ++ show u - -- given u(i) of type a(i) "squeezeHIT i a u" connects in the direction i -- transHIT i a u(i=0) to u(i=1) in a(1) squeezeHIT :: Name -> Val -> Val -> Val @@ -737,8 +735,6 @@ lemEq eq b aps = (a,VPath i (compNeg j (eq @@ j) p1 thetas')) -- insertSystem (i ~> 1) (transFillNeg j ej u) $ ws -- theta = compNeg j ej u xs - - -- Old version: -- gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val) -- gradLemmaU b eq us v = (u, VPath i theta'') @@ -831,8 +827,8 @@ instance Convertible Val where (VHComp a u ts,VHComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VGlue v equivs,VGlue v' equivs') -> conv ns (v,equivs) (v',equivs') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') - (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' -- Is this correct? - (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts') + (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' + (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts') (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') _ -> False @@ -893,8 +889,6 @@ instance Normal Val where VUnGlueElem u us -> unglueElem (normal ns u) (normal ns us) VUnGlueElemU e u us -> unGlueU (normal ns e) (normal ns u) (normal ns us) VCompU a ts -> VCompU (normal ns a) (normal ns ts) - -- TODO: Shouldn't we do: - -- VCompU u es -> compUniv (normal ns u) (normal ns es) VVar x t -> VVar x t -- (normal ns t) VFst t -> fstVal (normal ns t) VSnd t -> sndVal (normal ns t) diff --git a/examples/bool.ctt b/examples/bool.ctt index a101367..5edda04 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -170,3 +170,23 @@ eqBool : Id U bool bool = testf : bool = trans bool bool eqBool true testt : bool = trans bool bool eqBool false + +-- Some tests of normal forms of univalence: +testUniv1 (A : U) : Id U A A = + trans (equiv A A) (Id U A A) ( corrUniv A A @ -i) (idEquiv A) + +-- obtained by normal form +ntestUniv1 (A:U) : Id U A A = + comp (<_>U) + (comp (<_>U) A + [ (i = 0) -> comp (<_>U) A [ (l = 0) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> + ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ], (l = 1) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> + ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> A ]) [ (i = 0) -> A, (i = 1) -> A ] + +testUniv2 : bool = trans bool bool (ntestUniv1 bool) true + +ntestUniv2 : bool = + comp ( comp (<_>U) (comp (<_>U) bool [ (i = 0) -> comp (<_>U) bool [ (j = 0) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> + ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ], (j = 1) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> + ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] + diff --git a/examples/hz.ctt b/examples/hz.ctt index a2d5261..782b58c 100644 --- a/examples/hz.ctt +++ b/examples/hz.ctt @@ -1,3 +1,5 @@ +-- Z defined as a quotient of nat * nat by the relation: +-- (x1,x2) ~ (y1,y2) := (x1 + y2 = x2 + y1) module hz where import nat @@ -58,5 +60,8 @@ discretehz : discrete hz = isdiscretesetquot nat2 rel rem rem (x y : nat2) : isdecprop (rel.1 x y).1 = (natSet (add x.1 y.2) (add x.2 y.1),natDec (add x.1 y.2) (add x.2 y.1)) +-- Use the decision procedure to compute if "0 = 1": test01 : bool = discretetobool hz discretehz zeroz onez + +-- Use the decision procedure to compute if "1 = 1": test11 : bool = discretetobool hz discretehz onez onez \ No newline at end of file diff --git a/examples/setquot.ctt b/examples/setquot.ctt index 3661e1f..e0fe8f2 100644 --- a/examples/setquot.ctt +++ b/examples/setquot.ctt @@ -1,3 +1,4 @@ +-- Formalization of (impredicative) set quotients module setquot where import bool diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 697a388..2ed8ee2 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -1,8 +1,8 @@ -- This file contains two proofs of the univalence axiom. One using -- unglue (section 7.2) and a direct one (appendix B of the cubicaltt --- paper). The normal form of the first proof can be computed while --- the second one uses very much memory and don't terminate in --- reasonable time. +-- paper). The normal form of the first proof can be computed (and +-- typecheck, see nthmUniv) while the second one uses very much memory +-- and don't terminate in reasonable time. module univalence where import equiv @@ -77,7 +77,7 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A (isEquivContr (Sigma A B) (Sigma A C) cB cC (totalFun A B C f) (x,z)) -- test normal form --- nequivFunFib : (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A B)) (cC : isContr (Sigma A C)) (x:A) ->isEquiv (B x) (C x) (f x) = \(A : U) -> \(B C : A -> U) -> \(f : (x : A) -> (B x) -> (C x)) -> \(cB : Sigma (Sigma A (\(x : A) -> B x)) (\(x : Sigma A (\(x : A) -> B x)) -> (y : Sigma A (\(x0 : A) -> B x0)) -> IdP ( Sigma A (\(x0 : A) -> B x0)) x y)) -> \(cC : Sigma (Sigma A (\(x : A) -> C x)) (\(x : Sigma A (\(x : A) -> C x)) -> (y : Sigma A (\(x0 : A) -> C x0)) -> IdP ( Sigma A (\(x0 : A) -> C x0)) x y)) -> \(x : A) -> \(z : C x) -> ((comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ !2).1, (!0 = 1)(!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ (!1 /\ !2)).1, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!1 /\ !2)).1, (!1 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> (cC.2 ((x,z)) @ !1).2, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).2 ]) [ (!0 = 0) -> z, (!0 = 1) -> f (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1, (!1 = 1)(!2 = 1) -> (cC.2 ((x,z)) @ !3).1, (!2 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1 ])) cB.1.2 [ (!1 = 0) -> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!1 = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (!2 /\ -!3))) @ !4).1, (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ (!3 /\ !4)).1, (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).2, (!3 = 0) -> cC.1.2 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ !3).2, (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!3)) @ !4).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ (!5 /\ !6)).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!5 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (-!3 \/ -!4))) @ !5).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [ (!3 = 0) -> (cB.2 ((x,x0.1)) @ !0).2 ]) ]) [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1 ])) cB.1.2 [ (!3 = 0) -> cB.1.2 ]) ], (!0 = 1) -> comp ( C x) (x0.2 @ !2) [ (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) x0.1 [ (!3 = 1) -> x0.1, (!4 = 0) -> x0.1 ]), (!3 = 1) -> x0.2 @ !2 ], (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!3 = 1)(!4 = 1) -> x0.1 ], (!3 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [] ]) ])) +nequivFunFib : (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A B)) (cC : isContr (Sigma A C)) (x:A) ->isEquiv (B x) (C x) (f x) = \(A : U) -> \(B C : A -> U) -> \(f : (x : A) -> (B x) -> (C x)) -> \(cB : Sigma (Sigma A (\(x : A) -> B x)) (\(x : Sigma A (\(x : A) -> B x)) -> (y : Sigma A (\(x0 : A) -> B x0)) -> IdP ( Sigma A (\(x0 : A) -> B x0)) x y)) -> \(cC : Sigma (Sigma A (\(x : A) -> C x)) (\(x : Sigma A (\(x : A) -> C x)) -> (y : Sigma A (\(x0 : A) -> C x0)) -> IdP ( Sigma A (\(x0 : A) -> C x0)) x y)) -> \(x : A) -> \(z : C x) -> ((comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ !2).1, (!0 = 1)(!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ (!1 /\ !2)).1, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!1 /\ !2)).1, (!1 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> (cC.2 ((x,z)) @ !1).2, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).2 ]) [ (!0 = 0) -> z, (!0 = 1) -> f (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1, (!1 = 1)(!2 = 1) -> (cC.2 ((x,z)) @ !3).1, (!2 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1 ])) cB.1.2 [ (!1 = 0) -> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!1 = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (!2 /\ -!3))) @ !4).1, (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ (!3 /\ !4)).1, (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).2, (!3 = 0) -> cC.1.2 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ !3).2, (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!3)) @ !4).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ (!5 /\ !6)).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!5 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (-!3 \/ -!4))) @ !5).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [ (!3 = 0) -> (cB.2 ((x,x0.1)) @ !0).2 ]) ]) [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1 ])) cB.1.2 [ (!3 = 0) -> cB.1.2 ]) ], (!0 = 1) -> comp ( C x) (x0.2 @ !2) [ (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) x0.1 [ (!3 = 1) -> x0.1, (!4 = 0) -> x0.1 ]), (!3 = 1) -> x0.2 @ !2 ], (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!3 = 1)(!4 = 1) -> x0.1 ], (!3 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [] ]) ])) lem1 (B:U) : isContr ((X:U) * equiv X B) = @@ -114,7 +114,7 @@ lem1 (B:U) : isContr ((X:U) * equiv X B) = ,(j=1) -> v.2]) in (center,contr))) --- nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> IdP ( B) y (f x))) (\(x : Sigma X (\(x : X) -> IdP ( B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) -> IdP ( Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) x y0)))) -> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ], comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> IdP ( B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a, a),\(z : Sigma B (\(x0 : B) -> IdP ( B) a x0)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> (glueElem (comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> b ], (!1 = 1) -> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ], comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> b, (!3 = 0) -> b ], (!1 = 1) -> v.2 @ (!2 /\ !3), (!2 = 0) -> b ]))))) +nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> IdP ( B) y (f x))) (\(x : Sigma X (\(x : X) -> IdP ( B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) -> IdP ( Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) x y0)))) -> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ], comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> IdP ( B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a, a),\(z : Sigma B (\(x0 : B) -> IdP ( B) a x0)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> (glueElem (comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> b ], (!1 = 1) -> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ], comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> b, (!3 = 0) -> b ], (!1 = 1) -> v.2 @ (!2 /\ !3), (!2 = 0) -> b ]))))) contrSingl' (A : U) (a b : A) (p : Id A a b) : Id ((x:A) * Id A x b) (b,refl A b) (a,p) = (p @ -i, p @ -i\/j) @@ -142,52 +142,29 @@ corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (transEquiv' B A,univalence B A) --- -- Some tests of normal forms: --- testUniv1 (A : U) : Id U A A = --- trans (equiv A A) (Id U A A) ( corrUniv A A @ -i) (idEquiv A) - --- -- obtained by normal form --- ntestUniv1 (A:U) : Id U A A = --- comp (<_>U) --- (comp (<_>U) A --- [ (i = 0) -> comp (<_>U) A [ (l = 0) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> --- ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ], (l = 1) -> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i))))), (i = 1) -> (A,(comp ( A -> A) (\(x : A) -> x) [],comp ( (y : A) -> --- ((x : ((x : A) * IdP ( A) y (comp ( A) (comp ( A) x []) [ (l = 0) -> comp ( A) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : A) * IdP ( A) y (comp ( A) (comp ( A) x0 []) [ (l = 0) -> comp ( A) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : A) -> ((a, a),\(z : ((x : A) * IdP ( A) a x)) -> (z.2 @ l, z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> A ]) [ (i = 0) -> A, (i = 1) -> A ] - --- testUniv2 : bool = trans bool bool (ntestUniv1 bool) true - --- ntestUniv2 : bool = --- comp ( comp (<_>U) (comp (<_>U) bool [ (i = 0) -> comp (<_>U) bool [ (j = 0) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> --- ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ], (j = 1) -> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp ( bool -> bool) (\(x : bool) -> x) [],comp ( (y : bool) -> --- ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] - - --- ------------------------------------------------------------------------------ --- -- The direct proof of univalence using transEquiv which is too slow --- -- to normalize: - --- -- transEquiv is an equiv --- transEquivIsEquiv (A B : U) --- : isEquiv (Id U A B) (equiv A B) (transEquiv A B) --- = gradLemma (Id U A B) (equiv A B) (transEquiv A B) --- (transEquivToId A B) (idToId A B) (eqToEq A B) - --- -- Univalence proved using transEquiv --- univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = --- isoId (Id U A B) (equiv A B) (transEquiv A B) --- (transEquivToId A B) (idToId A B) (eqToEq A B) - --- univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) = --- (transEquiv A B,transEquivIsEquiv A B) - --- -- univalenceTrans takes extremely much memory when normalizing - --- -- This also takes too long to normalize: --- slowtest (A : U) : Id (equiv A A) --- (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) = --- idToId A A (idEquiv A) - - +------------------------------------------------------------------------------ +-- The direct proof of univalence using transEquiv which is too slow +-- to normalize: + +-- transEquiv is an equiv +transEquivIsEquiv (A B : U) + : isEquiv (Id U A B) (equiv A B) (transEquiv A B) + = gradLemma (Id U A B) (equiv A B) (transEquiv A B) + (transEquivToId A B) (idToId A B) (eqToEq A B) + +-- Univalence proved using transEquiv +-- univalenceTrans takes extremely much memory when normalizing +univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = + isoId (Id U A B) (equiv A B) (transEquiv A B) + (transEquivToId A B) (idToId A B) (eqToEq A B) + +univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) = + (transEquiv A B,transEquivIsEquiv A B) + +-- This also takes too long to normalize: +slowtest (A : U) : Id (equiv A A) + (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) = + idToId A A (idEquiv A) -- ------------------------------------------------------------------------------