\import Category
\import Category.Limit
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Logic.Unique
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\open PrecatWithBprod

\type Subobj {C : Precat} (obj : C)
  => Quotient {Mono {C} { | cod => obj }} \lam m1 m2 => \Sigma (f : Hom m1.dom m2.dom) (m2.f ∘ f = m1.f) (g : Hom m2.dom m1.dom) (m1.f ∘ g = m2.f)

\func inso~ {C : Precat} {obj : C} (m : Mono {C} { | cod => obj }) : Subobj m.cod
  => in~ m

\instance SubobjPoset {C : Precat} (obj : C) : Poset (Subobj obj)
  | <= (s1 s2 : Subobj obj) : \Prop \with {
    | in~ m1, in~ m2 => ∃ (f : Hom m1.dom m2.dom) (m2.f ∘ f = m1.f)
    | in~ m, ~-equiv x y r => propExt (\lam (inP (f,xf=m)) => inP (r. ∘ f, inv o-assoc *> pmap (∘ _) r. *> xf=m))
                                      (\lam (inP (f,yf=m)) => inP (r. ∘ f, inv o-assoc *> pmap (∘ _) r. *> yf=m))
    | ~-equiv x y r, in~ m => propExt (\lam (inP (f,mf=x)) => inP (f ∘ r., inv o-assoc *> pmap (∘ _) mf=x *> r.))
                                      (\lam (inP (f,mf=y)) => inP (f ∘ r., inv o-assoc *> pmap (∘ _) mf=y *> r.))
  }
  | <=-refl {x} => \case \elim x \with {
    | in~ m => inP (id, id-right)
  }
  | <=-transitive {x} {y} {z} => \case \elim x, \elim y, \elim z, \elim __, \elim __ \with {
    | in~ m1, in~ m2, in~ m3, inP p, inP q => inP (q. ∘ p., inv o-assoc *> pmap (∘ _) q. *> p.)
  }
  | <=-antisymmetric {x} {y} => \case \elim x, \elim y, \elim __, \elim __ \with {
    | in~ m1, in~ m2, inP p, inP q => path \lam i => ~-equiv m1 m2 (p.,p.,q.,q.) i
  }
  \where {
    \lemma extractMap {obj : C} {f g : Mono {C} { | cod => obj }} (f<=g : inso~ f <= inso~ g) : \Sigma (h : Hom f.dom g.dom) (g.f ∘ h = f)
      => TruncP.remove (\lam p q => ext $ g.isMono $ p. *> inv q.) f<=g

    \func subobj-iso {obj : C} {f g : Mono {C} { | cod => obj }}
                     (f<=g : inso~ f <= inso~ g) (g<=f : inso~ g <= inso~ f) : Iso {C} {f.dom} {g.dom} \cowith
      | f => (SubobjPoset.extractMap f<=g).
      | hinv => (SubobjPoset.extractMap g<=f).
      | hinv_f => f.isMono $ inv o-assoc *> pmap (∘ _) (SubobjPoset.extractMap g<=f). *> (SubobjPoset.extractMap f<=g). *> inv id-right
      | f_hinv => g.isMono $ inv o-assoc *> pmap (∘ _) (SubobjPoset.extractMap f<=g). *> (SubobjPoset.extractMap g<=f). *> inv id-right
  }

\lemma ~-unsoequiv {C : Precat} {obj : C} {m1 m2 : Mono {C} { | cod => obj }} (p : inso~ m1 = inso~ m2)
  : ∃ (f : Hom m1.dom m2.dom) (m2.f ∘ f = m1.f) (g : Hom m2.dom m1.dom) (m1.f ∘ g = m2.f)
  => \case =_<= p, =_<= (inv p) \with {
    | inP r1, inP r2 => inP (r1.,r1.,r2.,r2.)
  }
  \where {
    \lemma left-right=id (r : \Sigma (f : Hom m1.dom m2.dom) (m2.f ∘ f = m1.f) (g : Hom m2.dom m1.dom) (m1.f ∘ g = m2.f)) : r. ∘ r. = id
      => m1.isMono $ inv o-assoc *> pmap (∘ _) r. *> r. *> inv id-right

    \lemma right-left=id (r : \Sigma (f : Hom m1.dom m2.dom) (m2.f ∘ f = m1.f) (g : Hom m2.dom m1.dom) (m1.f ∘ g = m2.f)) : r. ∘ r. = id
      => m2.isMono $ inv o-assoc *> pmap (∘ _) r. *> r. *> inv id-right
  }

\sfunc subobjTop {C : Precat} {obj : C} : Subobj obj
  => inso~ idIso

