quotient3.cub

module quotient3 where

import description
import exists
import hedberg
import equivProp


quot : (A:U) -> (R:rel A) -> U
quot A R = Sigma (A->U) (\f->exists A (\c->Id (A->U) (R c) f))

canProj : (A:U) (R:rel A) -> A -> quot A R
canProj A R a = (R a , pr)
  where
    pr : exists A (\c -> Id (A->U) (R c) (R a))
    pr = inc (Sigma A (\c-> Id (A->U) (R c) (R a))) (a, refl (A->U) (R a))



propRel : (A : U) (R : rel A) -> U
propRel A R = (a b : A) -> prop (R a b)


relQuot : (A:U) (R:rel A) -> equivalence A R -> propRel A R -> (x y:A) -> R x y ->  
          Id (quot A R) (canProj A R x) (canProj A R y)
relQuot A R eqR propR x y equiv_xy  = res
where
    P : A -> U
    P = (canProj A R x).1
    Q : A->U
    Q = (canProj A R y).1
    lem1: (c:A) -> P c -> Q c
    lem1 c p = eqR.2 y c x (eqToSym A R eqR x y equiv_xy) (eqToSym A R eqR x c p)
    lem2 : (c:A) -> Q c -> P c
    lem2 c q = eqR.2 x c y equiv_xy (eqToSym A R eqR y c q)
    lem3 : (c:A) -> Id U (P c) (Q c)
    lem3 c = propExt (P c) (Q c) (propR x c) (propR y c) (lem1 c) (lem2 c)
    lem4 : Id (A->U) P Q
    lem4 = funExt A (\u->U) P Q lem3
    h : propFam (A->U) (\f->exists A (\c->Id (A->U) (R c) f))
    h f = squash (Sigma A (\c->Id (A->U) (R c) f))
    res : Id (quot A R) (canProj A R x) (canProj A R y)
    res = eqPropFam (A->U) (\f->exists A (\c->Id (A->U) (R c) f)) h (canProj A R x) (canProj A R y) lem4



exQuot : (A : U) (R : rel A) -> equivalence A R -> propRel A R -> (x:quot A R) -> (exists A x.1)
exQuot A R eqR pR x = exElim A (\c->Id (A->U) (R c) (x.1)) (exists A x.1) H exP0 (x.2)
   where
      H : prop (exists A x.1)
      H = squash (Sigma A x.1)
      exP0 : Sigma A (\c->Id (A->U) (R c) x.1) -> exists A x.1
      exP0 p = inc (Sigma A x.1) (p.1 , rem)
         where
            rem : x.1 p.1
            rem = subst (A->U) (\H->H p.1) (R p.1) x.1 p.2 (eqR.1 p.1)


prQuot : (A : U) (R : rel A) -> equivalence A R -> propRel A R -> (x:quot A R) -> (propFam A x.1)
prQuot A R eqR pR x = exElim A (\c->Id (A->U) (R c) (x.1)) H propH prP0 (x.2)
   where
      H : U
      H = propFam A x.1
      H0 : (a:A) -> prop (prop (x.1 a))
      H0 a = propIsProp (x.1 a)
      propH : prop H
      propH = propPi A (\a->prop (x.1 a)) H0
      prP0 : Sigma A (\c->Id (A->U) (R c) x.1) -> propFam A x.1
      prP0 p a = subst (A->U) (\f->prop (f a)) (R p.1) x.1 p.2 (pR p.1 a)


eqsym : (X:U) -> (x y:X) -> Id X x y -> Id X y x
eqsym X x y p = subst X (\z -> Id X z x) x y p (refl X x)


unQuot : (A : U) (R : rel A) -> equivalence A R -> propRel A R -> (x:quot A R) -> (a b:A) -> x.1 a -> x.1 b -> R a b
unQuot A R eqR pR x a b pa pb = exElim A (\c->Id (A->U) (R c) (x.1)) H propH unP0 (x.2)
  where
    H : U
    H = R a b
    propH : prop H
    propH = pR a b
    symR : symmetry A R
    symR = eqToSym A R eqR
    unP0 : Sigma A (\c->Id (A->U) (R c) x.1) -> R a b
    unP0 p = eqR.2 a b (p.1) (symR (p.1) a rca) (symR (p.1) b rcb)
       where
          rem : Id (A->U) x.1 (R p.1)
          rem = eqsym (A->U) (R p.1) x.1 p.2
          rca : R (p.1) a
          rca = subst (A->U) (\f->f a) x.1 (R p.1) rem pa
          rcb : R (p.1) b
          rcb = subst (A->U) (\f-> f b) x.1 (R p.1) rem pb


