\import Algebra.Meta
\import Category
\import Category.Limit
\import Equiv
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\class WFS {\classifying C : Precat} (L R : \Pi {x y : C} -> Hom x y -> \Prop) {
  | factors {x z : C} (h : Hom x z) : \Sigma (y : C) (f : Hom x y) (g : Hom y z) (g ∘ f = h) (L f) (R g)
  | lift {a b c d : C} (t : Hom a c) (s : Hom b d) (f : Hom a b) (g : Hom c d)
    : g ∘ t = s ∘ f -> L f -> R g -> \Sigma (l : Hom b c) (l ∘ f = t) (g ∘ l = s)
  {- a --t-> c
     |    /  |
   f |   /l  | g
     |  /    |
     b --s-> d
  -}
} \where {
  \open PrecatWithBprod

  \lemma left-epi {C : CartesianPrecat} (w : WFS {C}) {x y : C} (f : Hom x y) (Lf : L f) {z : C} (Rd : R (diagonal z)) {g h : Hom y z} (p : g ∘ f = h ∘ f) : g = h
    => \have | (l,_,q) => lift (g ∘ f) (pair g h) f (diagonal z) (inv o-assoc *> pmap (∘ f) (pair-comp *> pmap2 pair id-left id-left) *> pair-comp *> pmap (pair _) p *> inv pair-comp) Lf Rd
             | l=g => inv (pmap (∘ l) beta1) *> o-assoc *> pmap (proj1 ∘) q *> beta1
             | l=h => inv (pmap (∘ l) beta2) *> o-assoc *> pmap (proj2 ∘) q *> beta2
       \in inv l=g *> l=h
}

\class OFS \extends WFS
  | unique-lift {a b c d : C} (f : Hom a b) (g : Hom c d)
    : L f -> R g -> IsEquiv {Hom b c} {\Sigma (t : Hom a c) (s : Hom b d) (g ∘ t = s ∘ f)} (\lam l => (l ∘ f, g ∘ l, inv o-assoc))
  | lift t s f g p Lf Rg =>
    \have q => IsEquiv.f_ret (unique-lift f g Lf Rg)
    \in (IsEquiv.ret (unique-lift f g Lf Rg) $ later (t,s,p), pmap __. q, pmap __. q)
  \where {
    \lemma liftFromMono {C : Precat} {a b c d : C} (f : Hom a b) (g : Hom c d) (m : Mono g) (l : \Pi (t : Hom a c) (s : Hom b d) -> g ∘ t = s ∘ f -> \Sigma (l : Hom b c) (g ∘ l = s))
      : IsEquiv {Hom b c} {\Sigma (t : Hom a c) (s : Hom b d) (g ∘ t = s ∘ f)} (\lam l => (l ∘ f, g ∘ l, inv o-assoc))
      => IsEquiv.fromInjSurj
        (\lam {l1} {l2} p => m.isMono (pmap __. p))
        (\lam (t,s,p) => inP ((l t s p)., ext (m.isMono (rewriteEq (l t s p). (inv p)), (l t s p).)))
  }