\import Category
\import Category.Limit
\import Category.Subobj
\import Equiv
\import Function.Meta
\import Logic
\import Meta
\import Order.PartialOrder
\import Paths
\import Relation.Equivalence

\func IsRegularSubobj.{o,h} {C : Precat.{o,h}} {obj : C} (s : Subobj obj) : \Prop \elim s
  | in~ m => IsRegularMono m.f
  | ~-equiv m1 m2 r =>
    \have lem {m1 m2 : Mono {C} { | cod => obj }} (m1<=m2 : inso~ m1 <= inso~ m2) (m2<=m1 : inso~ m2 <= inso~ m1) (m1r : IsRegularMono m1.f) : IsRegularMono m2.f => \case \elim m1<=m2, \elim m2<=m1, \elim m1r \with {
      | inP m1<=m2, inP m2<=m1, inP e => inP $ Equalizer.mono=>equalizer m2
        (pmap (_ ∘) (inv m2<=m1.) *> inv o-assoc *> pmap (∘ _) e.equal *> o-assoc *> pmap (_ ∘) m2<=m1.)
        \lam h hp => inP (m1<=m2. ∘ e.eqMap h hp, inv o-assoc *> pmap (∘ _) m1<=m2. *> e.eqBeta)
    }
    \in propExt (lem (inP (r.,r.)) (inP (r.,r.))) (lem (inP (r.,r.)) (inP (r.,r.)))

\lemma regularSubobj-meet.{o,h} {C : FinCompletePrecat.{o,h}} {obj : C} {s1 s2 : Subobj obj} (r1 : IsRegularSubobj s1) (r2 : IsRegularSubobj s2)
  : IsRegularSubobj (SubobjectSemilattice.meet s1 s2) \elim s1, s2
  | in~ m1, in~ m2 => pullback-isRegularMono r1 r2
  \where {
    \open PrecatWithBprod

    \lemma pullback-isRegularMono {C : CartesianPrecat} {P : Pullback {C}} (fm : IsRegularMono P.f) (gm : IsRegularMono P.g) : IsRegularMono (P.f ∘ pbProj1) \elim fm, gm
      | inP (fe : Equalizer) \as fm, inP (ge : Equalizer) \as gm => inP $ Equalizer.mono=>equalizer
        (Mono.comp (regularMono_Mono fm) (regularMono_Mono $ regularMono_pullback P gm))
        (pair-comp *> pmap2 pair (inv o-assoc *> pmap (∘ _) fe.equal *> o-assoc) (pmap (_ ∘) P.pbCoh *> inv o-assoc *> pmap (∘ _) ge.equal *> o-assoc *> pmap (_ ∘) (inv P.pbCoh)) *> inv pair-comp)
        \lam {w} h p =>
          \have | (inP (m1,q1)) => IsEquiv.isSurj (fe.isEqualizer w) $ later (h, pmap (∘ h) (inv beta1) *> o-assoc *> pmap (proj1 ∘) p *> inv o-assoc *> pmap (∘ h) beta1)
                | (inP (m2,q2)) => IsEquiv.isSurj (ge.isEqualizer w) $ later (h, pmap (∘ h) (inv beta2) *> o-assoc *> pmap (proj2 ∘) p *> inv o-assoc *> pmap (∘ h) beta2)
                | p1 => pmap __. q1
                | p2 => pmap __. q2
          \in inP (pbMap m1 m2 (p1 *> inv p2), o-assoc *> pmap (_ ∘) P.pbBeta1 *> p1)
  }