From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 7 Jul 2016 12:06:08 +0000 (+0200)
Subject: make subset compile using opaque
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=05170941ab091494f02692ab69a0d5204bd2881b;p=cubicaltt.git

make subset compile using opaque
---

diff --git a/examples/injective.ctt b/examples/injective.ctt
index 631051c..5721337 100644
--- a/examples/injective.ctt
+++ b/examples/injective.ctt
@@ -1,9 +1,7 @@
 module injective where
 
-import prelude
 import prop
 
-
 -- First definition of injectivity, informally: if two elements f a0, f a1 are
 -- equal in B, then a0, a1 must be equal in A.
 inj0 (A B : U) (f : A -> B) (sA : set A) (sB : set B) : U
diff --git a/examples/pi.ctt b/examples/pi.ctt
index 1c957b1..0a92598 100644
--- a/examples/pi.ctt
+++ b/examples/pi.ctt
@@ -1,6 +1,5 @@
 module pi where
 
-import prelude
 import equiv
 
               -----------------------------------
diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index 51f1534..1f101b6 100644
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -1,6 +1,5 @@
 module sigma where
 
-import prelude
 import equiv
 
 lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) :
diff --git a/examples/subset.ctt b/examples/subset.ctt
index ddded4f..694f537 100644
--- a/examples/subset.ctt
+++ b/examples/subset.ctt
@@ -1,11 +1,9 @@
 module subset where
 
-import prelude
 import injective
 import sigma
 import univalence
 
-
 -- The first definition of a subset. Informally, there exists a second set B
 -- and an injective function from B to A.
 subset0 (A : U) (sA : set A) : U
@@ -36,6 +34,9 @@ subset01 (A : U) (sA : set A) : subset0 A sA -> subset1 A sA
   in
     (X, pX)
 
+lem (A:U) (P:A->U) (pP:(x:A) -> prop (P x)) (u v:(x:A) * P x) (p:Id A u.1 v.1) :
+ Id ((x:A)*P x) u v = <i>(p@i,(lemPropF A P pP u.1 v.1 p u.2 v.2)@i)
+
 -- A map from the second to the first definition of subsets.
 subset10 (A : U) (sA : set A)
   : subset1 A sA -> subset0 A sA
@@ -71,6 +72,9 @@ subset10 (A : U) (sA : set A)
   in
     (B, sB, f, inj)
 
+opaque lemPropF
+opaque subst
+
 -- Show that subset10 ∘ subset01 can be identified with the identity function
 subsetIso0 (A : U) (sA : set A) : (s0 : subset0 A sA) ->
       Id (subset0 A sA) (subset10 A sA (subset01 A sA s0)) s0
@@ -113,25 +117,20 @@ subsetIso0 (A : U) (sA : set A) : (s0 : subset0 A sA) ->
       = q.1
     -- Show that sB can be identified with sB'
     idsB : IdP (<i> set (idB @ i)) sB' sB
---      = lemPropF U set setIsProp B' B idB sB' sB
-      = undefined
+      = lemPropF U set setIsProp B' B idB sB' sB
     -- Show that f' can be identified with f. This follows from g∘g' ⇔ \x -> x
     -- and that there is a path q.2 between f'∘g∘g' and f
     idf : IdP (<i> idB @ i -> A) f' f
       = let
-        TEMP : IdP (<i> idB @ i -> A) f' f = undefined
         Q (h : B' -> B') : U
           = IdP (<i> q.1 @ i -> A) (\ (x : B') -> f' (h x)) f
         a : B' -> B' = \ (x : B') -> g (g' x)
         b : B' -> B' = \ (x : B') -> x
         p : Id (B' -> B') a b = <i> \ (x : B') -> (t x) @ i
-      in
-        -- subst (B' -> B') Q a b p q.2
-        TEMP
+      in subst (B' -> B') Q a b p q.2
     -- Show that inj can be identified with inj'
     idinj : IdP (<i> inj1 (idB @ i) A (idf @ i) (idsB @ i) sA) inj' inj
       = let
-        TEMP : IdP (<i> inj1 (idB @ i) A (idf @ i) (idsB @ i) sA) inj' inj = undefined
         T : U
           = (X : U) * (_ : X -> A) * (set X)
         P : T -> U
@@ -144,12 +143,9 @@ subsetIso0 (A : U) (sA : set A) : (s0 : subset0 A sA) ->
           = (B, f, sB)
         idT : Id T t0 t1
           = <i> (idB @ i, idf @ i, idsB @ i)
-      in
-        -- lemPropF T P pP t0 t1 idT inj' inj
-        TEMP
+      in lemPropF T P pP t0 t1 idT inj' inj
   in
     <i> (idB @ i, idsB @ i, idf @ i, idinj @ i)
-    -- TEMP
 
 -- Show that subset10 ∘ subset01 can be identified with the identity function
 subsetIso1 (A : U) (sA : set A) : (s1 : subset1 A sA) ->