From: Anders Mörtberg Date: Tue, 5 Jul 2016 11:57:49 +0000 (+0200) Subject: wip X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7840f7691e49ae3c65f840f1817bd24461c1159c;p=cubicaltt.git wip --- diff --git a/examples/quotient.ctt b/examples/quotient.ctt index e2e4b47..3480eac 100644 --- 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 -> 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 -> ? -- rem3 tt @ i - - -- Set quotient of A by R