\instance SubobjectSemilattice {C : PrecatWithPullbacks} (obj : C) : TopMeetSemilattice
  | Poset => SubobjPoset obj
  | meet (x y : Subobj obj) : Subobj obj \with {
    | in~ m1, in~ m2 => inso~ $ Mono.comp m1 $ Mono_pullback (pullback m1.f m2.f) m2
    | in~ m, ~-equiv x y r => <=-antisymmetric
      (inP (pbMap pbProj1 (r. ∘ pbProj2) $ pbCoh *> pmap (∘ _) (inv r.) *> o-assoc, o-assoc *> pmap (_ ∘) pbBeta1))
      (inP (pbMap pbProj1 (r. ∘ pbProj2) $ pbCoh *> pmap (∘ _) (inv r.) *> o-assoc, o-assoc *> pmap (_ ∘) pbBeta1))
    | ~-equiv x y r, in~ m => <=-antisymmetric
      (inP (pbMap (r. ∘ pbProj1) pbProj2 $ inv o-assoc *> pmap (∘ _) r. *> pbCoh, o-assoc *> pmap (_ ∘) pbBeta1 *> inv o-assoc *> pmap (∘ _) r.))
      (inP (pbMap (r. ∘ pbProj1) pbProj2 $ inv o-assoc *> pmap (∘ _) r. *> pbCoh, o-assoc *> pmap (_ ∘) pbBeta1 *> inv o-assoc *> pmap (∘ _) r.))
  }
  | meet-left {x} {y} => \case \elim x, \elim y \with {
    | in~ m1, in~ m2 => inP (pbProj1, idp)
  }
  | meet-right {x} {y} => \case \elim x, \elim y \with {
    | in~ m1, in~ m2 => inP (pbProj2, inv pbCoh)
  }
  | meet-univ {x} {y} {z} => \case \elim x, \elim y, \elim z, \elim __, \elim __ \with {
    | in~ xm, in~ ym, in~ zm, inP z<=x, inP z<=y => inP (pbMap z<=x. z<=y. $ z<=x. *> inv z<=y., o-assoc *> pmap (_ ∘) pbBeta1 *> z<=x.)
  }
  | top => subobjTop
  | top-univ {x} => rewrite (\peval subobjTop {_} {obj}) \case \elim x \with {
    | in~ m => inP (m, id-left)
  }

\func subobjLifts {C : Precat} {x y : C} (f : Hom x y) (s : Subobj y) : \Prop \elim s
  | in~ m => ∃ (g : Hom x m.dom) (m.f ∘ g = f)
  | ~-equiv m1 m2 r => propExt
    (\lam (inP (g,p)) => inP (r. ∘ g, inv o-assoc *> pmap (∘ _) r. *> p))
    (\lam (inP (g,p)) => inP (r. ∘ g, inv o-assoc *> pmap (∘ _) r. *> p))
  \where {
    \func toMap {s : Subobj y} {m : Mono {C} { | cod => y}} (p : s = inso~ m) (l : subobjLifts f s) : \Sigma (g : Hom x m.dom) (m.f ∘ g = f) \elim p
      | idp => TruncP.remove (\lam s s' => ext $ m.isMono $ s. *> inv s'.) l
  }

\lemma subobjLifts_id_top {C : Precat} {x : C} {s : Subobj x} : subobjLifts id s <-> (s = subobjTop) \elim s
  | in~ m => rewrite (\peval subobjTop {_} {x}) (<=-antisymmetric $ inP (m, id-left), \lam r => =_<= (inv r))

\sfunc subobjEq {C : PrecatWithBprod} (c : C) : Subobj (Bprod c c)
  => inso~ diagonal-splitMono

\lemma subobjEq-lifts {C : PrecatWithBprod} {x c : C} {f g : Hom x c} : subobjLifts (pair f g) (subobjEq c) <-> (f = g)
  => rewrite (\peval subobjEq c)
    (\lam (inP (h,p)) => inv beta1 *> pmap (proj1 ∘) (inv p) *> inv o-assoc *> pmap (∘ h) (beta1 *> inv beta2) *> o-assoc *> pmap (proj2 ∘) p *> beta2,
     \lam p => inP (f, pair-unique (inv o-assoc *> pmap (∘ _) beta1 *> id-left *> inv beta1) (inv o-assoc *> pmap (∘ _) beta2 *> id-left *> p *> inv beta2)))

\func subobjPullback {C : PrecatWithPullbacks} {x y : C} (h : Hom x y) (s : Subobj y) : Subobj x \elim s
  | in~ m => inso~ $ Mono_pullback (pullback h m.f) m
  | ~-equiv m1 m2 r => <=-antisymmetric
    (inP (pbMap pbProj1 (r. ∘ pbProj2) $ pbCoh *> pmap (∘ _) (inv r.) *> o-assoc, pbBeta1))
    (inP (pbMap pbProj1 (r. ∘ pbProj2) $ pbCoh *> pmap (∘ _) (inv r.) *> o-assoc, pbBeta1))

