eval ignores opaqueness

Proof of BZ = (X : (A:U) * (A->A)) * inh (X = (Z, sucZ))

diff --git a/CTT.hs b/CTT.hs
index 8bd2f35eb8164e730079463d2f4db9e9af71d570..d47df49d7bac51bb7bf5e3281c4136058871525d 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -240,6 +240,12 @@ def (OpaqueDecl n) (rho,vs,fs,Nameless os) = (rho,vs,fs,Nameless (Set.insert n o
 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)
 
+defWhere :: Decls -> Env -> Env
+defWhere (MutualDecls ds) (rho,vs,fs,Nameless os) = (Def ds rho,vs,fs,Nameless (os Set.\\ Set.fromList (declIdents ds)))
+defWhere (OpaqueDecl _) rho = rho
+defWhere (VisibleDecl _) rho = rho
+defWhere VisibleAllDecl rho = rho
+
 sub :: (Name,Formula) -> Env -> Env
 sub (i,phi) (rho,vs,fs,os) = (Sub i rho,vs,phi:fs,os)
 

diff --git a/Eval.hs b/Eval.hs
index 9a651bc2c5fbb1726c82afc28837b3571b3e7cb1..ef330da74dfe52b267c2bd6d3eeb318ed65a2372 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -157,7 +157,7 @@ eval rho@(_,_,_,Nameless os) v = case v of
   Pair a b            -> VPair (eval rho a) (eval rho b)
   Fst a               -> fstVal (eval rho a)
   Snd a               -> sndVal (eval rho a)
-  Where t decls       -> eval (def decls rho) t
+  Where t decls       -> eval (defWhere decls rho) t
   Con name ts         -> VCon name (map (eval rho) ts)
   PCon name a ts phis  ->
     pcon name (eval rho a) (map (eval rho) ts) (map (evalFormula rho) phis)

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 9c44d9a7b78dd49d83c946d4528f60d663cc3a85..3581c3723befe7cc65c3747407c80dca1dc542da 100644 (file)
--- a/examples/torsor.ctt
+++ b/examples/torsor.ctt
@@ -598,6 +598,38 @@ decodeZQ (A : BZ) (a : BZSet A) : IdP (<i> ((decodeZP A a)@-i) -> ((decodeZP A a
          = <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
+\r
+AA : U = (X : U) * (X -> X)\r
+BZ' : U = (X : AA) * ishinh_UU (Id AA X (Z, sucZ))\r
+BZequivBZ' : Id U BZ BZ' = isoId BZ BZ' F G FG GF\r
+  where\r
+    F (A : BZ) : BZ' = ((BZSet A, BZS A), BZNE A (ishinh (Id AA (BZSet A, BZS A) (Z, sucZ)))\r
+                        (\(a : BZSet A) -> hinhpr (Id AA (BZSet A, BZS A) (Z, sucZ)) (<i> (decodeZP A a @ i, decodeZQ A a @ -i))))\r
+    G (A : BZ') : BZ = (A.1.1,\r
+                       (A.2 (set A.1.1, setIsProp A.1.1) (\(a : Id AA A.1 (Z, sucZ)) -> transport (<i> set (a @ -i).1) ZSet),\r
+                       (A.2 (ishinh A.1.1) (\(a : Id AA A.1 (Z, sucZ)) -> hinhpr A.1.1 (transport (<i> (a @ -i).1) zeroZ)),\r
+                       ((A.1.2, SHIFT), EQUIV))))\r
+                       where\r
+                         SHIFT : isEquiv A.1.1 A.1.1 A.1.2\r
+                               = A.2 (isEquiv A.1.1 A.1.1 A.1.2, propIsEquiv A.1.1 A.1.1 A.1.2)\r
+                                 (\(a : Id AA A.1 (Z, sucZ)) -> transport (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ))\r
+                         ZEquiv : (x : Z) -> isEquiv Z Z (action Z (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) x) = BZEquiv ZBZ\r
+                         hole (a : Id AA A.1 (Z, sucZ))\r
+                             : IdP (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ) SHIFT\r
+                             = lemIdPProp (isEquiv Z Z sucZ) (isEquiv A.1.1 A.1.1 A.1.2) (propIsEquiv Z Z sucZ)\r
+                               (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ) SHIFT\r
+                         ZEquivEq (a : Id AA A.1 (Z, sucZ))\r
+                             : Id U ((x : Z) -> isEquiv Z Z (action Z (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) x))\r
+                                    ((x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x))\r
+                             = <i> (x : (a@-i).1) -> isEquiv Z (a@-i).1 (action (a@-i).1 ((a@-i).2, hole a @ i) x)\r
+                         EQUIV : (x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x)\r
+                               = A.2 ((x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x)\r
+                                     , propPi A.1.1 (\(x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x))\r
+                                       (\(x : A.1.1) -> propIsEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x)))\r
+                                     (\(a : Id AA A.1 (Z, sucZ)) -> transport (ZEquivEq a) ZEquiv)\r
+    FG (A : BZ') : Id BZ' (F (G A)) A = <i> ((A.1.1, A.1.2), propishinh (Id AA (A.1.1, A.1.2) (Z, sucZ)) (F (G A)).2 A.2 @ i)\r
+    GF (A : BZ) : Id BZ (G (F A)) A = (lemBZ (G (F A)) A).1 (<_> BZSet A, <_> BZS A)\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