wip

diff --git a/examples/quotient.ctt b/examples/quotient.ctt
index e2e4b475c1d9c225fcdd81b9695fdff1651c6cdc..3480eac5bc68a1a49e8afdbe6c8503e31b4f826d 100644 (file)
--- a/examples/quotient.ctt
+++ b/examples/quotient.ctt
@@ -25,10 +25,9 @@ f2 : S1 -> s1quot = split
   base -> inj tt
   loop @ i -> quoteq{s1quot} tt tt tt @ i
 
-rem3 : (a : Unit) -> Id s1quot (f2 (f1 (inj a))) (inj a) = split
+rem3 : (a : Unit) -> Id s1quot (inj tt) (inj a) = split
    tt -> <i> inj tt
 
-
 test : Id U s1quot S1 =
   isoId s1quot S1 f1 f2 rem1 rem2
     where
@@ -38,22 +37,6 @@ test : Id U s1quot S1 =
     rem2 : (x : s1quot) -> Id s1quot (f2 (f1 x)) x = split
       inj a -> rem3 a
       quoteq a b r @ i -> ?
-        -- rem4 : (a b : Unit) (r : RS1 a b)->
-        --        Id s1quot (quoteq{s1quot} tt tt tt @ i)
-        --                  (quoteq{s1quot} a b r @ i) = split
-        --   tt -> \(b : Unit) (r : RS1 a b) -> rem5 b r
-        --    where
-        --    rem5 : (b r : Unit) ->
-        --           Id s1quot (quoteq{s1quot} tt tt tt @ i)
-        --                     (quoteq{s1quot} tt b r @ i) = split
-        --      tt -> \(r : Unit) -> rem6 r
-        --       where
-        --       rem6 : (r : Unit) ->
-        --               Id s1quot (quoteq{s1quot} tt tt tt @ i)
-        --                         (quoteq{s1quot} tt tt r @ i) = split
-        --         tt -> ? -- <i> rem3 tt @ i
-
-
 
 
 -- Set quotient of A by R