resp : (A B : U) (R : rel A) (f : A -> B) -> U
resp A B R f = (x y : A) -> R x y -> Id B (f x) (f y)

univQuot : (A B : U) (R : rel A) (f : A -> B) -> set B -> resp A B R f -> 
        (eqR : equivalence A R) (pR : propRel A R) (x : quot A R) -> B
univQuot A B R f uip fresp eqR pR x = iota B imfP rem1 rem2
   where
      P : A -> U
      P = x.1
      ex : exists A P
      ex = exQuot A R eqR pR x
      un : (a b : A) -> P a -> P b -> R a b
      un = unQuot A R eqR pR x
      pr : propFam A P
      pr = prQuot A R eqR pR x
      S : B -> A -> U
      S b a = and (P a) (Id B (f a) b)
      imfP : B -> U
      imfP b = exists A (\a -> S b a)
      rem1 : propFam B imfP
      rem1 b = squash (Sigma A (\a -> S b a))
      rem3 : Sigma A P -> exists B imfP
      rem3 z = inc (Sigma B imfP) (f z.1,inc (Sigma A (S (f z.1))) (z.1,(z.2,refl B (f z.1))))
      rem4 : exists B imfP
      rem4 = inhrec (Sigma A P) (exists B imfP) (squash (Sigma B imfP)) rem3 ex
      rem6 : (b b' : B) (a a' : A) (_ : and (P a) (Id B (f a) b))
             (_ : and (P a') (Id B (f a') b')) -> Id B b b'
      rem6 b b' a a' z z' = compUp B (f a) b (f a') b' z.2 z'.2 rem7
            where rem8 : R a a'
                  rem8 = un a a' z.1 z'.1
                  rem7 : Id B (f a) (f a')
                  rem7 = fresp a a' rem8
      rem7 : (b b' : B) -> Sigma A (S b) ->  Sigma A (S b') -> Id B b b'
      rem7 b b' z z' = rem6 b b' z.1 z'.1 z.2 z'.2
      rem8 : (b b' : B) -> Sigma A (S b) -> exists A (S b') -> Id B b b'
      rem8 b b' h = exElim A (S b') (Id B b b') (uip b b') (rem7 b b' h)
      rem9 : (b b' : B) -> exists A (S b) -> exists A (S b') -> Id B b b'
      rem9 b b' h h' = exElim A (S b) (Id B b b') (uip b b')
                                    (\h'' -> rem8 b b' h'' h') h
      rem5 : atmostOne B imfP
      rem5 = rem9
      rem2 : exactOne B imfP
      rem2 = (rem4,rem5)



---------------
exAnd : (A:U) (P Q: A -> U) -> exists A P -> exists A Q -> exists (and A A) (\x -> and (P x.1) (Q x.2))
exAnd A P Q = res
  where
    rem1 : Sigma A P -> Sigma A Q -> exists (and A A) (\x->and (P x.1) (Q x.2))
    rem1 p q = inc (Sigma (and A A) (\x->and (P x.1) (Q x.2))) ((p.1,q.1) , (p.2 , q.2))
    rem2 : Sigma A P -> exists A Q -> exists (and A A) (\x->and (P x.1) (Q x.2))
    rem2 p = exElim A Q (exists (and A A) (\x->and (P x.1) (Q x.2))) (squash (Sigma (and A A) (\x->and (P x.1) (Q x.2)))) (rem1 p)
    H : U
    H = exists A Q -> exists (and A A) (\x->and (P x.1) (Q x.2))
    propH : prop H
    propH = propImply (exists A Q) (exists (and A A) (\x->and (P x.1) (Q x.2))) (\_ -> squash (Sigma (and A A) (\x->and (P x.1) (Q x.2))))
    res : exists A P -> exists A Q -> exists (and A A) (\x->and (P x.1) (Q x.2))
    res = exElim A P H propH rem2



resp2 : (A B : U) (R:rel A) (f: A->A->B) -> U
resp2 A B R f = (a b c d:A) -> R a b -> R c d -> Id B (f a c) (f b d)

univQuot2 : (A B : U) (R : rel A) (f : A -> A -> B) -> set B -> resp2 A B R f -> 
           (eqR : equivalence A R) (pR : propRel A R) ->
           (x y : quot A R) -> B
univQuot2 A B R f uip fresp2 eqR pR x y = iota B imfP rem1 rem2
   where
      P : A -> U
      P = x.1
      exP : exists A P
      exP = exQuot A R eqR pR x
      unP : (a b : A) -> P a -> P b -> R a b
      unP = unQuot A R eqR pR x
      prP : propFam A P
      prP = prQuot A R eqR pR x
      Q : A -> U
      Q = y.1
      exQ : exists A Q
      exQ = exQuot A R eqR pR y
      unQ : (a b : A) -> Q a -> Q b -> R a b
      unQ = unQuot A R eqR pR y
      prQ : propFam A Q
      prQ = prQuot A R eqR pR y
      f0 : (and A A) -> B
      f0 x = f x.1 x.2
      PQ : (and A A) -> U
      PQ x = and (P x.1) (Q x.2)
      exPQ : exists (and A A) PQ
      exPQ = exAnd A P Q exP exQ
      S : B -> (and A A) -> U
      S b x = and (PQ x) (Id B (f x.1 x.2) b)
      imfP : B -> U
      imfP b = exists (and A A) (\x -> (S b x))
      rem1 : propFam B imfP
      rem1 b = squash (Sigma (and A A) (\x -> (S b x)))
      rem3 : Sigma (and A A) PQ -> exists B imfP
      rem3 z = inc (Sigma B imfP) (f0 z.1 , inc (Sigma (and A A) (S (f0 z.1))) (z.1,(z.2,refl B (f0 z.1))))
      rem4 : exists B imfP
      rem4 = inhrec (Sigma (and A A) PQ) (exists B imfP) (squash (Sigma B imfP)) rem3 exPQ
      rem6 : (b b':B) (x x':(and A A)) (_ : S b x) (_ : S b' x') -> Id B b b'
      rem6 b b' x x' z z' = compUp B (f0 x) b (f0 x') b' z.2 z'.2 H
           where H0 : R x.1 x'.1
                 H0 = unP x.1 x'.1 (z.1.1) (z'.1.1)
                 H1 : R x.2 x'.2
                 H1 = unQ x.2 x'.2 (z.1.2) (z'.1.2)
                 H : Id B (f0 x) (f0 x')
                 H = fresp2 x.1 x'.1 x.2 x'.2 H0 H1
      rem7 : (b b':B) -> Sigma (and A A) (S b) -> Sigma (and A A) (S b') -> Id B b b'
      rem7 b b' z z' = rem6 b b' z.1 z'.1 z.2 z'.2
      rem8 : (b b':B) -> Sigma (and A A) (S b) -> exists (and A A) (S b') -> Id B b b'
      rem8 b b' h = exElim (and A A) (S b') (Id B b b') (uip b b') (rem7 b b' h)
      rem9 : (b b' : B) -> exists (and A A) (S b) -> exists (and A A) (S b') -> Id B b b'
      rem9 b b' h h' = exElim (and A A) (S b) (Id B b b') (uip b b') (\h'' -> rem8 b b' h'' h') h
      rem5 : atmostOne B imfP
      rem5 = rem9
      rem2 : exactOne B imfP
      rem2 = (rem4,rem5)




kernel : (A B : U) (f : A -> B) -> rel A
kernel A B f a a' = Id B (f a) (f a')

kerRef : (A B : U) (f : A -> B) -> reflexive A (kernel A B f)
kerRef A B f a = refl B (f a)

kerEucl : (A B : U) (f : A -> B) -> euclidean A (kernel A B f)
kerEucl A B f a b c p q = compInv B (f c) (f a) (f b) rem rem1
   where 
     rem : Id B (f c) (f a)
     rem = inv B (f a) (f c) p
     rem1 : Id B (f c) (f b)
     rem1 = inv B (f b) (f c) q

kerEquiv : (A B : U) (f : A -> B) -> equivalence A (kernel A B f)
kerEquiv A B f = (kerRef A B f,kerEucl A B f)