{- Quotient Type: Copyright (c) Groupoid Infinity, 2016-2020. HoTT 6.10 Quotients -} module quotient where import set -- Quotient A by R data quot (A: U) (R: A -> A -> U) = quotient (a: A) | identification (a b: A) (r: R a b) [ (i = 0) -> quotient a , (i = 1) -> quotient b ] -- Set quotient of A by R data setQuot (A: U) (R: A -> A -> U) = quotient (a: A) | identification (a b: A) (r: R a b) [ (i=0) -> quotient a, (i=1) -> quotient b ] | trunc (a b : setQuot A R) (p q : Path (setQuot A R) a b) [ (i = 0) -> p @ j , (i = 1) -> q @ j , (j = 0) -> a , (j = 1) -> b ] -- Groupoid quotient of A by R data grpdQuot (A: U) (R: A -> A -> U) = quotient (a: A) | identification (a b: A) (r: R a b) [ (i = 0) -> quotient a, (i = 1) -> quotient b ] | trunc (a b : grpdQuot A R) (p q : Path (grpdQuot A R) a b) (x y: Path (Path (grpdQuot A R) a b) p q) [ (i = 0) -> x @ j @ k , (i = 1) -> y @ j @ k , (j = 0) -> p @ k , (j = 1) -> q @ k , (k = 0) -> a , (k = 1) -> b ] quotId (A: U) (R: A -> A -> U) (a b: A) (r: R a b) : Path (quot A R) (quotient a) (quotient b) = identification {quot A R} a b r @ i setQuotId (A : U) (R : A -> A -> U) (a b : A) (r : R a b) : Path (setQuot A R) (quotient a) (quotient b) = identification {setQuot A R} a b r @ i setQuotIsSet (A : U) (R : A -> A -> U) : isSet (setQuot A R) = \(a b : setQuot A R) (p q : Path (setQuot A R) a b) -> trunc {setQuot A R} a b p q @ i @ j setQuotLift (A B : U) (R : A -> A -> U) (H : isSet B) (f : A -> B) (G : (a b : A) -> R a b -> Path B (f a) (f b)) : setQuot A R -> B = split quotient x -> f x identification a b r @ i -> G a b r @ i trunc a b p q @ i j -> H (lift a) (lift b) ( lift (p @ k)) ( lift (q @ k)) @ i @ j where lift : setQuot A R -> B = setQuotLift A B R H f G lemPropF (A : U) (B : A -> U) (h : (x : A) -> isProp (B x)) (x y : A) (p : Path A x y) (u : B x) (v : B y) : PathP ( B (p @ i)) u v = substPathP (B x) (B y) ( B (p @ i)) u v q where u' : B y = transport ( B (p @ i)) u q : Path (B y) u' v = h y u' v setQuotLem (A : U) (P : A -> U) (sP : (x : A) -> isSet (P x)) (a : A) : (b : A) (p q : Path A a b) (r : Path (Path A a b) p q) (a1 : P a) (b1 : P b) (p1 : PathP ( P (p @ i)) a1 b1) (q1 : PathP ( P (q @ i)) a1 b1) -> PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1 = J A a (\(b : A) (p : Path A a b) -> (q : Path A a b) (r : Path (Path A a b) p q) (a1 : P a) (b1 : P b) (p1 : PathP ( P (p @ i)) a1 b1) (q1 : PathP (P (q @ i)) a1 b1) -> PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1) rem where rem : (q : Path A a a) (r : Path (Path A a a) (refl A a) q) (a1 b1 : P a) (p1 : Path (P a) a1 b1) (q1 : PathP ( P (q @ i)) a1 b1) -> PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1 = J (Path A a a) (refl A a) (\(q : Path A a a) (r : Path (Path A a a) (refl A a) q) -> (a1 b1 : P a) (p1 : Path (P a) a1 b1) (q1 : PathP ( P (q @ i)) a1 b1) -> PathP ( PathP ( P (r @ i @ j)) a1 b1) p1 q1) (sP a) setQuotElim (A : U) (R : A -> A -> U) (B : setQuot A R -> U) (sB : (x : setQuot A R) -> isSet (B x)) (f : (x : A) -> B (quotient x)) (g : (a b : A) (r : R a b) -> PathP ( B (setQuotId A R a b r @ i)) (f a) (f b)) : (x : setQuot A R) -> B x = split quotient a -> f a identification a b r @ i -> g a b r @ i trunc a b p q @ i j -> setQuotLem (setQuot A R) B sB a b p q ( trunc{setQuot A R} a b p q @ i @ j) (f' a) (f' b) ( f' (p @ k)) ( f' (q @ k)) @ i @ j where f' : (z : setQuot A R) -> B z = setQuotElim A R B sB f g setQuotIndProp (A : U) (R : A -> A -> U) (B : setQuot A R -> U) (f : (x : A) -> B (quotient x)) (g : (x : setQuot A R) -> isProp (B x)) : (x : setQuot A R) -> B x = setQuotElim A R B (\(x : setQuot A R) -> propSet (B x) (g x)) f (\(a b : A) (r : R a b) -> lemPropF (setQuot A R) B g (quotient a) (quotient b) (setQuotId A R a b r) (f a) (f b)) setQuotLift2 (A B C : U) (X : A -> A -> U) (Y : B -> B -> U) (reflA : (a : A) -> X a a) (reflB : (b : B) -> Y b b) (h : isSet C) (f : A -> B -> C) (p : (a1 b1 : A) (a2 b2 : B) -> X a1 b1 -> Y a2 b2 -> Path C (f a1 a2) (f b1 b2)) : setQuot A X -> setQuot B Y -> C = setQuotLift A (setQuot B Y -> C) X (setPi (setQuot B Y) (\(_ : setQuot B Y) -> C) (\(_ : setQuot B Y) -> h)) lift (\(a1 b1 : A) (r : X a1 b1) -> funext (setQuot B Y) C (lift a1) (lift b1) (setQuotIndProp B Y (\(x : setQuot B Y) -> Path C (lift a1 x) (lift b1 x)) (\(x : B) -> p a1 b1 x x r (reflB x)) (\(x : setQuot B Y) -> h (lift a1 x) (lift b1 x)))) where lift (a : A) : setQuot B Y -> C = setQuotLift B C Y h (f a) (\(a2 b2 : B) (r : Y a2 b2) -> p a a a2 b2 (reflA a) r) {- -- Test to define circle as a quotient of unit import s1 import quotient RS1 (a b: unit): U = unit s1quot : U = quot unit RS1 f1: s1quot -> S1 = split quotient _ -> base identification a b r @ i -> loop1 @ i f2: S1 -> s1quot = split base -> quotient tt loop @ i -> identification {s1quot} tt tt tt @ i rem: (a: unit) -> Path s1quot (quotient tt) (quotient a) = split tt -> quotient tt -}