visible_all command

diff --git a/CTT.hs b/CTT.hs
index c92fff228bf63ddc2237576e1979df92e1658223..8bd2f35eb8164e730079463d2f4db9e9af71d570 100644 (file)
--- 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 148ea46f6cd1d10e224653f2773202d9d4b53833..9a651bc2c5fbb1726c82afc28837b3571b3e7cb1 100644 (file)
--- 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 d4a878491919de90c872cc5eb5458937ec14ffa9..6a95ee6322e4e5eb15eb20ba00369910c26c014c 100644 (file)
--- 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 f5414eccb0cae89986d230eb87ffa5b6220be092..f4573a14f427eccebd9e1bb960ac0ccfd590ee02 100644 (file)
--- 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 918e443d8c06d19bd1743d1006b9c468b119ae6e..b89cc5dfed32bb5ce73954fe0921908b61bdfd96 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -234,6 +234,7 @@ checkDecls (MutualDecls d) = do
     checks (tele,rho) ters\r
 checkDecls (OpaqueDecl _) = return ()\r
 checkDecls (VisibleDecl _) = return ()\r
+checkDecls VisibleAllDecl = return ()\r
 \r
 -- Check a telescope\r
 checkTele :: Tele -> Typing ()\r

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 07876e9abec410ff201d5dc1e4693360dab44265..4e7f8768ca9c9c37b4fce2e031b1f1dfbb4d893b 100644 (file)
--- 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) (<i>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) (<i>p@-i))) rem
- where rem : Id (Id A a b) q 
+ where rem : Id (Id A a b) q
                            (<i>comp (<_>A) (comp (<_>A) (q@i) [(i=0) -> <_>a,(i=1) -> <_>b]) [(i=0) -> <_>a,(i=1) -> <_>b]) =
           <j i>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 = <i>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 (<i>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 (<i>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) =
     <j>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)) =
