{- 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> [ (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> [ (i=0) -> quotient a, (i=1) -> quotient b ]
   | trunc (a b : setQuot A R) (p q : Path (setQuot A R) a b)
     <i j> [ (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> [ (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 j k> [ (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)
  = <i> 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)
  = <i> 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) ->
    <i j> 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) (<k> lift (p @ k)) (<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 (<i> B (p @ i)) u v
  = substPathP (B x) (B y) (<i> B (p @ i)) u v q
  where
    u' : B y = transport (<i> 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 (<i> P (p @ i)) a1 b1) (q1 : PathP (<i> P (q @ i)) a1 b1) ->
           PathP (<i> PathP (<j> 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 (<i> P (p @ i)) a1 b1) (q1 : PathP (<i>P (q @ i)) a1 b1) ->
          PathP (<i> PathP (<j> 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 (<i> P (q @ i)) a1 b1) ->
      PathP (<i> PathP (<j> 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 (<i> P (q @ i)) a1 b1) ->
          PathP (<i> PathP (<j> 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 (<i> 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
               (<i j> trunc{setQuot A R} a b p q @ i @ j)
               (f' a) (f' b) (<k> f' (p @ k)) (<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 -> <i> quotient tt
-}