setquot.ctt

-- Formalization of (impredicative) set quotients
module setquot where

import bool
import sigma
import pi
import univalence

subtypeEquality (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))
                (s t : (x : A) * B x) : Path A s.1 t.1 -> Path (Sigma A B) s t =
  trans (Path A s.1 t.1) (Path (Sigma A B) s t) rem
    where
    rem : Path U (Path A s.1 t.1) (Path (Sigma A B) s t) =
      <i> lemSigProp A B pB s t @ -i

-- (* Propositions *)

hProp : U = (X : U) * prop X

ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1)

propishinh (X : U) : prop (ishinh_UU X) =
  propPi hProp (\(P : hProp) -> ((X -> P.1) -> P.1)) rem1
  where
   rem1 (P : hProp) : prop ((X -> P.1) -> P.1) =
     propPi (X -> P.1) (\(_ : X -> P.1) -> P.1) (\(f : X -> P.1) -> P.2)

ishinh (X : U) : hProp = (ishinh_UU X,propishinh X)

hinhpr (X : U) : X -> (ishinh X).1 =
  \(x : X) (P : hProp) (f : X -> P.1) -> f x

hinhuniv (X : U) (P : hProp) (f : X -> P.1) (inhX : (ishinh X).1) : P.1 =
  inhX P f

hdisj (P Q : U) : hProp = ishinh (or P Q)

hdisj_in1 (P Q : U) (X : P) : (hdisj P Q).1 = hinhpr (or P Q) (inl X)
hdisj_in2 (P Q : U) (X : Q) : (hdisj P Q).1 = hinhpr (or P Q) (inr X)

-- Direct proof that logical equivalence is equiv for props
isEquivprop (A B : U) (f : A -> B) (g : B -> A) (pA : prop A) (pB : prop B) : isEquiv A B f = rem
  where
  rem (y : B) : isContr (fiber A B f y) = (s,t)
    where
    s : fiber A B f y = (g y,pB y (f (g y)))
    t (w : fiber A B f y) : Path ((x :  A) * Path B y (f x)) s w =
      subtypeEquality A (\(x : A) -> Path B y (f x)) pb s w r1
       where
       pb (x : A) : (a b : Path B y (f x)) -> Path (Path B y (f x)) a b = propSet B pB y (f x)
       r1 : Path A s.1 w.1 = pA s.1 w.1

equivhProp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : equiv P.1 P'.1 =
  (f,isEquivprop P.1 P'.1 f g P.2 P'.2)

