\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 __.1 q, pmap __.2 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).1, ext (m.isMono (rewriteEq (l t s p).2 (inv p)), (l t s p).2))
| Embedding => Embedding.fromInjection (\lam {l1} {l2} p => m.isMono (pmap __.2 p))
}
}