\lemma subobjPullback-char {C : PrecatWithPullbacks} {s m : Mono {C}} {sub : Subobj s.cod} (p : sub = inso~ s) {h : Hom m.cod s.cod} (q : subobjPullback h sub = inso~ m)
  : Contr (Pullback h s.f m.dom m) \elim p
  | idp => \case ~-unsoequiv {_} {_} {Mono_pullback _ s} q \with {
    | inP r => \new Contr {
      | center => \new Pullback {
        | pbProj2 => pbProj2 ∘ r.
        | pbCoh => pmap (h ∘) (inv r.) *> inv o-assoc *> pmap (∘ _) pbCoh *> o-assoc
        | pbMap p1 p2 c => r. ∘ pbMap p1 p2 c
        | pbBeta1 => inv o-assoc *> pmap (∘ _) r. *> pbBeta1
        | pbBeta2 => o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) (~-unsoequiv.left-right=id {_} {_} {Mono_pullback _ s} r) *> id-left) *> pbBeta2
        | pbEta e _ => m.isMono e
      }
      | contraction P => exts (s.isMono $ inv o-assoc *> pmap (∘ _) (inv pbCoh) *> o-assoc *> pmap (_ ∘) r. *> pbCoh,
                               \lam p1 p2 c => m.isMono $ inv o-assoc *> pmap (∘ _) r. *> pbBeta1 *> inv P.pbBeta1)
    }
  }

\lemma subobjPullback-lifts {C : PrecatWithPullbacks} {x y z : C} {f : Hom x y} {g : Hom y z} {s : Subobj z}
  : subobjLifts f (subobjPullback g s) <-> subobjLifts (g ∘ f) s \elim s
  | in~ m => (\lam (inP (h,p)) => inP (pbProj2 ∘ h, inv o-assoc *> pmap (∘ h) (inv pbCoh) *> o-assoc *> pmap (g ∘) p),
              \lam (inP (h,p)) => inP (pbMap f h (inv p), pbBeta1))

\lemma subobjLifts_top {C : PrecatWithPullbacks} {x y : C} {f : Hom x y} {s : Subobj y}
  : subobjLifts f s <-> (subobjPullback f s = subobjTop)
  => transport (subobjLifts __ _ <-> _) id-right $ <->trans (<->sym subobjPullback-lifts) subobjLifts_id_top

\lemma subobjPullback_id {C : PrecatWithPullbacks} {x : C} {s : Subobj x}
  : subobjPullback id s = s \elim s
  | in~ m => <=-antisymmetric (inP (pbProj2, inv pbCoh *> id-left)) (inP (pbMap m id $ id-left *> inv id-right, pbBeta1))

\lemma subobjPullback_o {C : PrecatWithPullbacks} {x y z : C} {f : Hom x y} {g : Hom y z} {s : Subobj z}
  : subobjPullback (g ∘ f) s = subobjPullback f (subobjPullback g s) \elim s
  | in~ m => <=-antisymmetric
    (inP (pbMap pbProj1 (pbMap (f ∘ pbProj1) pbProj2 (inv o-assoc *> pbCoh)) (inv pbBeta1), pbBeta1))
    (inP (pbMap pbProj1 (pbProj2 ∘ pbProj2) $ o-assoc *> pmap (g ∘) pbCoh *> inv o-assoc *> pmap (∘ _) pbCoh *> o-assoc, pbBeta1))

\lemma subobjPullback-top {C : PrecatWithPullbacks} {x y : C} {f : Hom x y} {s : Subobj y} (p : s = inso~ idIso) : subobjPullback f s = inso~ idIso \elim p
  | idp => <=-antisymmetric (inP (pbProj1, id-left)) (inP (pbMap id f (id-right *> inv id-left), pbBeta1))

\lemma subobjPullback_top {C : PrecatWithPullbacks} {x y : C} {f : Hom x y} : subobjPullback f subobjTop = subobjTop
  => subobjPullback-top (\peval subobjTop {_} {y}) *> inv (\peval subobjTop {_} {x})

\lemma subobjPullback-self {C : PrecatWithPullbacks} {h : Mono {C}} {s : Subobj h.cod} (p : s = inso~ h) : subobjPullback h.f s = inso~ idIso \elim p
  | idp => <=-antisymmetric (inP (pbProj1, id-left)) (inP (pbMap id id idp, pbBeta1))

\func subobjPullback_Iso-equiv {C : PrecatWithPullbacks} (h : Iso {C}) : QEquiv {Subobj h.cod} {Subobj h.dom} \cowith
  | f => subobjPullback h.f
  | ret => subobjPullback h.hinv
  | ret_f s => inv subobjPullback_o *> pmap (subobjPullback __ s) h.f_hinv *> subobjPullback_id
  | f_sec s => inv subobjPullback_o *> pmap (subobjPullback __ s) h.hinv_f *> subobjPullback_id

\func subobjPullback_Iso {C : PrecatWithPullbacks} (h : Iso {C}) {s : Subobj h.cod} {m : Mono {C} { | cod => h.cod }} (p : s = inso~ m)
  : subobjPullback h.f s = inso~ (Mono.comp h.reverse m) \elim p
  | idp => <=-antisymmetric
    (inP (pbProj2, o-assoc *> pmap (_ ∘) (inv pbCoh) *> inv o-assoc *> pmap (∘ _) h.hinv_f *> id-left))
    (inP (pbMap (h.hinv ∘ m) id $ inv o-assoc *> pmap (∘ _) h.f_hinv *> id-left *> inv id-right, pbBeta1))