\import Category
\import Category.Limit
\import Equiv
\import Logic
\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) (pair-unique (rewriteEq (beta1 g h, beta1 (id z) (id z)) id-left) (rewriteEq (beta2 g h, beta2 (id z) (id z)) (id-left *> p))) Lf Rd
             | l=g => inv (pmap (`∘ l) (beta1 _ _)) *> o-assoc *> pmap (proj1 ∘) q *> beta1 g h
             | l=h => inv (pmap (`∘ l) (beta2 _ _)) *> o-assoc *> pmap (proj2 ∘) q *> beta2 g h
       \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
    -> Equiv {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 => Equiv.f_ret {unique-lift f g Lf Rg} (t,s,p)
    \in (ret {unique-lift f g Lf Rg} (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))
      : Equiv {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))
      => \new ESEquiv {
        | isSurjMap (t,s,p) => inP ((l t s p)., ext (m.isMono (rewriteEq (l t s p). (inv p)), (l t s p).))
        | Embedding => Embedding.fromInjection (\lam {l1} {l2} p => m.isMono (pmap __. p))
      }
  }