{- Quotient Type:
   Copyright (c) Groupoid Infinity, 2014-2018.

   HoTT 6.10 Quotients -}

module quotient where
import s1
import set

-- Quotient A by R
data quot (A: U) (R: A -> A -> U)
   = inj (a: A)
   | quoteq (a b: A) (r: R a b)
      <i> [ (i=0) -> inj a,
            (i=1) -> inj 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 ]

quoteq' (A: U) (R: A -> A -> U) (a b: A) (r: R a b)
  : Path (quot A R) (inj a) (inj b) = <i> 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

rem: (a: unit) -> Path s1quot (inj tt) (inj a) = split
   tt -> <i> inj tt

identsetquot (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