- <j i>comp (<_>A) (p @ i) [(i=0) -> <_> a, (i = 1) -> <_>b, (j=0) -> <_>(p@i) ]   
+ <j 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)) =  <i>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) =
       <i>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 (<i>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) =
   <i>\(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 = <j> helix (loop1@j) -> Id S1 base (loop1@j)
          rem2 (n:Z) : Id loopS1 (oneTurn (loopIt n)) (loopIt (sucZ n)) = <i>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 (<i> 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 (<i>Id (Id S1 base (p@i)) (decode (p@i) (encode (p@i) (<j>p@(i/\j)))) (<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 (<i>helix (loop1@i)) (inr n)) (inr (su
 lemTransBackTurn (n:nat) : Id Z (transport (<i>helix (loop1@-i)) (inl n)) (inl (suc n)) =
  <i>inl (suc (comp (<_>nat) (comp (<_>nat) n [(i=1) -> <_>n]) [(i=1) -> <_>n]))
 
-corFib2 (u:Z) (l:loopS1) : Id Z (transport (<i>helix (oneTurn l@i)) u) 
+corFib2 (u:Z) (l:loopS1) : Id Z (transport (<i>helix (oneTurn l@i)) u)
                                 (transport (<i>helix (loop1@i)) (transport (<i>helix (l@i)) u)) =
  <i>lemFib2 S1 helix base base l u base loop1@-i
 
-corFib3 (u:Z) (l:loopS1) : Id Z (transport (<i>helix (backTurn l@i)) u) 
+corFib3 (u:Z) (l:loopS1) : Id Z (transport (<i>helix (backTurn l@i)) u)
                                 (transport (<i>helix (loop1@-i)) (transport (<i>helix (l@i)) u)) =
  <i>lemFib2 S1 helix base base l u base (<j>loop1@-j)@-i
 
@@ -146,12 +146,12 @@ decodeEncodeBasePos : (n : nat) -> Id Z (transport (<x> helix (itLoop n @ x)) (i
   suc n ->  comp (<j>Id Z (transport (<i>helix (oneTurn l@i)) (inr zero)) (lemTransOneTurn n@j)) rem3 []
     where l : loopS1 = itLoop n
           rem1 : Id Z (transport (<i> helix (l@i)) (inr zero)) (inr n) = decodeEncodeBasePos n
-          rem2 : Id Z (transport (<i>helix (oneTurn l@i)) (inr zero)) 
-                      (transport (<i>helix (loop1@i)) (transport (<i>helix (l@i)) (inr zero))) = 
+          rem2 : Id Z (transport (<i>helix (oneTurn l@i)) (inr zero))
+                      (transport (<i>helix (loop1@i)) (transport (<i>helix (l@i)) (inr zero))) =
               corFib2 (inr zero) l
-          rem3 : Id Z (transport (<i>helix (oneTurn l@i)) (inr zero)) 
-                      (transport (<i>helix (loop1@i)) (inr n)) = 
-            comp (<j>Id Z (transport (<i>helix (oneTurn l@i)) (inr zero)) 
+          rem3 : Id Z (transport (<i>helix (oneTurn l@i)) (inr zero))
+                      (transport (<i>helix (loop1@i)) (inr n)) =
+            comp (<j>Id Z (transport (<i>helix (oneTurn l@i)) (inr zero))
                           (transport (<i>helix (loop1@i)) (rem1@j))) rem2 []
 
 decodeEncodeBaseNeg : (n : nat) -> Id Z (transport (<x> helix (itLoopNeg n @ x)) (inr zero)) (inl n) = split
@@ -159,19 +159,19 @@ decodeEncodeBaseNeg : (n : nat) -> Id Z (transport (<x> helix (itLoopNeg n @ x))
   suc n ->  comp (<j>Id Z (transport (<i>helix (backTurn l@i)) (inr zero)) (lemTransBackTurn n@j)) rem3 []
     where l : loopS1 = itLoopNeg n
           rem1 : Id Z (transport (<i> helix (l@i)) (inr zero)) (inl n) = decodeEncodeBaseNeg n
-          rem2 : Id Z (transport (<i>helix (backTurn l@i)) (inr zero)) 
-                      (transport (<i>helix (loop1@-i)) (transport (<i>helix (l@i)) (inr zero))) = 
+          rem2 : Id Z (transport (<i>helix (backTurn l@i)) (inr zero))
+                      (transport (<i>helix (loop1@-i)) (transport (<i>helix (l@i)) (inr zero))) =
               corFib3 (inr zero) l
-          rem3 : Id Z (transport (<i>helix (backTurn l@i)) (inr zero)) 
-                      (transport (<i>helix (loop1@-i)) (inl n)) = 
-            comp (<j>Id Z (transport (<i>helix (backTurn l@i)) (inr zero)) 
+          rem3 : Id Z (transport (<i>helix (backTurn l@i)) (inr zero))
+                      (transport (<i>helix (loop1@-i)) (inl n)) =
+            comp (<j>Id Z (transport (<i>helix (backTurn l@i)) (inr zero))
                           (transport (<i>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)
         = <j> 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) = <i> 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 (<i>Id (Id S1 base base) (refl S1 base) (<j>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) = <i>\ (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 = <i> comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base]
+lemInvS1 : Id S1 (invS1 base) base = <i> 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 (<i>Id S1 (lem@i) (lem@i)) l
+rePar (l: loopInvS1) : loopS1 = transport (<i>Id S1 (lemInvS1@i) (lemInvS1@i)) l
 
 test2 : Z = winding (rePar (<i>invS1 (loop2@i)))
 -- EVAL: inl (suc zero)                Time: 1m26.400s

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 24a5c53f324d264a75693f5d9df8d2a73a9ea7b1..9c44d9a7b78dd49d83c946d4528f60d663cc3a85 100644 (file)
--- 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 (<i> p@i -> p
           pS : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = w.2\r
           pASet  : IdP (<i> set (p@i)) ASet BSet\r
                  = lemIdPProp (set A) (set B) (setIsProp A) (<i> set (p@i)) ASet BSet\r
-          opaque pASet\r
           pNE   : IdP (<i> ishinh_UU (p@i)) a b\r
                 = lemIdPProp (ishinh_UU A) (ishinh_UU B) (propishinh A) (<i> ishinh_UU (p@i)) a b\r
-          opaque pNE\r
           pShift : IdP (<i> equiv (p@i) (p@i)) AShift BShift =\r
             <i> ( pS @ i\r
                 , (lemIdPProp\r
@@ -413,7 +411,6 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p
                     (\(x : A) -> propIsEquiv Z A (action A AShift x)))\r
                     (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x))\r
                    AEquiv BEquiv\r
-          opaque pEquiv\r
           hole : Id BZ BA BB = <i> (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i))))\r
       G (q : Id BZ BA BB) : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = (<i> BZSet (q @ i), <i> (BZShift (q@i)).1)\r
       GF (w : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB))\r
@@ -426,10 +423,8 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p
           q2 : Id BZ BA BB = F (p, p2)\r
           pASet  : Id (IdP (<i> set (p@i)) ASet BSet) (<i> BZASet (q2@i)) (<i> BZASet (q@i))\r
                  = lemIdPSet (set A) (set B) (propSet (set A) (setIsProp A)) (<i> set (p@i)) ASet BSet (<i> BZASet (q2@i)) (<i> BZASet (q@i))\r
-          opaque pASet\r
           pNE    : Id (IdP (<i> ishinh_UU (p@i)) a b) (<i> BZNE (q2@i)) (<i> BZNE (q@i))\r
                  = lemIdPSet (ishinh_UU A) (ishinh_UU B) (propSet (ishinh_UU A) (propishinh A)) (<i> ishinh_UU (p@i)) a b (<i> BZNE (q2@i)) (<i> BZNE (q@i))\r
-          opaque pNE\r
           pShift : Id (IdP (<i> equiv (p@i) (p@i)) AShift BShift) (<i> BZShift (q2@i)) (<i> BZShift (q@i)) =\r
                  <j i> ( p2 @ i\r
                        , (lemIdPSet\r
@@ -440,7 +435,6 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p
                           AShift.2 BShift.2\r
                           (<i> (BZShift (q2@i)).2) (<i> (BZShift (q@i)).2)) @ j @ i\r
                        )\r
-          opaque pShift\r
           pEquiv : IdP (<j> IdP (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x)) AEquiv BEquiv) (<i> BZEquiv (q2@i)) (<i> BZEquiv (q@i))\r
                  = lemIdPSet2\r
                    ((x : A) -> isEquiv Z A (action A AShift x))\r
@@ -452,7 +446,6 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p
                    (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@1@i) x))\r
                    (<j i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x))\r
                    AEquiv BEquiv (<i> BZEquiv (q2@i)) (<i> BZEquiv (q@i))\r
-          opaque pEquiv\r
           hole : Id (Id BZ BA BB) q2 q = <j i> (p@i, (pASet@j@i, (pNE@j@i, (pShift@j@i, pEquiv@j@i))))\r
       hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB)\r
            = (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF)\r
@@ -580,29 +573,32 @@ invLoopZ : loopBZ = <i> loopZ @ -i
 \r
 encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport (<i> BZSet (p@i)) zeroZ\r
 \r
-decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> p @ -i, q)\r
-  where\r
-    p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a\r
-    p : Id U (BZSet A) Z = <i> (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i\r
-    hole1 (x : Z) : Id Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
-                    (p1 (BZS A (BZAction A a x))).1.1\r
-      = compId Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
-                 (transport p (BZS A (BZAction A a x)))\r
-                 (p1 (BZS A (BZAction A a x))).1.1\r
-                 (<i> transport p (BZS A (lem0 Z (BZSet A) (BZAction A a) p1 x @ i)))\r
-                 (lem1 Z (BZSet A) (BZAction A a) p1 (BZS A (BZAction A a x)))\r
-    opaque hole1\r
-    hole2 (x : Z) : Id Z (p1 (BZS A (BZAction A a x))).1.1 (sucZ x)\r
-      = compId Z (p1 (BZS A (BZAction A a x))).1.1 (p1 (BZAction A a (sucZ x))).1.1 (sucZ x)\r
-        (<i> (p1 (lem2 (BZSet A) (BZShift A) a x @ i)).1.1)\r
-        (secEq Z (BZSet A) (BZAction A a, p1) (sucZ x))\r
-    opaque hole2\r
-    hole : Id (Z->Z) (\(x : Z) -> transport p (BZS A (transport (<i> p @ -i) x))) sucZ\r
-      = <i> \(x : Z) -> compId Z (transport p (BZS A (transport (<i> p @ -i) x))) (p1 (BZS A (BZAction A a x))).1.1 (sucZ x) (hole1 x) (hole2 x) @ i\r
-    opaque hole\r
-    q : IdP (<i> (p@-i) -> (p@-i)) sucZ (BZS A)\r
-      = <i> substIdP (BZSet A -> BZSet A) (Z -> Z) (<i> (p@i) -> (p@i)) (BZS A) sucZ hole @ -i\r
-    opaque q\r
+decodeZP (A : BZ) (a : BZSet A) : Id U (BZSet A) Z = <i> (univalence (BZSet A) Z (BZAction A a, BZEquiv A a)).1.1 @ -i\r
+\r
+decodeZ1 (A : BZ) (a : BZSet A) (x : Z) : Id Z (transport (decodeZP A a) (BZS A (transport (<i> (decodeZP A a) @ -i) x)))\r
+                   (BZEquiv A a (BZS A (BZAction A a x))).1.1\r
+      = compId Z (transport (decodeZP A a) (BZS A (transport (<i> (decodeZP A a) @ -i) x)))\r
+                 (transport (decodeZP A a) (BZS A (BZAction A a x)))\r
+                 (BZEquiv A a (BZS A (BZAction A a x))).1.1\r
+                 (<i> transport (decodeZP A a) (BZS A (lem0 Z (BZSet A) (BZAction A a) (BZEquiv A a) x @ i)))\r
+                 (lem1 Z (BZSet A) (BZAction A a) (BZEquiv A a) (BZS A (BZAction A a x)))\r
+opaque decodeZ1\r
+\r
+decodeZ2 (A : BZ) (a : BZSet A) (x : Z) : Id Z (BZEquiv A a (BZS A (BZAction A a x))).1.1 (sucZ x)\r
+      = 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)\r
+        (<i> (BZEquiv A a (lem2 (BZSet A) (BZShift A) a x @ i)).1.1)\r
+        (secEq Z (BZSet A) (BZAction A a, BZEquiv A a) (sucZ x))\r
+opaque decodeZ2\r
+\r
+decodeZ3 (A : BZ) (a : BZSet A) : Id (Z->Z) (\(x : Z) -> transport (decodeZP A a) (BZS A (transport (<i> (decodeZP A a) @ -i) x))) sucZ\r
+         = <i> \(x : Z) -> compId Z (transport (decodeZP A a) (BZS A (transport (<i> (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\r
+opaque decodeZ3\r
+\r
+decodeZQ (A : BZ) (a : BZSet A) : IdP (<i> ((decodeZP A a)@-i) -> ((decodeZP A a)@-i)) sucZ (BZS A)\r
+         = <i> substIdP (BZSet A -> BZSet A) (Z -> Z) (<i> ((decodeZP A a)@i) -> ((decodeZP A a)@i)) (BZS A) sucZ (decodeZ3 A a) @ -i\r
+opaque decodeZQ\r
+\r
+decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> decodeZP A a @ -i, decodeZQ A a)\r
 \r
 prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = hole\r
         where\r
@@ -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))\r
 opaque GF\r
 \r
+F_fullyFaithful0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
+                 = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base)\r
+opaque F_fullyFaithful0\r
+\r
+\r
 F_fullyFaithful : (x y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)\r
   = lemPropFib (\(x : S1) -> (y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
                (\(x : S1) -> propPi S1 (\(y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
@@ -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))\r
                 hole)\r
   where\r
-    hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
-         = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base)\r
-    opaque hole0\r
     hole : isEquiv loopS1 loopBZ (mapOnPath S1 BZ F base base)\r
-         = transport (<i> isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2\r
-    opaque hole\r
+         = transport (<i> isEquiv loopS1 loopBZ (F_fullyFaithful0 @ -i)) loopS1equalsLoopBZ'.2\r
 opaque F_fullyFaithful\r
 \r
 F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole\r
@@ -752,7 +749,14 @@ S1equalsBZ : Id U S1 BZ = hole
   where\r
     G (y : BZ) : S1 = (F_essentiallySurjective y).1\r
     FG (y : BZ) : Id BZ (F (G y)) y = <i> (F_essentiallySurjective y).2 @ -i\r
-    opaque FG\r
     GF (x : S1) : Id S1 (G (F x)) x = (F_fullyFaithful (G (F x)) x (FG (F x))).1.1\r
-    opaque GF\r
-    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\r
+\r
+invBZ : BZ -> BZ = transport (<i> S1equalsBZ@i -> S1equalsBZ@i) invS1\r
+doubleLoopBZ : loopBZ -> loopBZ = transport (<i> loopS1equalsLoopBZ@i -> loopS1equalsLoopBZ@i) doubleLoop\r
+\r
+-- > transport (<i> BZSet (doubleLoopBZ loopZ @ i)) zeroZ\r
+-- EVAL: inr (suc (suc zero))\r
+-- Time: 0m25.191s\r
+\r
+-- visible_all\r