From: Thierry Coquand <coquand@dhcp-179211.eduroam.chalmers.se>
Date: Wed, 27 Apr 2016 09:27:47 +0000 (+0200)
Subject: small change
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e11e54d35289b35739b20346428c3104a90ff49d;p=cubicaltt.git

small change
---

diff --git a/examples/subset.ctt b/examples/subset.ctt
index 8845828..ddded4f 100644
--- a/examples/subset.ctt
+++ b/examples/subset.ctt
@@ -75,7 +75,6 @@ subset10 (A : U) (sA : set A)
 subsetIso0 (A : U) (sA : set A) : (s0 : subset0 A sA) ->
       Id (subset0 A sA) (subset10 A sA (subset01 A sA s0)) s0
   = \ (s0 : subset0 A sA) -> let
---    TEMP : Id (subset0 A sA) (subset10 A sA (subset01 A sA s0)) s0 = undefined
     s0'
       : subset0 A sA
       = subset10 A sA (subset01 A sA s0)
@@ -114,7 +113,7 @@ 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
+--      = lemPropF U set setIsProp B' B idB sB' sB
       = undefined
     -- 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