-- Proof of uahp using full univalence
uahp' (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Path hProp P P' =
  subtypeEquality U prop propIsProp P P' rem
  where
  rem : Path U P.1 P'.1 = transport (<i> corrUniv P.1 P'.1 @ -i) (equivhProp P P' f g)

-- Direct proof of uahp
uahp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Path hProp P P' =
  subtypeEquality U prop propIsProp P P' rem
  where
  rem : Path U P.1 P'.1 = isoPath P.1 P'.1 f g s t
    where s (y : P'.1) : Path P'.1 (f (g y)) y = P'.2 (f (g y)) y
          t (x : P.1) : Path P.1 (g (f x)) x = P.2 (g (f x)) x

-- A short proof that hProp form a set using univalence: (this is not needed!)

propequiv (X Y : U) (H : prop Y) (f g : equiv X Y) : Path (equiv X Y) f g =
  equivLemma X Y f g (<i> \(x : X) -> H (f.1 x) (g.1 x) @ i)

propidU (X Y : U) : Path U X Y -> prop Y -> prop X = substInv U prop X Y

sethProp (P P' : hProp) : prop (Path hProp P P') =
  propidU (Path hProp P P') (equiv P.1 P'.1) rem (propequiv P.1 P'.1 P'.2)
  where
   rem1 : Path U (Path hProp P P') (Path U P.1 P'.1) = lemSigProp U prop propIsProp P P'
   rem2 : Path U (Path U P.1 P'.1) (equiv P.1 P'.1) = corrUniv P.1 P'.1
   rem : Path U (Path hProp P P') (equiv P.1 P'.1) =
     compPath U (Path hProp P P') (Path U P.1 P'.1) (equiv P.1 P'.1) rem1 rem2

-- (* Sets *)

hsubtypes (X : U) : U = X -> hProp

carrier (X : U) (A : hsubtypes X) : U = (x : X) * (A x).1
sethsubtypes (X : U) : set (hsubtypes X) =
  setPi X (\(_ : X) -> hProp) (\(_ : X) -> sethProp)

-- Definition hrel (X : UU) := X -> X -> hProp.
hrel (X : U) : U = X -> X -> hProp

iseqclass (X : U) (R : hrel X) (A : hsubtypes X) : U =
  and (and (ishinh (carrier X A)).1
                   ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1))
          ((x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1)

eqax0 (X : U) (R : hrel X) (A : hsubtypes X) (eqc : iseqclass X R A) :
  (ishinh (carrier X A)).1 = eqc.1.1
eqax1 (X : U) (R : hrel X) (A : hsubtypes X) (eqc : iseqclass X R A) :
  (x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1 = eqc.1.2
eqax2 (X : U) (R : hrel X) (A : hsubtypes X) (eqc : iseqclass X R A) :
  (x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1 = eqc.2

propiseqclass (X : U) (R : hrel X) (A : hsubtypes X) : prop (iseqclass X R A) =
  propAnd (and (ishinh (carrier X A)).1
                          ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1))
                 ((x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1)
                 (propAnd (ishinh (carrier X A)).1
                                 ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1) p1 p2)
                 p3
  where
  p1 : prop (ishinh (carrier X A)).1 = propishinh (carrier X A)

  -- This proof is quite cool, but it looks ugly...
  p2 (f g : (x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1) :
   Path ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1) f g =
    <i> \(x1 x2 : X) (h1 : (R x1 x2).1) (h2 : (A x1).1) ->
         (A x2).2 (f x1 x2 h1 h2) (g x1 x2 h1 h2) @ i

  p3 (f g : (x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1) :
    Path ((x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1) f g =
   <i> \(x1 x2 : X) (h1 : (A x1).1) (h2 : (A x2).1) ->
        (R x1 x2).2 (f x1 x2 h1 h2) (g x1 x2 h1 h2) @ i

hSet : U = (X : U) * set X

isrefl (X : U) (R : hrel X) : U = (x : X) -> (R x x).1
issymm (X : U) (R : hrel X) : U = (x1 x2 : X) -> (R x1 x2).1 -> (R x2 x1).1
istrans (X : U) (R : hrel X) : U =
  (x1 x2 x3 : X) -> (R x1 x2).1 -> (R x2 x3).1 -> (R x1 x3).1

ispreorder (X : U) (R : hrel X) : U = and (istrans X R) (isrefl X R)

iseqrel (X : U) (R : hrel X) : U = and (ispreorder X R) (issymm X R)

eqrel (X : U) : U = (R : hrel X) * (iseqrel X R)

eqrelrefl (X : U) (R : eqrel X) : isrefl X R.1 = R.2.1.2
eqrelsymm (X : U) (R : eqrel X) : issymm X R.1 = R.2.2
eqreltrans (X : U) (R : eqrel X) : istrans X R.1 = R.2.1.1

boolset : hSet = (bool,setbool)

setquot (X : U) (R : hrel X) : U = (A : hsubtypes X) * (iseqclass X R A)
pr1setquot (X : U) (R : hrel X) (Q : setquot X R) : hsubtypes X = Q.1

setquotpr (X : U) (R : eqrel X) (X0 : X) : setquot X R.1 = (A,((p1,p2),p3))
   where
   rax : isrefl X R.1 = eqrelrefl X R
   sax : issymm X R.1 = eqrelsymm X R
   tax : istrans X R.1 = eqreltrans X R
   A : hsubtypes X = \(x : X) -> R.1 X0 x
   p1 : (ishinh (carrier X A)).1 = hinhpr (carrier X A) (X0,rax X0)
   p2 (x1 x2 : X) (X1 : (R.1 x1 x2).1) (X2 : (A x1).1) : (A x2).1 = tax X0 x1 x2 X2 X1
   p3 (x1 x2 : X) (X1 : (A x1).1) (X2 : (A x2).1) : (R.1 x1 x2).1 = tax x1 X0 x2 (sax X0 x1 X1) X2

setquotl0 (X : U) (R : eqrel X) (c : setquot X R.1) (x : carrier X c.1) :
  Path (setquot X R.1) (setquotpr X R x.1) c = subtypeEquality (hsubtypes X) (iseqclass X R.1) p (setquotpr X R x.1) c rem
  where
  p (A : hsubtypes X) : prop (iseqclass X R.1 A) = propiseqclass X R.1 A
  rem : Path (hsubtypes X) (setquotpr X R x.1).1 c.1 = <i> \(x : X) -> (rem' x) @ i -- inlined use of funext
    where rem' (a : X) : Path hProp ((setquotpr X R x.1).1 a) (c.1 a) =
            uahp' ((setquotpr X R x.1).1 a) (c.1 a) l2r r2l   -- This is where uahp appears
              where
              l2r (r : ((setquotpr X R x.1).1 a).1) : (c.1 a).1 = eqax1 X R.1 c.1 c.2 x.1 a r x.2
              r2l : (c.1 a).1 -> ((setquotpr X R x.1).1 a).1 = eqax2 X R.1 c.1 c.2 x.1 a x.2

setquotunivprop (X : U) (R : eqrel X) (P : setquot X R.1 -> hProp)
  (ps : (x : X) -> (P (setquotpr X R x)).1) (c : setquot X R.1) : (P c).1 = hinhuniv (carrier X c.1) (P c) f rem
  where
   f (x : carrier X c.1) : (P c).1 =
     let e : Path (setquot X R.1) (setquotpr X R x.1) c = setquotl0 X R c x
     in subst (setquot X R.1) (\(w : setquot X R.1) -> (P w).1) (setquotpr X R x.1) c e (ps x.1)
   rem : (ishinh (carrier X c.1)).1 = eqax0 X R.1 c.1 c.2

setquotuniv2prop (X : U) (R : eqrel X) (P : setquot X R.1 -> setquot X R.1 -> hProp)
  (ps : (x x' : X) -> (P (setquotpr X R x) (setquotpr X R x')).1) (c c' : setquot X R.1) : (P c c').1 =
    setquotunivprop X R (\ (c0' : setquot X R.1) -> P c c0')
      (\ (x : X) -> setquotunivprop X R (\ (c0 : setquot X R.1) -> P c0 (setquotpr X R x))
                      (\ (x0 : X) -> ps x0 x) c) c'

setquotuniv3prop (X : U) (R : eqrel X)
    (P : setquot X R.1 -> setquot X R.1 -> setquot X R.1 -> hProp)
    (ps : (x0 x1 x2 : X) -> (P (setquotpr X R x0) (setquotpr X R x1) (setquotpr X R x2)).1)
    (q0 q1 q2 : setquot X R.1) : (P q0 q1 q2).1
  = setquotunivprop X R (P q0 q1) (\(x2' : X) -> setquotunivprop X R (\ (q1' : setquot X R.1) -> P q0 q1' (setquotpr X R x2'))
          (\(x1' : X) ->  setquotunivprop X R (\(q0' : setquot X R.1) -> P q0' (setquotpr X R x1')
              (setquotpr X R x2')) (\(x0' : X) -> ps x0' x1' x2') q0) q1) q2

setsetquot (X : U) (R : hrel X) : set (setquot X R) =
  setSig (hsubtypes X) (\(A : hsubtypes X) -> iseqclass X R A)
    sA sB
    where
    sA : set (hsubtypes X) = sethsubtypes X
    sB (x : hsubtypes X) : set (iseqclass X R x) = propSet (iseqclass X R x) (propiseqclass X R x)

iscompsetquotpr (X : U) (R : eqrel X) (x x' : X) (a : (R.1 x x').1) :
  Path (setquot X R.1) (setquotpr X R x) (setquotpr X R x') =
  subtypeEquality (hsubtypes X) (iseqclass X R.1) rem1 (setquotpr X R x) (setquotpr X R x') rem2
  where
  rem1 (x : hsubtypes X) : prop (iseqclass X R.1 x) = propiseqclass X R.1 x
  rem2 : Path (hsubtypes X) (setquotpr X R x).1 (setquotpr X R x').1 =
    <i> \(x0 : X) -> rem x0 @ i
    where
    rem (x0 : X) : Path hProp (R.1 x x0) (R.1 x' x0) = uahp' (R.1 x x0) (R.1 x' x0) f g
      where
      f (r0 : (R.1 x x0).1) : (R.1 x' x0).1 =
        eqreltrans X R x' x x0 (eqrelsymm X R x x' a) r0
      g (r0 : (R.1 x' x0).1) : (R.1 x x0).1 =
        eqreltrans X R x x' x0 a r0

weqpathsinsetquot (X : U) (R : eqrel X) (x x' : X) :
  equiv (R.1 x x').1 (Path (setquot X R.1) (setquotpr X R x) (setquotpr X R x')) =
  (iscompsetquotpr X R x x',rem)
  where
  rem : isEquiv (R.1 x x').1
                (Path (setquot X R.1) (setquotpr X R x) (setquotpr X R x'))
                (iscompsetquotpr X R x x') =
    isEquivprop (R.1 x x').1
                (Path (setquot X R.1) (setquotpr X R x) (setquotpr X R x'))
                (iscompsetquotpr X R x x')
                g pA pB
   where g (e : Path (setquot X R.1) (setquotpr X R x) (setquotpr X R x')) :
             (R.1 x x').1 = transport (<i> (rem1 @ i).1) rem
           where
           rem : (R.1 x' x').1 = eqrelrefl X R x'
           rem2 : Path hProp (R.1 x x') (R.1 x' x') = <i> (e @ i).1 x'
           rem1 : Path hProp (R.1 x' x') (R.1 x x') = <i> rem2 @ -i
         pA : prop (R.1 x x').1 = (R.1 x x').2
         pB : prop (Path (setquot X R.1) (setquotpr X R x) (setquotpr X R x')) =
                setsetquot X R.1 (setquotpr X R x) (setquotpr X R x')

isdecprop (X : U) : U = and (prop X) (dec X)

propisdecprop (X : U): prop (isdecprop X) =
  propSig (prop X) (\ (_ : prop X) -> dec X) rem1 rem2
  where
  rem1 : prop (prop X) = propIsProp X
  rem2 : prop X -> prop (dec X) = propDec X

isdeceqif (X : U) (h : (x x' : X) -> isdecprop (Path X x x')) : discrete X =
  \(x x' : X) -> (h x x').2

propEquiv (X Y : U) (w : equiv X Y) : prop X -> prop Y = subst U prop X Y rem
  where
  rem : Path U X Y = transport (<i> corrUniv X Y @ -i) w

isdecpropweqf (X Y : U) (w : equiv X Y) (hX : isdecprop X) : isdecprop Y = (rem1,rem2 hX.2)
  where
  rem1 : prop Y = propEquiv X Y w hX.1
  rem2 : dec X -> dec Y = split
    inl x -> inl (w.1 x)
    inr nx -> inr (\(y : Y) -> nx (invEq X Y w y))

isdiscretesetquot (X : U) (R : eqrel X) (is : (x x' : X) -> isdecprop (R.1 x x').1) :
  discrete (setquot X R.1) = isdeceqif (setquot X R.1) rem
  where
  rem : (x x' : setquot X R.1) -> isdecprop (Path (setquot X R.1) x x') =
    setquotuniv2prop X R
      (\(x0 x0' : setquot X R.1) -> (isdecprop (Path (setquot X R.1) x0 x0'),
                                     propisdecprop (Path (setquot X R.1) x0 x0'))) rem'
    where
    rem' (x0 x0' : X) : isdecprop (Path (setquot X R.1) (setquotpr X R x0) (setquotpr X R x0')) =
      isdecpropweqf (R.1 x0 x0').1 (Path (setquot X R.1) (setquotpr X R x0) (setquotpr X R x0'))
                    (weqpathsinsetquot X R x0 x0') (is x0 x0')

discretetobool (X : U) (h : discrete X) (x y : X) : bool = rem (h x y)
  where
  rem : dec (Path X x y) -> bool = split
    inl _ -> true
    inr _ -> false



-- The universal property of set quotients

funresprel (A B : U) (f : A -> B) (R : hrel A) : U
  = (a a' : A) (r : (R a a').1) -> Path B (f a) (f a')

-- If f respects R then all x belonging to the equivalence class C are mapped into the same unique image
setquotmapcontr (A B : U) (sB : set B) (R : hrel A) (f : A -> B)
    (frr : funresprel A B f R) (C : setquot A R)
  : isContr ((y : B) * ((x : carrier A C.1) -> Path B y (f x.1)))
  = let
    T : U = (y : B) * ((x : carrier A C.1) -> Path B y (f x.1))
    pT (a b : T) : Path T a b
      = let
        h (x : carrier A C.1) : Path B a.1 b.1 = <i> comp (<j> B) (a.2 x @ i)
          [ (i = 0) -> <j> a.1
          , (i = 1) -> <j> b.2 x @ -j ]
        p0 : Path B a.1 b.1
          = C.2.1.1 (Path B a.1 b.1, sB a.1 b.1) h
        p1 : PathP (<i> (x : carrier A C.1) -> Path B (p0 @ i) (f x.1)) a.2 b.2
          = let
            P (b : B) : U
              = (x : carrier A C.1) -> Path B b (f x.1)
            pP (b : B) (s t : (P b)) : Path (P b) s t
              = <i>  \ (x : carrier A C.1) -> (sB b (f x.1) (s x) (t x)) @ i
          in lemPropF B P pP a.1 b.1 p0 a.2 b.2
      in <i> (p0 @ i, p1 @ i)
    h (x : carrier A C.1) : T
      = (f x.1, \ (x' : carrier A C.1) -> frr x.1 x'.1 (C.2.2 x.1 x'.1 x.2 x'.2))
    y : T
      = C.2.1.1 (T, pT) h
  in (y, pT y)

setquotmap (A B : U) (sB : set B) (R : hrel A) (f : A -> B)
    (frr : funresprel A B f R) (c : setquot A R) : B
  = (setquotmapcontr A B sB R f frr c).1.1

setquotmapeq (A B : U) (sB : set B) (R : eqrel A) (f : A -> B)
    (frr : funresprel A B f R.1) (x : A)
  : Path B (setquotmap A B sB R.1 f frr (setquotpr A R x)) (f x)
  = (setquotmapcontr A B sB R.1 f frr (setquotpr A R x)).1.2 (x, R.2.1.2 x)

opaque setquotunivprop

setquotuniversalproperty (A B : U) (sB : set B) (R : eqrel A) (f : A -> B)
    (frr : funresprel A B f R.1)
  : isContr ( (g : setquot A R.1 -> B)
            * (Path (A -> B) (\ (a : A) -> g (setquotpr A R a)) f))
  = let
    G : U
      = setquot A R.1 -> B
    I (g : G) : U
      = Path (A -> B) (\ (a : A) -> g (setquotpr A R a)) f
    pI (g : G) : prop (I g)
      = setPi A (\ (a : A) -> B) (\ (a : A) -> sB) (\ (a : A) -> g (setquotpr A R a)) f
    g : G
      = setquotmap A B sB R.1 f frr
    i : I g
      = <i> \ (a : A) -> setquotmapeq A B sB R f frr a @ i
    eq (h : (g : G) * I g) : Path ((g : G) * I g) (g, i) h
      = let
        p0 : Path G g h.1
          = <j> \ (x : setquot A R.1) -> let
            P (y : setquot A R.1) : hProp
              = (Path B (g y) (h.1 y), sB (g y) (h.1 y))
            ps (a : A) : (P (setquotpr A R a)).1
              = <k> comp (<_> B) ((i @ k) a)
                [ (k = 0) -> <_> g (setquotpr A R a)
                , (k = 1) -> <l> (h.2 @ -l) a ]
          in setquotunivprop A R P ps x @ j
        p1 : PathP (<i> I (p0 @ i)) i h.2
          = lemPropF G I pI g h.1 p0 i h.2
      in <i> (p0 @ i, p1 @ i)
  in ((g, i), eq)

funresprel2 (A B C : U) (f : A -> B -> C) (R0 : hrel A) (R1 : hrel B) : U
  = (a a' : A) (b b' : B) -> (R0 a a').1 -> (R1 b b').1 -> Path C (f a b) (f a' b')

hProppair (X Y : hProp) : hProp
  = (and X.1 Y.1, propAnd X.1 Y.1 X.2 Y.2)

hrelpair (A B : U) (R0 : hrel A) (R1 : hrel B) (x y : and A B) : hProp
  = hProppair (R0 x.1 y.1) (R1 x.2 y.2)

iseqrelpair (A B : U) (R0 : hrel A) (R1 : hrel B) (E0 : iseqrel A R0)
    (E1 : iseqrel B R1) : iseqrel (and A B) (hrelpair A B R0 R1)
  = let
    T : U
      = and A B
    R : hrel T
      = hrelpair A B R0 R1
    rax : isrefl T R
      = \ (t0 : T) -> (E0.1.2 t0.1, E1.1.2 t0.2)
    sax : issymm T R
      = \ (t0 t1 : T) (e : (R t0 t1).1) -> (E0.2 t0.1 t1.1 e.1, E1.2 t0.2 t1.2 e.2)
    tax : istrans T R
      = \ (t0 t1 t2 : T) (e0 : (R t0 t1).1) (e1 : (R t1 t2).1) ->
            (E0.1.1 t0.1 t1.1 t2.1 e0.1 e1.1, E1.1.1 t0.2 t1.2 t2.2 e0.2 e1.2)
  in ((tax, rax), sax)

eqrelpair (A B : U) (R0 : eqrel A) (R1 : eqrel B) : eqrel (and A B)
  = (hrelpair A B R0.1 R1.1, iseqrelpair A B R0.1 R1.1 R0.2 R1.2)

hsubtypespair (A B : U) (H0 : hsubtypes A) (H1 : hsubtypes B) (x : and A B) : hProp
  = hProppair (H0 x.1) (H1 x.2)

iseqclasspair (A B : U) (R0 : hrel A) (R1 : hrel B) (H0 : hsubtypes A)
    (H1 : hsubtypes B) (E0 : iseqclass A R0 H0) (E1 : iseqclass B R1 H1)
  : iseqclass (and A B) (hrelpair A B R0 R1) (hsubtypespair A B H0 H1)
  = let
    H : hsubtypes (and A B)
      = hsubtypespair A B H0 H1
    a (P : hProp) (f : carrier (and A B) H -> P.1) : P.1
      = let
        g (x0 : carrier A H0) : P.1
          = let
            h (x1 : carrier B H1) : P.1
              = f ((x0.1, x1.1), (x0.2, x1.2))
          in E1.1.1 P h
      in E0.1.1 P g
    b (x0 x1 : and A B) (r : (hrelpair A B R0 R1 x0 x1).1) (h0 : (H x0).1) : (H x1).1
      = (E0.1.2 x0.1 x1.1 r.1 h0.1, E1.1.2 x0.2 x1.2 r.2 h0.2)
    c (x0 x1 : and A B) (h0 : (H x0).1) (h1 : (H x1).1) : (hrelpair A B R0 R1 x0 x1).1
      = (E0.2 x0.1 x1.1 h0.1 h1.1, E1.2 x0.2 x1.2 h0.2 h1.2)
  in ((a, b), c)

setquotpair (A B : U) (R0 : hrel A) (R1 : hrel B) (q0 : setquot A R0)
    (q1 : setquot B R1)
  : setquot (and A B) (hrelpair A B R0 R1)
  = ( hsubtypespair A B q0.1 q1.1
    , iseqclasspair A B R0 R1 q0.1 q1.1 q0.2 q1.2)

setquotmap2 (A B C : U) (sC : set C) (R0 : hrel A) (R1 : hrel B)
    (f : A -> B -> C) (frr : funresprel2 A B C f R0 R1) (c0 : setquot A R0)
    (c1 : setquot B R1) : C
  = let
    f' (t : and A B) : C
      = f t.1 t.2
    R' : hrel (and A B)
      = hrelpair A B R0 R1
    frr' (s t : and A B) (r : (R' s t).1) : Path C (f' s) (f' t)
      = frr s.1 t.1 s.2 t.2 r.1 r.2
    c' : setquot (and A B) R'
      = setquotpair A B R0 R1 c0 c1
  in setquotmap (and A B) C sC R' f' frr' c'

setquotmapeq2 (A B C : U) (sC : set C) (R0 : eqrel A) (R1 : eqrel B)
    (f : A -> B -> C) (frr : funresprel2 A B C f R0.1 R1.1) (x0: A) (x1 : B)
  : Path C (setquotmap2 A B C sC R0.1 R1.1 f frr (setquotpr A R0 x0) (setquotpr B R1 x1)) (f x0 x1)
  = let
    f' (t : and A B) : C
      = f t.1 t.2
    R : eqrel (and A B)
      = eqrelpair A B R0 R1
    frr' (s t : and A B) (r : (R.1 s t).1) : Path C (f' s) (f' t)
      = frr s.1 t.1 s.2 t.2 r.1 r.2
  in setquotmapeq (and A B) C sC R f' frr' (x0, x1)

transparent setquotunivprop


-- The bool exercise:

R : eqrel bool = (r1,r2)
  where
  r1 : hrel bool = \(x y : bool) -> (Path bool x y,setbool x y)
  r2 : iseqrel bool r1 = ((compPath bool,refl bool),inv bool)

bool' : U = setquot bool R.1
true' : bool' = setquotpr bool R true
false' : bool' = setquotpr bool R false

P' (t : bool') : hProp =
  hdisj (Path bool' t true') (Path bool' t false')

K' (t : bool') : (P' t).1 = setquotunivprop bool R P' ps t
  where
  ps : (x : bool) -> (P' (setquotpr bool R x)).1 = split
    false -> hdisj_in2 (Path bool' false' true')
                       (Path bool' false' false') (<_> false')
    true  -> hdisj_in1 (Path bool' true' true')
                       (Path bool' true' false') (<_> true')

test : (P' true').1 = hdisj_in1 (Path bool' true' true')
                                (Path bool' true' false') (<_> true')
test' : (P' true').1 = K' true'

-- test'' : Path (P' true').1 test test' = (P' true').2 test test'

-- These two terms are not convertible:
-- test' : Path (P' true').1 (K' true')
--           (hdisj_in1 (Path (setquot bool R.1) true' true') (Path (setquot bool R.1) true' false') (<_> true')) =
--   <_> K' true'


-- Another test:

true'neqfalse' (H : Path bool' true' false') : N0 = falseNeqTrue rem1
  where
  rem : Path U (Path bool true true) (Path bool false true) = <i> ((H @ i).1 true).1
  rem1 : Path bool false true = comp rem (<_> true) []

test1 (x : bool') (H1 : Path bool' x true') (H2 : Path bool' x false') : N0 = true'neqfalse' rem
  where
  rem : Path bool' true' false' = <i> comp (<_> bool') x [(i = 0) -> H1, (i = 1) -> H2]

test2 (x : bool') (p1 : (ishinh (Path bool' x true')).1)
                  (p2 : (ishinh (Path bool' x false')).1) : N0 =
  hinhuniv (Path bool' x true') (N0,propN0) rem p1
  where
  rem (H1 : Path bool' x true') : N0 =
    hinhuniv (Path bool' x false') (N0,propN0)
             (\(H2 : Path bool' x false') -> test1 x H1 H2) p2

-- shorthand for this big type
T (x : bool') : U = or (ishinh (Path bool' x true')).1 (ishinh (Path bool' x false')).1

-- test3 (x : bool') : prop (T x)
test3 (x : bool') : (a b : T x) -> Path (T x) a b = split
  inl a' -> rem
    where
    rem : (b : T x) -> Path (T x) (inl a') b = split
      inl b' -> <i> inl (propishinh (Path bool' x true') a' b' @ i)
      inr b' -> efq (Path (T x) (inl a') (inr b')) (test2 x a' b')
  inr a' -> rem
    where
    rem : (b : T x) -> Path (T x) (inr a') b = split
      inl b' -> efq (Path (T x) (inr a') (inl b')) (test2 x b' a')
      inr b' -> <i> inr (propishinh (Path bool' x false') a' b' @ i)

f (x : bool') : or (ishinh (Path bool' x true')).1 (ishinh (Path bool' x false')).1 -> bool = split
  inl _ -> true
  inr _ -> false

bar (x : bool') : or (Path bool' x true') (Path bool' x false') ->
  or (ishinh (Path bool' x true')).1 (ishinh (Path bool' x false')).1 = split
  inl p -> inl (hinhpr (Path bool' x true') p)
  inr p -> inr (hinhpr (Path bool' x false') p)

-- finally the map:
foo (x : bool') (x' : (P' x).1) : bool = f x rem
  where
  rem : or (ishinh (Path bool' x true')).1 (ishinh (Path bool' x false')).1 =
    hinhuniv (or (Path bool' x true') (Path bool' x false'))
             (or (ishinh (Path bool' x true')).1 (ishinh (Path bool' x false')).1,test3 x)
             (bar x) x'

-- > :n testfoo
-- NORMEVAL: true
-- Time: 0m0.490s
testfoo : bool = foo true' (K' true')

testfoo' : Path bool (foo true' (K' true')) true = <i> foo true' (K' true')


-- Tests of checking normal forms:

ntrue' : bool' = (\(x : bool) -> (PathP (<i0> bool) true x,lem8 x),((\(P : Sigma U (\(X : U) -> (a b : X) -> PathP (<i0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> PathP (<i0> bool) true x)) -> P.1) -> f ((true,<i0> true)),\(x1 x2 : bool) -> \(X1 : PathP (<i0> bool) x1 x2) -> \(X2 : PathP (<i0> bool) true x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> true, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : PathP (<i0> bool) true x1) -> \(X2 : PathP (<i0> bool) true x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ]))


nhdisj_in1 : (P Q : U) (X : P) -> (hdisj P Q).1 =
  \(P Q : U) -> \(X : P) -> \(P0 : Sigma U (\(X0 : U) -> (a b : X0) -> PathP (<!0> X0) a b)) -> \(f : or P Q -> P0.1) -> f (inl X)

ntest : (P' true').1 = \(P : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> \(f : or (PathP (<!0> Sigma (bool -> (Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b))) (\(A : bool -> (Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b))) -> Sigma (Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (PathP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (PathP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (PathP (<!0> bool) x1 x2))))) ((\(x : bool) -> (PathP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> PathP (<!0> bool) true x)) -> P0.1) -> f ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) x1 x2) -> \(X2 : PathP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) true x1) -> \(X2 : PathP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))) ((\(x : bool) -> (PathP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> PathP (<!0> bool) true x)) -> P0.1) -> f ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) x1 x2) -> \(X2 : PathP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) true x1) -> \(X2 : PathP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ])))) PathP (<!0> Sigma (bool -> (Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b))) (\(A : bool -> (Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b))) -> Sigma (Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (PathP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (PathP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (PathP (<!0> bool) x1 x2))))) ((\(x : bool) -> (PathP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> PathP (<!0> bool) true x)) -> P0.1) -> f ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) x1 x2) -> \(X2 : PathP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) true x1) -> \(X2 : PathP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))) ((\(x : bool) -> (PathP (<!0> bool) false x,lem7 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> PathP (<!0> bool) false x)) -> P0.1) -> f ((false,<!0> false)),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) x1 x2) -> \(X2 : PathP (<!0> bool) false x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> false, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) false x1) -> \(X2 : PathP (<!0> bool) false x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))) -> P.1) -> f (inl (<!0> (\(x : bool) -> (PathP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> PathP (<!0> X) a b)) -> \(f0 : (Sigma bool (\(x : bool) -> PathP (<!0> bool) true x)) -> P0.1) -> f0 ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) x1 x2) -> \(X2 : PathP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : PathP (<!0> bool) true x1) -> \(X2 : PathP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))))