From: Anders Mörtberg Date: Tue, 5 Jul 2016 11:41:10 +0000 (+0200) Subject: wip on an equivalent presentation of the circle as a quotient of unit X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a59bd33e0fba452870fc91b01990b79ce538191d;p=cubicaltt.git wip on an equivalent presentation of the circle as a quotient of unit --- diff --git a/examples/quotient.ctt b/examples/quotient.ctt index 9a172c0..e2e4b47 100644 --- a/examples/quotient.ctt +++ b/examples/quotient.ctt @@ -1,20 +1,81 @@ module quotient where import prelude +import circle -- Quotient A by R data Quot (A : U) (R : A -> A -> U) = + inj (a : A) + | quoteq (a b : A) (r : R a b) + [ (i = 0) -> inj a, (i = 1) -> inj b ] + +quoteq' (A : U) (R : A -> A -> U) (a b : A) (r : R a b) + : Id (Quot A R) (inj a) (inj b) = quoteq {Quot A R} a b r @ i + + +-- Test to define circle as a quotient of unit +RS1 (a b : Unit) : U = Unit +s1quot : U = Quot Unit RS1 + +f1 : s1quot -> S1 = split + inj _ -> base + quoteq a b r @ i -> loop1 @ i + +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 + tt -> inj tt + + +test : Id U s1quot S1 = + isoId s1quot S1 f1 f2 rem1 rem2 + where + rem1 : (y : S1) -> Id S1 (f1 (f2 y)) y = split + base -> base + loop @ i -> loop1 @ i + 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 +data setquot (A : U) (R : A -> A -> U) = quot (a : A) | identification (a b : A) (r : R a b) [ (i = 0) -> quot a, (i = 1) -> quot b ] - | setTruncation (a b : Quot A R) (p q : Id (Quot A R) a b) + | setTruncation (a b : setquot A R) (p q : Id (setquot A R) a b) [ (i = 0) -> p @ j , (i = 1) -> q @ j , (j = 0) -> a , (j = 1) -> b ] -identQuot (A : U) (R : A -> A -> U) (a b : A) (r : R a b) - : Id (Quot A R) (quot a) (quot b) = identification {Quot A R} a b r @ i -setQuot (A : U) (R : A -> A -> U) : set (Quot A R) = - \(a b : Quot A R) (p q : Id (Quot A R) a b) -> - setTruncation {Quot A R} a b p q @ i @ j +{- + b + p q + a +-} + +identsetquot (A : U) (R : A -> A -> U) (a b : A) (r : R a b) + : Id (setquot A R) (quot a) (quot b) = identification {setquot A R} a b r @ i + +setsetquot (A : U) (R : A -> A -> U) : set (setquot A R) = + \(a b : setquot A R) (p q : Id (setquot A R) a b) -> + setTruncation {setquot A R} a b p q @ i @ j