From: Rafaël Bocquet Date: Tue, 12 Apr 2016 15:29:34 +0000 (+0200) Subject: visible_all command X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=35fc628baccd8f4a7fd39ba609b67a3cd0e88e0e;p=cubicaltt.git visible_all command --- diff --git a/CTT.hs b/CTT.hs index c92fff2..8bd2f35 100644 --- a/CTT.hs +++ b/CTT.hs @@ -40,6 +40,7 @@ type Decl = (Ident,(Ter,Ter)) data Decls = MutualDecls [Decl] | OpaqueDecl Ident | VisibleDecl Ident + | VisibleAllDecl deriving Eq declIdents :: [Decl] -> [Ident] @@ -237,6 +238,7 @@ def :: Decls -> Env -> Env def (MutualDecls ds) (rho,vs,fs,Nameless os) = (Def ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds))) def (OpaqueDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.insert n os)) def (VisibleDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.delete n os)) +def VisibleAllDecl (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless Set.empty) sub :: (Name,Formula) -> Env -> Env sub (i,phi) (rho,vs,fs,os) = (Sub i rho,vs,phi:fs,os) @@ -377,6 +379,7 @@ showDecls (MutualDecls defs) = [ text x <+> equals <+> showTer d | (x,(_,d)) <- defs ] showDecls (OpaqueDecl i) = text "opaque" <+> text i showDecls (VisibleDecl i) = text "visible" <+> text i +showDecls VisibleAllDecl = text "visible_all" instance Show Val where show = render . showVal diff --git a/Eval.hs b/Eval.hs index 148ea46..9a651bc 100644 --- a/Eval.hs +++ b/Eval.hs @@ -150,7 +150,7 @@ eval rho@(_,_,_,Nameless os) v = case v of U -> VU App r s -> app (eval rho r) (eval rho s) Var i - | i `elem` os -> VOpaque i t + | i `elem` os -> VOpaque i (lookType i rho) | otherwise -> look i rho Pi t@(Lam _ a _) -> VPi (eval rho a) (eval rho t) Sigma t@(Lam _ a _) -> VSigma (eval rho a) (eval rho t) diff --git a/Exp.cf b/Exp.cf index d4a8784..6a95ee6 100644 --- a/Exp.cf +++ b/Exp.cf @@ -12,15 +12,16 @@ Module. Module ::= "module" AIdent "where" "{" [Imp] [Decl] "}" ; Import. Imp ::= "import" AIdent ; separator Imp ";" ; -DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; -DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; -DeclHData. Decl ::= "hdata" AIdent [Tele] "=" [Label] ; -DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; -DeclUndef. Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ; -DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; -DeclOpaque. Decl ::= "opaque" AIdent ; -DeclVisible. Decl ::= "visible" AIdent ; -separator Decl ";" ; +DeclDef. Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ; +DeclData. Decl ::= "data" AIdent [Tele] "=" [Label] ; +DeclHData. Decl ::= "hdata" AIdent [Tele] "=" [Label] ; +DeclSplit. Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ; +DeclUndef. Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ; +DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ; +DeclOpaque. Decl ::= "opaque" AIdent ; +DeclVisible. Decl ::= "visible" AIdent ; +DeclVisibleAll. Decl ::= "visible_all" ; +separator Decl ";" ; Where. ExpWhere ::= Exp "where" "{" [Decl] "}" ; NoWhere. ExpWhere ::= Exp ; diff --git a/Resolver.hs b/Resolver.hs index f5414ec..f4573a1 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -344,6 +344,7 @@ resolveDecl d = case d of DeclVisible i -> do resolveVar i return (CTT.VisibleDecl (unAIdent i), []) + DeclVisibleAll -> return (CTT.VisibleAllDecl, []) _ -> do let (f,typ,body,ns) = resolveNonMutualDecl d a <- typ d <- body diff --git a/TypeChecker.hs b/TypeChecker.hs index 918e443..b89cc5d 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -234,6 +234,7 @@ checkDecls (MutualDecls d) = do checks (tele,rho) ters checkDecls (OpaqueDecl _) = return () checkDecls (VisibleDecl _) = return () +checkDecls VisibleAllDecl = return () -- Check a telescope checkTele :: Tele -> Typing () diff --git a/examples/helix.ctt b/examples/helix.ctt index 07876e9..4e7f876 100644 --- a/examples/helix.ctt +++ b/examples/helix.ctt @@ -4,7 +4,7 @@ import circle import equiv import pi -oneTurn (l: loopS1) : loopS1 = compS1 l loop1 +oneTurn (l: loopS1) : loopS1 = compS1 l loop1 backTurn (l: loopS1) : loopS1 = compS1 l invLoop @@ -17,7 +17,7 @@ compInvS1 : Id loopS1 (refl S1 base) (compS1 invLoop loop1) = compInv S1 base ba compInv (A:U) (a b:A) (q:Id A a b) : (x:A) (p:Id A b x) -> Id (Id A a b) q (compId A a x b (compId A a b x q p) (p@-i)) = J A b (\ (x:A) (p:Id A b x) -> Id (Id A a b) q (compId A a x b (compId A a b x q p) (p@-i))) rem - where rem : Id (Id A a b) q + where rem : Id (Id A a b) q (comp (<_>A) (comp (<_>A) (q@i) [(i=0) -> <_>a,(i=1) -> <_>b]) [(i=0) -> <_>a,(i=1) -> <_>b]) = comp (<_>A) (comp (<_>A) (q@i) [(j=0) -> <_>q@i,(i=0) -> <_>a,(i=1) -> <_>b]) [(j=0) -> <_>q@i,(i=0) -> <_>a,(i=1) -> <_>b] @@ -30,14 +30,14 @@ transC (A:U) (a:A) : A = comp (<_>A) a [] lemTransC (A:U) (a:A) : Id A (transC A a) a = comp (<_>A) a [(i=1) -> <_>a] lemFib1 (A:U) (F G : A -> U) (a:A) (fa : F a -> G a) : - (x:A) (p : Id A a x) -> (fx : F x -> G x) -> + (x:A) (p : Id A a x) -> (fx : F x -> G x) -> Id U (Id (F a -> G x) (\ (u:F a) -> subst A G a x p (fa u)) (\ (u:F a) -> fx (subst A F a x p u))) (IdP (F (p@i) -> G (p@i)) fa fx) = - J A a (\ (x:A) (p : Id A a x) -> (fx : F x -> G x) -> + J A a (\ (x:A) (p : Id A a x) -> (fx : F x -> G x) -> Id U (Id (F a -> G x) (\ (u:F a) -> subst A G a x p (fa u)) (\ (u:F a) -> fx (subst A F a x p u))) (IdP (F (p@i) -> G (p@i)) fa fx)) rem where - rem (ga : F a -> G a) : Id U (Id (F a -> G a) (\ (u:F a) -> transC (G a) (fa u)) (\ (u:F a) -> ga (transC (F a) u))) + rem (ga : F a -> G a) : Id U (Id (F a -> G a) (\ (u:F a) -> transC (G a) (fa u)) (\ (u:F a) -> ga (transC (F a) u))) (Id (F a -> G a) fa ga) = Id (F a -> G a) (\ (u:F a) -> lemTransC (G a) (fa u)@j) (\ (u : F a) -> ga (lemTransC (F a) u@j)) @@ -49,17 +49,17 @@ corFib1 (A:U) (F G : A -> U) (a:A) (fa ga : F a -> G a) (p:Id A a a) compIdL (A:U) (a b:A) (p : Id A a b) : Id (Id A a b) p (compId A a b b p (<_>b)) = - comp (<_>A) (p @ i) [(i=0) -> <_> a, (i = 1) -> <_>b, (j=0) -> <_>(p@i) ] + comp (<_>A) (p @ i) [(i=0) -> <_> a, (i = 1) -> <_>b, (j=0) -> <_>(p@i) ] -lemFib2 (A:U) (F:A->U) (a b:A) (p:Id A a b) (u:F a) : +lemFib2 (A:U) (F:A->U) (a b:A) (p:Id A a b) (u:F a) : (c:A) (q:Id A b c) -> Id (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (compId A a b c p q) u) = J A b (\ (c:A) (q:Id A b c) -> Id (F c) (subst A F b c q (subst A F a b p u)) (subst A F a c (compId A a b c p q) u)) rem - where + where rem1 : Id (F b) (subst A F a b p u) (subst A F b b (<_>b) (subst A F a b p u)) = lemTransC (F b) (subst A F a b p u)@-i rem2 : Id (F b) (subst A F a b p u) (subst A F a b (compId A a b b p (<_>b)) u) = subst A F a b (compIdL A a b p@i) u - rem : Id (F b) (subst A F b b (<_>b) (subst A F a b p u)) (subst A F a b (compId A a b b p (<_>b)) u) = + rem : Id (F b) (subst A F b b (<_>b) (subst A F a b p u)) (subst A F a b (compId A a b b p (<_>b)) u) = comp (Id (F b) (rem1@i) (rem2@i)) (<_>subst A F a b p u) [] testIsoId (A B : U) (f : A -> B) (g : B -> A) @@ -69,16 +69,16 @@ testIsoId (A B : U) (f : A -> B) (g : B -> A) testH (n:Z) : Z = subst S1 helix base base loop1 n -testHelix : Id (Z->Z) sucZ (subst S1 helix base base loop1) = +testHelix : Id (Z->Z) sucZ (subst S1 helix base base loop1) = \(n:Z) -> testIsoId Z Z sucZ predZ sucpredZ predsucZ n@i encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ itLoop : nat -> loopS1 = split zero -> triv - suc n -> oneTurn (itLoop n) + suc n -> oneTurn (itLoop n) -itLoopNeg : nat -> loopS1 = split +itLoopNeg : nat -> loopS1 = split zero -> invLoop suc n -> backTurn (itLoopNeg n) @@ -116,14 +116,14 @@ decode : (x:S1) -> helix x -> Id S1 base x = split G (x:S1) : U = Id S1 base x p : Id U T T = helix (loop1@j) -> Id S1 base (loop1@j) rem2 (n:Z) : Id loopS1 (oneTurn (loopIt n)) (loopIt (sucZ n)) = lem1It n@-i - rem1 (n:Z) : Id loopS1 (subst S1 G base base loop1 (loopIt n)) (loopIt (subst S1 helix base base loop1 n)) = + rem1 (n:Z) : Id loopS1 (subst S1 G base base loop1 (loopIt n)) (loopIt (subst S1 helix base base loop1 n)) = comp ( Id loopS1 (oneTurn (loopIt n)) (loopIt (testHelix@i n))) (rem2 n) [] rem : IdP p loopIt loopIt = corFib1 S1 helix G base loopIt loopIt loop1 rem1 -encodeDecode (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p = +encodeDecode (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p = transport (Id (Id S1 base (p@i)) (decode (p@i) (encode (p@i) (p@(i/\j)))) (p@(i/\j))) (refl loopS1 triv) --- encodeDecode : (c : S1) (p : Id S1 base c) -> Id (Id S1 base c) (decode c (encode c p)) p = +-- encodeDecode : (c : S1) (p : Id S1 base c) -> Id (Id S1 base c) (decode c (encode c p)) p = -- J S1 base (\ (c : S1) (p : Id S1 base c) -> Id (Id S1 base c) (decode c (encode c p)) p) -- (<_> (<_> base)) @@ -133,11 +133,11 @@ lemTransOneTurn (n:nat) : Id Z (transport (helix (loop1@i)) (inr n)) (inr (su lemTransBackTurn (n:nat) : Id Z (transport (helix (loop1@-i)) (inl n)) (inl (suc n)) = inl (suc (comp (<_>nat) (comp (<_>nat) n [(i=1) -> <_>n]) [(i=1) -> <_>n])) -corFib2 (u:Z) (l:loopS1) : Id Z (transport (helix (oneTurn l@i)) u) +corFib2 (u:Z) (l:loopS1) : Id Z (transport (helix (oneTurn l@i)) u) (transport (helix (loop1@i)) (transport (helix (l@i)) u)) = lemFib2 S1 helix base base l u base loop1@-i -corFib3 (u:Z) (l:loopS1) : Id Z (transport (helix (backTurn l@i)) u) +corFib3 (u:Z) (l:loopS1) : Id Z (transport (helix (backTurn l@i)) u) (transport (helix (loop1@-i)) (transport (helix (l@i)) u)) = lemFib2 S1 helix base base l u base (loop1@-j)@-i @@ -146,12 +146,12 @@ decodeEncodeBasePos : (n : nat) -> Id Z (transport ( helix (itLoop n @ x)) (i suc n -> comp (Id Z (transport (helix (oneTurn l@i)) (inr zero)) (lemTransOneTurn n@j)) rem3 [] where l : loopS1 = itLoop n rem1 : Id Z (transport ( helix (l@i)) (inr zero)) (inr n) = decodeEncodeBasePos n - rem2 : Id Z (transport (helix (oneTurn l@i)) (inr zero)) - (transport (helix (loop1@i)) (transport (helix (l@i)) (inr zero))) = + rem2 : Id Z (transport (helix (oneTurn l@i)) (inr zero)) + (transport (helix (loop1@i)) (transport (helix (l@i)) (inr zero))) = corFib2 (inr zero) l - rem3 : Id Z (transport (helix (oneTurn l@i)) (inr zero)) - (transport (helix (loop1@i)) (inr n)) = - comp (Id Z (transport (helix (oneTurn l@i)) (inr zero)) + rem3 : Id Z (transport (helix (oneTurn l@i)) (inr zero)) + (transport (helix (loop1@i)) (inr n)) = + comp (Id Z (transport (helix (oneTurn l@i)) (inr zero)) (transport (helix (loop1@i)) (rem1@j))) rem2 [] decodeEncodeBaseNeg : (n : nat) -> Id Z (transport ( helix (itLoopNeg n @ x)) (inr zero)) (inl n) = split @@ -159,19 +159,19 @@ decodeEncodeBaseNeg : (n : nat) -> Id Z (transport ( helix (itLoopNeg n @ x)) suc n -> comp (Id Z (transport (helix (backTurn l@i)) (inr zero)) (lemTransBackTurn n@j)) rem3 [] where l : loopS1 = itLoopNeg n rem1 : Id Z (transport ( helix (l@i)) (inr zero)) (inl n) = decodeEncodeBaseNeg n - rem2 : Id Z (transport (helix (backTurn l@i)) (inr zero)) - (transport (helix (loop1@-i)) (transport (helix (l@i)) (inr zero))) = + rem2 : Id Z (transport (helix (backTurn l@i)) (inr zero)) + (transport (helix (loop1@-i)) (transport (helix (l@i)) (inr zero))) = corFib3 (inr zero) l - rem3 : Id Z (transport (helix (backTurn l@i)) (inr zero)) - (transport (helix (loop1@-i)) (inl n)) = - comp (Id Z (transport (helix (backTurn l@i)) (inr zero)) + rem3 : Id Z (transport (helix (backTurn l@i)) (inr zero)) + (transport (helix (loop1@-i)) (inl n)) = + comp (Id Z (transport (helix (backTurn l@i)) (inr zero)) (transport (helix (loop1@-i)) (rem1@j))) rem2 [] -decodeEncodeBase : (n : Z) -> Id Z (encode base (decode base n)) n = split +decodeEncodeBase : (n : Z) -> Id Z (encode base (decode base n)) n = split inl n -> decodeEncodeBaseNeg n inr n -> decodeEncodeBasePos n -loopS1equalsZ : Id U loopS1 Z = +loopS1equalsZ : Id U loopS1 Z = isoId loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base) setLoop : set loopS1 = substInv U set loopS1 Z loopS1equalsZ ZSet @@ -191,7 +191,7 @@ isGroupoidS1 : groupoid S1 = lem lem : (x y : S1) -> set (Id S1 x y) = lemPropFib (\ (x:S1) -> (y : S1) -> set (Id S1 x y)) pP lem2 - where + where pP (x:S1) : prop ((y:S1) -> set (Id S1 x y)) = propPi S1 (\ (y:S1) -> set (Id S1 x y)) (\ (y:S1) -> setIsProp (Id S1 x y)) @@ -229,7 +229,7 @@ lemSetTorus (E : S1 -> S1 -> U) (sE : set (E base base)) rem3 : prop (P y) = substInv U prop (P y) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) rem1 rem2 - + lem2 : IdS S1 (G base) base base loop1 (g base) (g base) = g (loop1 @ j) @@ -254,13 +254,13 @@ multCom : (x y : S1) -> Id S1 (mult x y) (mult y x) = -- associativity -multAssoc (x :S1) : (y z : S1) -> Id S1 (mult x (mult y z)) (mult (mult x y) z) = +multAssoc (x :S1) : (y z : S1) -> Id S1 (mult x (mult y z)) (mult (mult x y) z) = lemSetTorus E sE f g efg where E (y z : S1) : U = Id S1 (mult x (mult y z)) (mult (mult x y) z) sE : set (E base base) = isGroupoidS1 x x f (z : S1) : E base z = rem - where + where rem1 : Id S1 (mult base z) z = multCom base z rem : Id S1 (mult x (mult base z)) (mult x z) = mult x (rem1 @ i) @@ -269,14 +269,14 @@ multAssoc (x :S1) : (y z : S1) -> Id S1 (mult x (mult y z)) (mult (mult x y) z) -- inverse law -lemPropRel (P:S1 -> S1 -> U) (pP:(x y:S1) -> prop (P x y)) (bP:P base base) : (x y:S1) -> P x y = +lemPropRel (P:S1 -> S1 -> U) (pP:(x y:S1) -> prop (P x y)) (bP:P base base) : (x y:S1) -> P x y = lemPropFib (\ (x:S1) -> (y:S1) -> P x y) (\ (x:S1) -> propPi S1 (P x) (pP x)) - (lemPropFib (P base) (pP base) bP) + (lemPropFib (P base) (pP base) bP) invLaw : (x y : S1) -> Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y)) - (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) = lemPropRel P pP bP + (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) = lemPropRel P pP bP where P (x y : S1) : U = Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y)) @@ -286,13 +286,13 @@ invLaw : (x y : S1) -> isGroupoidS1 (mult x y) (mult x y) (refl S1 (mult x y)) (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) - bP : P base base = + bP : P base base = comp (Id (Id S1 base base) (refl S1 base) (comp (<_>S1) base [(i=0) -> refl S1 base, (j=0) -> refl S1 base, (j=1) -> refl S1 base])) (refl (Id S1 base base) (refl S1 base)) [] -- the multiplication is invertible -multIsEquiv : (x:S1) -> isEquiv S1 S1 (mult x) = lemPropFib P pP bP +multIsEquiv : (x:S1) -> isEquiv S1 S1 (mult x) = lemPropFib P pP bP where P (x:S1) : U = isEquiv S1 S1 (mult x) pP (x:S1) : prop (P x) = propIsEquiv S1 S1 (mult x) rem : Id (S1 -> S1) (idfun S1) (mult base) = \ (x:S1) -> idL x @ -i @@ -304,11 +304,11 @@ invMult (x y:S1) : S1 = (multIsEquiv x y).1.1 invS1 (x:S1) : S1 = invMult x base -lem : Id S1 (invS1 base) base = comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base] +lemInvS1 : Id S1 (invS1 base) base = comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base] loopInvS1 : U = Id S1 (invS1 base) (invS1 base) -rePar (l: loopInvS1) : loopS1 = transport (Id S1 (lem@i) (lem@i)) l +rePar (l: loopInvS1) : loopS1 = transport (Id S1 (lemInvS1@i) (lemInvS1@i)) l test2 : Z = winding (rePar (invS1 (loop2@i))) -- EVAL: inl (suc zero) Time: 1m26.400s diff --git a/examples/torsor.ctt b/examples/torsor.ctt index 24a5c53..9c44d9a 100644 --- a/examples/torsor.ctt +++ b/examples/torsor.ctt @@ -392,10 +392,8 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p pS : IdP ( p@i -> p@i) (BZS BA) (BZS BB) = w.2 pASet : IdP ( set (p@i)) ASet BSet = lemIdPProp (set A) (set B) (setIsProp A) ( set (p@i)) ASet BSet - opaque pASet pNE : IdP ( ishinh_UU (p@i)) a b = lemIdPProp (ishinh_UU A) (ishinh_UU B) (propishinh A) ( ishinh_UU (p@i)) a b - opaque pNE pShift : IdP ( equiv (p@i) (p@i)) AShift BShift = ( pS @ i , (lemIdPProp @@ -413,7 +411,6 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p (\(x : A) -> propIsEquiv Z A (action A AShift x))) ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x)) AEquiv BEquiv - opaque pEquiv hole : Id BZ BA BB = (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i)))) G (q : Id BZ BA BB) : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB) = ( BZSet (q @ i), (BZShift (q@i)).1) GF (w : (p : Id U A B) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) @@ -426,10 +423,8 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p q2 : Id BZ BA BB = F (p, p2) pASet : Id (IdP ( set (p@i)) ASet BSet) ( BZASet (q2@i)) ( BZASet (q@i)) = lemIdPSet (set A) (set B) (propSet (set A) (setIsProp A)) ( set (p@i)) ASet BSet ( BZASet (q2@i)) ( BZASet (q@i)) - opaque pASet pNE : Id (IdP ( ishinh_UU (p@i)) a b) ( BZNE (q2@i)) ( BZNE (q@i)) = lemIdPSet (ishinh_UU A) (ishinh_UU B) (propSet (ishinh_UU A) (propishinh A)) ( ishinh_UU (p@i)) a b ( BZNE (q2@i)) ( BZNE (q@i)) - opaque pNE pShift : Id (IdP ( equiv (p@i) (p@i)) AShift BShift) ( BZShift (q2@i)) ( BZShift (q@i)) = ( p2 @ i , (lemIdPSet @@ -440,7 +435,6 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p AShift.2 BShift.2 ( (BZShift (q2@i)).2) ( (BZShift (q@i)).2)) @ j @ i ) - opaque pShift pEquiv : IdP ( IdP ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x)) AEquiv BEquiv) ( BZEquiv (q2@i)) ( BZEquiv (q@i)) = lemIdPSet2 ((x : A) -> isEquiv Z A (action A AShift x)) @@ -452,7 +446,6 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@1@i) x)) ( (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x)) AEquiv BEquiv ( BZEquiv (q2@i)) ( BZEquiv (q@i)) - opaque pEquiv hole : Id (Id BZ BA BB) q2 q = (p@i, (pASet@j@i, (pNE@j@i, (pShift@j@i, pEquiv@j@i)))) hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP ( p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF) @@ -580,29 +573,32 @@ invLoopZ : loopBZ = loopZ @ -i encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport ( BZSet (p@i)) zeroZ -decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 ( p @ -i, q) - where - p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a - p : Id U (BZSet A) Z = (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i - hole1 (x : Z) : Id Z (transport p (BZS A (transport ( p @ -i) x))) - (p1 (BZS A (BZAction A a x))).1.1 - = compId Z (transport p (BZS A (transport ( p @ -i) x))) - (transport p (BZS A (BZAction A a x))) - (p1 (BZS A (BZAction A a x))).1.1 - ( transport p (BZS A (lem0 Z (BZSet A) (BZAction A a) p1 x @ i))) - (lem1 Z (BZSet A) (BZAction A a) p1 (BZS A (BZAction A a x))) - opaque hole1 - hole2 (x : Z) : Id Z (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) - = compId Z (p1 (BZS A (BZAction A a x))).1.1 (p1 (BZAction A a (sucZ x))).1.1 (sucZ x) - ( (p1 (lem2 (BZSet A) (BZShift A) a x @ i)).1.1) - (secEq Z (BZSet A) (BZAction A a, p1) (sucZ x)) - opaque hole2 - hole : Id (Z->Z) (\(x : Z) -> transport p (BZS A (transport ( p @ -i) x))) sucZ - = \(x : Z) -> compId Z (transport p (BZS A (transport ( p @ -i) x))) (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) (hole1 x) (hole2 x) @ i - opaque hole - q : IdP ( (p@-i) -> (p@-i)) sucZ (BZS A) - = substIdP (BZSet A -> BZSet A) (Z -> Z) ( (p@i) -> (p@i)) (BZS A) sucZ hole @ -i - opaque q +decodeZP (A : BZ) (a : BZSet A) : Id U (BZSet A) Z = (univalence (BZSet A) Z (BZAction A a, BZEquiv A a)).1.1 @ -i + +decodeZ1 (A : BZ) (a : BZSet A) (x : Z) : Id Z (transport (decodeZP A a) (BZS A (transport ( (decodeZP A a) @ -i) x))) + (BZEquiv A a (BZS A (BZAction A a x))).1.1 + = compId Z (transport (decodeZP A a) (BZS A (transport ( (decodeZP A a) @ -i) x))) + (transport (decodeZP A a) (BZS A (BZAction A a x))) + (BZEquiv A a (BZS A (BZAction A a x))).1.1 + ( transport (decodeZP A a) (BZS A (lem0 Z (BZSet A) (BZAction A a) (BZEquiv A a) x @ i))) + (lem1 Z (BZSet A) (BZAction A a) (BZEquiv A a) (BZS A (BZAction A a x))) +opaque decodeZ1 + +decodeZ2 (A : BZ) (a : BZSet A) (x : Z) : Id Z (BZEquiv A a (BZS A (BZAction A a x))).1.1 (sucZ x) + = compId Z (BZEquiv A a (BZS A (BZAction A a x))).1.1 (BZEquiv A a (BZAction A a (sucZ x))).1.1 (sucZ x) + ( (BZEquiv A a (lem2 (BZSet A) (BZShift A) a x @ i)).1.1) + (secEq Z (BZSet A) (BZAction A a, BZEquiv A a) (sucZ x)) +opaque decodeZ2 + +decodeZ3 (A : BZ) (a : BZSet A) : Id (Z->Z) (\(x : Z) -> transport (decodeZP A a) (BZS A (transport ( (decodeZP A a) @ -i) x))) sucZ + = \(x : Z) -> compId Z (transport (decodeZP A a) (BZS A (transport ( (decodeZP A a) @ -i) x))) (BZEquiv A a (BZS A (BZAction A a x))).1.1 (sucZ x) (decodeZ1 A a x) (decodeZ2 A a x) @ i +opaque decodeZ3 + +decodeZQ (A : BZ) (a : BZSet A) : IdP ( ((decodeZP A a)@-i) -> ((decodeZP A a)@-i)) sucZ (BZS A) + = substIdP (BZSet A -> BZSet A) (Z -> Z) ( ((decodeZP A a)@i) -> ((decodeZP A a)@i)) (BZS A) sucZ (decodeZ3 A a) @ -i +opaque decodeZQ + +decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 ( decodeZP A a @ -i, decodeZQ A a) prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = hole where @@ -721,6 +717,11 @@ GF : (y : S1) -> (x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F (lemHcomp3 (<_> base)) opaque GF +F_fullyFaithful0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 + = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base) +opaque F_fullyFaithful0 + + F_fullyFaithful : (x y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y) = lemPropFib (\(x : S1) -> (y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)) (\(x : S1) -> propPi S1 (\(y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)) @@ -729,12 +730,8 @@ F_fullyFaithful : (x y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPa (\(y : S1) -> propIsEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y)) hole) where - hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 - = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base) - opaque hole0 hole : isEquiv loopS1 loopBZ (mapOnPath S1 BZ F base base) - = transport ( isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2 - opaque hole + = transport ( isEquiv loopS1 loopBZ (F_fullyFaithful0 @ -i)) loopS1equalsLoopBZ'.2 opaque F_fullyFaithful F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole @@ -752,7 +749,14 @@ S1equalsBZ : Id U S1 BZ = hole where G (y : BZ) : S1 = (F_essentiallySurjective y).1 FG (y : BZ) : Id BZ (F (G y)) y = (F_essentiallySurjective y).2 @ -i - opaque FG GF (x : S1) : Id S1 (G (F x)) x = (F_fullyFaithful (G (F x)) x (FG (F x))).1.1 - opaque GF - hole : Id U S1 BZ = isoId S1 BZ F G FG GF \ No newline at end of file + hole : Id U S1 BZ = isoId S1 BZ F G FG GF + +invBZ : BZ -> BZ = transport ( S1equalsBZ@i -> S1equalsBZ@i) invS1 +doubleLoopBZ : loopBZ -> loopBZ = transport ( loopS1equalsLoopBZ@i -> loopS1equalsLoopBZ@i) doubleLoop + +-- > transport ( BZSet (doubleLoopBZ loopZ @ i)) zeroZ +-- EVAL: inr (suc (suc zero)) +-- Time: 0m25.191s + +-- visible_all