Library UniMath.CategoryTheory.ModelCategories.WFS
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Pushouts.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.Opp.
Require Import UniMath.CategoryTheory.ModelCategories.Retract.
Require Import UniMath.CategoryTheory.ModelCategories.MorphismClass.
Section wfs.
Local Open Scope cat.
Local Open Scope morcls.
Local Open Scope retract.
Definition lp {M : category} {a x e b : M} (i : a --> x) (p : e --> b) : UU :=
∏ (g : a --> e) (f : x --> b),
p ∘ g = f ∘ i -> ∃ l : x --> e, (l ∘ i = g) × (p ∘ l = f).
Definition isaprop_lp {M : category} {a b x y : M} (f : a --> b) (g : x --> y) : isaprop (lp f g).
Proof.
do 3 (apply impred_isaprop; intro).
apply propproperty.
Qed.
Definition lp_hProp {M : category} {a b x y : M} (f : a --> b) (g : x --> y) : hProp :=
make_hProp (lp f g) (isaprop_lp f g).
Definition llp {M : category} (R : morphism_class M) : (morphism_class M) :=
λ {a x : M} (i : a --> x), ∀ (e b : M) (p : e --> b), ((R _ _) p ⇒ lp_hProp i p)%logic.
Definition rlp {M : category} (L : morphism_class M) : (morphism_class M) :=
λ {e b : M} (p : e --> b), ∀ (a x : M) (i : a --> x), ((L _ _) i ⇒ lp_hProp i p)%logic.
Lemma llp_anti {M : category} {R R' : morphism_class M} (h : R ⊆ R') : llp R' ⊆ llp R.
Proof.
unfold "⊆" in *.
intros a x i H.
intros e b p K.
apply (H e b p).
apply (h e b p).
exact K.
Defined.
Lemma opp_rlp_is_llp_opp {M : category} (L : morphism_class M) :
morphism_class_opp (rlp L) = (llp (morphism_class_opp L)).
Proof.
apply morphism_class_subset_antisymm; intros a b f.
- intro rlpf.
intros x y g hg.
intros top bottom H.
use (rlpf _ _ (rm_opp_mor g)).
* exact hg.
* exact (rm_opp_mor bottom).
* exact (rm_opp_mor top).
* symmetry.
exact H.
*
intros hl.
destruct hl as [l [hlg hlf]].
apply hinhpr.
exists (opp_mor l).
split; assumption.
- intro rlpf.
intros x y g hg.
intros top bottom H.
use (rlpf _ _ (rm_opp_mor g)).
* exact hg.
* exact (rm_opp_mor bottom).
* exact (rm_opp_mor top).
* symmetry.
exact H.
* intro hl.
destruct hl as [l [hlg hlf]].
apply hinhpr.
exists (opp_mor l).
split; assumption.
Defined.
Lemma opp_llp_is_rlp_opp {M : category} (L : morphism_class M) :
morphism_class_opp (llp L) = rlp (morphism_class_opp L).
Proof.
rewrite <- (morphism_class_opp_opp (rlp _)).
rewrite (opp_rlp_is_llp_opp _).
trivial.
Defined.
Definition wfs_fact_ax {M : category} (L R : morphism_class M) :=
(∀ x y (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (L _ _) g × (R _ _) h × h ∘ g = f).
Definition is_wfs {M : category} (L R : morphism_class M) :=
(L = llp R) × (R = rlp L) × (wfs_fact_ax L R).
Definition make_is_wfs {M : category} {L R : morphism_class M}
(llp : L = llp R) (rlp : R = rlp L) (fact : wfs_fact_ax L R) : is_wfs L R :=
make_dirprod llp (make_dirprod rlp fact).
Definition wfs (M : category) :=
∑ (L R : morphism_class M), is_wfs L R.
Definition make_wfs {M : category} (L R : morphism_class M) (w : is_wfs L R) : wfs M :=
tpair _ L (tpair _ R w).
Definition wfs_L {M : category} (w : wfs M) := (pr1 w).
Definition wfs_R {M : category} (w : wfs M) := pr1 (pr2 w).
Definition is_wfs_llp {M : category} {L R : morphism_class M} (w : is_wfs L R) := pr1 w.
Definition is_wfs_rlp {M : category} {L R : morphism_class M} (w : is_wfs L R) := pr1 (pr2 w).
Definition is_wfs_fact {M : category} {L R : morphism_class M} (w : is_wfs L R) := pr2 (pr2 w).
Definition wfs_is_wfs {M : category} (w : wfs M) := pr2 (pr2 w).
Definition wfs_llp {M : category} (w : wfs M) := is_wfs_llp (wfs_is_wfs w).
Definition wfs_rlp {M : category} (w : wfs M) := is_wfs_rlp (wfs_is_wfs w).
Definition wfs_fact {M : category} (w : wfs M) := is_wfs_fact (wfs_is_wfs w).
Lemma isaprop_is_wfs {M : category} (L R : morphism_class M) : isaprop (is_wfs L R).
Proof.
apply isapropdirprod.
- unfold isaprop.
exact (isasetmorphism_class _ _).
- apply isapropdirprod.
* exact (isasetmorphism_class _ _).
* do 3 (apply impred_isaprop; intro).
apply propproperty.
Qed.
Lemma wfs'lp {M : category} (w : wfs M)
{a b x y} {f : a --> b} {g : x --> y} (hf : (wfs_L w _ _) f) (hg : (wfs_R w _ _) g) : lp_hProp f g.
Proof.
unfold wfs_L in hf.
rewrite (wfs_llp w) in hf.
exact (hf _ _ _ hg).
Defined.
Lemma wfs_L_retract {M : category} (w : wfs M)
{a b a' b'} {f : a --> b} {f' : a' --> b'} (r : retract f f') (hf : (wfs_L w _ _) f) : (wfs_L w _ _) f'.
Proof.
destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]].
unfold wfs_L.
rewrite (wfs_llp w).
intros x y g hg h k s.
use (wfs'lp w hf hg (h ∘ ra) (k ∘ rb) _).
{
rewrite <- assoc, s, assoc, assoc, hr.
reflexivity.
}
intro hl.
destruct hl as [l [hlh hlk]].
apply hinhpr.
exists (l ∘ ib).
split.
* rewrite assoc, <- hi, <- assoc, hlh, assoc, ha, id_left.
reflexivity.
* rewrite <- assoc, hlk, assoc, hb, id_left.
reflexivity.
Defined.
Lemma llp_rlp_self {M : category} (L : morphism_class M) : L ⊆ llp (rlp L).
Proof.
intros a b f hf x y g hg.
apply (hg _ _ _).
exact hf.
Defined.
Lemma rlp_llp_self {M : category} (L : morphism_class M) : L ⊆ rlp (llp L).
Proof.
intros a b f hf x y g hg.
apply (hg _ _ _).
exact hf.
Defined.
Lemma wfs_of_factorization {M : category} (I : morphism_class M)
(h : ∀ (x y : M) (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (llp (rlp I) _ _ g) × (rlp I _ _ h) × (h ∘ g = f)) :
is_wfs (llp (rlp I)) (rlp I).
Proof.
use make_is_wfs.
- trivial.
- apply morphism_class_subset_antisymm; intros x y g hg.
* exact (rlp_llp_self _ _ _ _ hg).
* intros a b f hf.
apply (hg _ _ _).
exact (llp_rlp_self _ _ _ _ hf).
- exact h.
Defined.
Lemma retract_argument {M : category} {L' : morphism_class M} (w : wfs M)
(H : ∀ x y (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (L' _ _) g × (wfs_R w _ _) h × h ∘ g = f) :
∏ (a b : M) (f : a --> b), (wfs_L w _ _) f -> ∃ x' y' (f' : x' --> y') (r : retract f' f), (L' _ _) f'.
Proof.
intros a b f hf.
specialize (H _ _ f) as eHf.
simpl in eHf.
use (hinhuniv _ eHf).
intro Hf.
destruct Hf as [z [g [h [hg [hh hgh]]]]].
use (wfs'lp w hf hh g (identity _)).
{
rewrite hgh, id_right.
reflexivity.
}
intro hl.
destruct hl as [l [hl1 hl2]].
assert (r : retract g f).
{
use (make_retract (identity a) (identity a) l h).
use make_is_retract.
- now rewrite id_left.
- assumption.
- rewrite id_left. now symmetry.
- rewrite id_left. now symmetry.
}
apply hinhpr.
exists a, z, g, r.
exact hg.
Defined.
Lemma lp_isos_univ {M : category} {a b x y : M} (f : a --> b) (g : x --> y) :
(morphism_class_isos M _ _ f) -> lp f g.
Proof.
intro H.
set (fiso := make_iso _ H).
change (lp fiso g).
intros h k s.
apply hinhpr.
exists (h ∘ (inv_from_iso fiso)).
split.
* rewrite assoc, iso_inv_after_iso, id_left.
reflexivity.
* rewrite <- assoc, s, assoc.
rewrite iso_after_iso_inv, id_left.
reflexivity.
Defined.
Lemma lp_univ_isos {M : category} {a b x y : M} (f : a --> b) (g : x --> y) :
(morphism_class_isos M _ _ f) -> lp g f.
Proof.
intro H.
set (fiso := make_iso _ H).
change (lp g fiso).
intros h k s.
apply hinhpr.
exists ((inv_from_iso fiso) ∘ k).
split.
* rewrite assoc, <- s, <- assoc, iso_inv_after_iso, id_right.
reflexivity.
* rewrite <- assoc, iso_after_iso_inv, id_right.
reflexivity.
Defined.
Lemma llp_univ {M : category} : llp (morphism_class_univ M) = morphism_class_isos M.
Proof.
apply morphism_class_subset_antisymm; intros a b f H.
-
specialize ((H _ _ f) tt).
use (H (identity _) (identity _)).
{
rewrite id_left, id_right.
reflexivity.
}
intro hl.
destruct hl as [l [hfl hlf]].
unfold morphism_class_isos.
assert (is_z_isomorphism f) as f_z_iso.
{
exists l.
split; assumption.
}
apply is_iso_from_is_z_iso.
exact f_z_iso.
- intros x y g _.
exact (lp_isos_univ f g H).
Defined.
Lemma rlp_isos {M : category} : rlp (morphism_class_isos M) = morphism_class_univ M.
Proof.
apply morphism_class_subset_antisymm.
-
intros x y g H.
unfold morphism_class_univ.
exact tt.
-
rewrite <- llp_univ.
exact (rlp_llp_self _).
Defined.
Lemma wfs_isos_univ {M : category} : is_wfs (morphism_class_isos M) (morphism_class_univ M).
Proof.
use make_is_wfs; try symmetry.
- exact llp_univ.
- exact rlp_isos.
-
intros x y f.
apply hinhpr.
exists x, (identity x), f.
repeat split.
* exact (identity_is_iso M x).
* rewrite id_left.
reflexivity.
Defined.
Definition opp_is_wfs {M : category} {L R : morphism_class M} (w : is_wfs L R) : is_wfs (morphism_class_opp R) (morphism_class_opp L).
Proof.
use make_is_wfs.
- rewrite (is_wfs_rlp w).
exact (opp_rlp_is_llp_opp _).
- rewrite (is_wfs_llp w).
exact (opp_llp_is_rlp_opp _).
- intros x y f.
specialize ((is_wfs_fact w) _ _ (rm_opp_mor f)) as test.
simpl in test.
use (hinhuniv _ test).
intro H.
destruct H as [z [g [h [? [? ?]]]]].
apply hinhpr.
exists (opp_ob z), (opp_mor h), (opp_mor g).
repeat split; assumption.
Defined.
Definition opp_wfs {M : category} (w : wfs M) : wfs (op_cat M).
Proof.
exists (morphism_class_opp (wfs_R w)), (morphism_class_opp (wfs_L w)).
exact (opp_is_wfs (wfs_is_wfs w)).
Defined.
Lemma wfs_L_contains_isos {M : category} (w : wfs M) : (morphism_class_isos M) ⊆ (wfs_L w).
Proof.
rewrite <- llp_univ.
unfold wfs_L.
rewrite (wfs_llp w).
apply llp_anti.
intros x y f hf.
exact tt.
Defined.
Lemma wfs_R_contains_isos {M : category} (w : wfs M) : (morphism_class_isos M) ⊆ (wfs_R w).
Proof.
intros x y f hf.
set (opp_containment := wfs_L_contains_isos (opp_wfs w)).
exact (opp_containment _ _ (opp_mor f) (opp_is_iso _ hf)).
Defined.
Lemma wfs_R_retract {M : category} (w : wfs M)
{a b a' b'} {f : a --> b} {f' : a' --> b'} (r : retract f f') (hf : (wfs_R w _ _) f) : (wfs_R w _ _) f'.
Proof.
use (wfs_L_retract (opp_wfs w) (opp_retract r)).
exact hf.
Defined.
Lemma wfs_closed_pullbacks {M : category} (w : wfs M)
{x y z : M} {p : x --> y} {f : z --> y} (Pb : Pullback f p) : ((wfs_R w _ _) p) -> ((wfs_R w _ _) (PullbackPr1 Pb)).
Proof.
intro p_r.
destruct Pb as [[zfx [f'p p2]] [H isPb]].
simpl in *.
cbn.
unfold wfs_R.
rewrite (wfs_rlp w).
intros a b i i_l.
intros p1 g Hp1g.
unfold wfs_R in p_r.
rewrite (wfs_rlp w) in p_r.
use (p_r _ _ i i_l (p2 ∘ p1) (f ∘ g) _).
{
rewrite <- assoc, <- H, assoc, Hp1g, assoc.
reflexivity.
}
intro hl.
destruct hl as [l [hl1 hl2]].
symmetry in hl2.
destruct (isPb _ g l hl2) as [[gh [hgh1 hgh2]] _].
apply hinhpr.
exists gh.
split.
-
apply (MorphismsIntoPullbackEqual isPb).
* rewrite <-assoc, hgh1, Hp1g.
reflexivity.
* rewrite <- assoc, hgh2, hl1.
reflexivity.
-
exact hgh1.
Defined.
Lemma wfs_closed_pushouts {M : category} (w : wfs M)
{x y z : M} {p : x --> y} {f : x --> z} (Po : Pushout f p) : ((wfs_L w _ _) p) -> ((wfs_L w _ _) (PushoutIn1 Po)).
Proof.
apply (wfs_closed_pullbacks (opp_wfs w)).
Defined.
Lemma wfs_closed_coproducts
(aoc : AxiomOfChoice)
{I : hSet} {M : category} (w : wfs M)
{a b : I -> M} {f : ∏ (i : I), a i --> b i} (hf : ∀ (i : I), (wfs_L w _ _) (f i))
(CCa : Coproduct _ _ a) (CCb : Coproduct _ _ b) :
(wfs_L w _ _) (CoproductOfArrows _ _ CCa CCb f).
Proof.
unfold wfs_L in *.
rewrite (wfs_llp w) in *.
intros x y g hg.
intros h k s.
set (hi := λ i, h ∘ (CoproductIn _ _ CCa i)).
set (ki := λ i, k ∘ (CoproductIn _ _ CCb i)).
assert (∏ i, ∃ li, (li ∘ (f i) = hi i) × (g ∘ li = ki i)) as ilift.
{
intro i.
specialize (hf i _ _ g hg) as H.
specialize (H (hi i) (ki i)).
use H.
unfold hi, ki.
rewrite <- assoc, s, assoc, assoc.
now rewrite (CoproductOfArrowsIn _ _).
}
assert (∥∏ i, ∑ li, (li ∘ (f i) = hi i) × (g ∘ li = ki i)∥) as ilift_aoc.
{
set (aocI := aoc I).
simpl in aocI.
apply (aocI).
exact ilift.
}
assert (∃ (li : (∏ i, (b i --> x))), (∏ i, (li i) ∘ (f i) = hi i × (g ∘ (li i) = ki i))) as ilifts.
{
use (hinhuniv _ ilift_aoc).
intro ilift_aoc_sig.
apply hinhpr.
use tpair.
- intro i.
set (li := ilift_aoc_sig i).
destruct li as [l hl].
exact l.
- intro i.
set (li := ilift_aoc_sig i).
simpl.
destruct li as [l hl].
exact hl.
}
use (hinhuniv _ ilifts).
intro ilift_sig.
destruct ilift_sig as [li hli].
set (hl := isCoproduct_Coproduct _ _ CCb x li).
destruct hl as [[l hl] uniqueness].
apply hinhpr.
exists l.
split; rewrite CoproductArrowEta, (CoproductArrowEta _ _ _ _ _ l).
-
rewrite (precompWithCoproductArrow).
apply CoproductArrowUnique.
intro i.
rewrite CoproductInCommutes.
destruct (hli i) as [hlicomm _].
change (CoproductIn _ _ _ _ · h) with (hi i).
rewrite (hl i).
exact hlicomm.
-
apply CoproductArrowUnique.
intro i.
rewrite assoc.
rewrite CoproductInCommutes.
destruct (hli i) as [_ klicomm].
change (CoproductIn _ _ _ _ · k) with (ki i).
rewrite (hl i).
exact klicomm.
Qed.
Lemma wfs_closed_products
(aoc : AxiomOfChoice)
{I : hSet} {M : category} (w : wfs M)
{a b : I -> M} {f : ∏ (i : I), b i --> a i} (hf : ∀ (i : I), (wfs_R w _ _) (f i))
(CCa : Product _ _ a) (CCb : Product _ _ b) :
(wfs_R w _ _) (ProductOfArrows _ _ CCa CCb f).
Proof.
apply (wfs_closed_coproducts aoc (opp_wfs w)).
exact hf.
Defined.
Definition wfs_llp' {M : category} (w : wfs M) : (morphism_class M) :=
λ {x y : M} (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h ∘ g = f × lp_hProp g f.
Definition wfs_rlp' {M : category} (w : wfs M) : (morphism_class M) :=
λ {x y : M} (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h ∘ g = f × lp_hProp f h.
Lemma llp_iff_lift_with_R {M : category} (w : wfs M) {x y : M} (f : x --> y) : (wfs_llp' w _ _) f <-> (wfs_R w _ _) f.
Proof.
split.
- intro hf.
unfold wfs_R.
rewrite (wfs_rlp w).
intros a b g hg.
intros top bottom comm_total.
use hf.
intro h.
destruct h as [Mf [lf [rf [lf_l [rf_r [fact lp_lff]]]]]].
use (lp_lff (identity _) rf).
{
rewrite id_left.
now symmetry.
}
intro H.
destruct H as [lift_lff [comm_lff1 comm_lff2]].
assert (lp_hProp g rf) as lp_grf.
{
unfold wfs_R in rf_r.
rewrite (wfs_rlp) in rf_r.
exact (rf_r _ _ g hg).
}
use (lp_grf (lf ∘ top) bottom).
{
rewrite <- assoc, fact.
exact comm_total.
}
intro H.
destruct H as [lift_grf [comm_grf1 comm_grf2]].
apply hinhpr.
exists (lift_lff ∘ lift_grf).
split.
* rewrite assoc, comm_grf1, <- assoc, comm_lff1, id_right.
reflexivity.
* rewrite <- assoc, comm_lff2.
exact comm_grf2.
-
intro hf.
use (wfs_fact w _ _ f).
intro h.
destruct h as [z [g [h [g_l [h_r comp]]]]].
apply hinhpr.
exists z, g, h.
repeat split; try assumption.
unfold wfs_R in hf.
rewrite wfs_rlp in hf.
exact (hf _ _ _ g_l).
Defined.
Lemma lp_of_retracts {M : category} {a b x y a' b' x' y' : M}
{f : a --> b} {f' : a' --> b'}
{g : x --> y} {g' : x' --> y'}
(rf : retract f' f) (rg : retract g' g) :
(lp f' g') -> (lp f g).
Proof.
intros Hlp h k Hcomm.
destruct rf as [ia [ra [ib [rb [ha [hb [hif hrf]]]]]]].
destruct rg as [ix [rx [iy [ry [hx [hy [hig hrg]]]]]]].
use Hlp.
- exact (ra · h · ix).
- exact (rb · k · iy).
- rewrite <- assoc, hig, assoc, <- (assoc _ h g), Hcomm, assoc, hrf, assoc, assoc.
reflexivity.
- intro Hl.
destruct Hl as [l [H1 H2]].
apply hinhpr.
exists (ib · l · rx).
split.
* rewrite assoc, assoc, <- hif, <- (assoc _ f' l), H1, assoc, assoc.
now rewrite ha, id_left, <- assoc, hx, id_right.
* rewrite <- assoc, hrg, assoc, <- (assoc _ l g'), H2, assoc, assoc.
now rewrite hb, id_left, <- assoc, hy, id_right.
Defined.
End wfs.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Pushouts.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.Opp.
Require Import UniMath.CategoryTheory.ModelCategories.Retract.
Require Import UniMath.CategoryTheory.ModelCategories.MorphismClass.
Section wfs.
Local Open Scope cat.
Local Open Scope morcls.
Local Open Scope retract.
Definition lp {M : category} {a x e b : M} (i : a --> x) (p : e --> b) : UU :=
∏ (g : a --> e) (f : x --> b),
p ∘ g = f ∘ i -> ∃ l : x --> e, (l ∘ i = g) × (p ∘ l = f).
Definition isaprop_lp {M : category} {a b x y : M} (f : a --> b) (g : x --> y) : isaprop (lp f g).
Proof.
do 3 (apply impred_isaprop; intro).
apply propproperty.
Qed.
Definition lp_hProp {M : category} {a b x y : M} (f : a --> b) (g : x --> y) : hProp :=
make_hProp (lp f g) (isaprop_lp f g).
Definition llp {M : category} (R : morphism_class M) : (morphism_class M) :=
λ {a x : M} (i : a --> x), ∀ (e b : M) (p : e --> b), ((R _ _) p ⇒ lp_hProp i p)%logic.
Definition rlp {M : category} (L : morphism_class M) : (morphism_class M) :=
λ {e b : M} (p : e --> b), ∀ (a x : M) (i : a --> x), ((L _ _) i ⇒ lp_hProp i p)%logic.
Lemma llp_anti {M : category} {R R' : morphism_class M} (h : R ⊆ R') : llp R' ⊆ llp R.
Proof.
unfold "⊆" in *.
intros a x i H.
intros e b p K.
apply (H e b p).
apply (h e b p).
exact K.
Defined.
Lemma opp_rlp_is_llp_opp {M : category} (L : morphism_class M) :
morphism_class_opp (rlp L) = (llp (morphism_class_opp L)).
Proof.
apply morphism_class_subset_antisymm; intros a b f.
- intro rlpf.
intros x y g hg.
intros top bottom H.
use (rlpf _ _ (rm_opp_mor g)).
* exact hg.
* exact (rm_opp_mor bottom).
* exact (rm_opp_mor top).
* symmetry.
exact H.
*
intros hl.
destruct hl as [l [hlg hlf]].
apply hinhpr.
exists (opp_mor l).
split; assumption.
- intro rlpf.
intros x y g hg.
intros top bottom H.
use (rlpf _ _ (rm_opp_mor g)).
* exact hg.
* exact (rm_opp_mor bottom).
* exact (rm_opp_mor top).
* symmetry.
exact H.
* intro hl.
destruct hl as [l [hlg hlf]].
apply hinhpr.
exists (opp_mor l).
split; assumption.
Defined.
Lemma opp_llp_is_rlp_opp {M : category} (L : morphism_class M) :
morphism_class_opp (llp L) = rlp (morphism_class_opp L).
Proof.
rewrite <- (morphism_class_opp_opp (rlp _)).
rewrite (opp_rlp_is_llp_opp _).
trivial.
Defined.
Definition wfs_fact_ax {M : category} (L R : morphism_class M) :=
(∀ x y (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (L _ _) g × (R _ _) h × h ∘ g = f).
Definition is_wfs {M : category} (L R : morphism_class M) :=
(L = llp R) × (R = rlp L) × (wfs_fact_ax L R).
Definition make_is_wfs {M : category} {L R : morphism_class M}
(llp : L = llp R) (rlp : R = rlp L) (fact : wfs_fact_ax L R) : is_wfs L R :=
make_dirprod llp (make_dirprod rlp fact).
Definition wfs (M : category) :=
∑ (L R : morphism_class M), is_wfs L R.
Definition make_wfs {M : category} (L R : morphism_class M) (w : is_wfs L R) : wfs M :=
tpair _ L (tpair _ R w).
Definition wfs_L {M : category} (w : wfs M) := (pr1 w).
Definition wfs_R {M : category} (w : wfs M) := pr1 (pr2 w).
Definition is_wfs_llp {M : category} {L R : morphism_class M} (w : is_wfs L R) := pr1 w.
Definition is_wfs_rlp {M : category} {L R : morphism_class M} (w : is_wfs L R) := pr1 (pr2 w).
Definition is_wfs_fact {M : category} {L R : morphism_class M} (w : is_wfs L R) := pr2 (pr2 w).
Definition wfs_is_wfs {M : category} (w : wfs M) := pr2 (pr2 w).
Definition wfs_llp {M : category} (w : wfs M) := is_wfs_llp (wfs_is_wfs w).
Definition wfs_rlp {M : category} (w : wfs M) := is_wfs_rlp (wfs_is_wfs w).
Definition wfs_fact {M : category} (w : wfs M) := is_wfs_fact (wfs_is_wfs w).
Lemma isaprop_is_wfs {M : category} (L R : morphism_class M) : isaprop (is_wfs L R).
Proof.
apply isapropdirprod.
- unfold isaprop.
exact (isasetmorphism_class _ _).
- apply isapropdirprod.
* exact (isasetmorphism_class _ _).
* do 3 (apply impred_isaprop; intro).
apply propproperty.
Qed.
Lemma wfs'lp {M : category} (w : wfs M)
{a b x y} {f : a --> b} {g : x --> y} (hf : (wfs_L w _ _) f) (hg : (wfs_R w _ _) g) : lp_hProp f g.
Proof.
unfold wfs_L in hf.
rewrite (wfs_llp w) in hf.
exact (hf _ _ _ hg).
Defined.
Lemma wfs_L_retract {M : category} (w : wfs M)
{a b a' b'} {f : a --> b} {f' : a' --> b'} (r : retract f f') (hf : (wfs_L w _ _) f) : (wfs_L w _ _) f'.
Proof.
destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]].
unfold wfs_L.
rewrite (wfs_llp w).
intros x y g hg h k s.
use (wfs'lp w hf hg (h ∘ ra) (k ∘ rb) _).
{
rewrite <- assoc, s, assoc, assoc, hr.
reflexivity.
}
intro hl.
destruct hl as [l [hlh hlk]].
apply hinhpr.
exists (l ∘ ib).
split.
* rewrite assoc, <- hi, <- assoc, hlh, assoc, ha, id_left.
reflexivity.
* rewrite <- assoc, hlk, assoc, hb, id_left.
reflexivity.
Defined.
Lemma llp_rlp_self {M : category} (L : morphism_class M) : L ⊆ llp (rlp L).
Proof.
intros a b f hf x y g hg.
apply (hg _ _ _).
exact hf.
Defined.
Lemma rlp_llp_self {M : category} (L : morphism_class M) : L ⊆ rlp (llp L).
Proof.
intros a b f hf x y g hg.
apply (hg _ _ _).
exact hf.
Defined.
Lemma wfs_of_factorization {M : category} (I : morphism_class M)
(h : ∀ (x y : M) (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (llp (rlp I) _ _ g) × (rlp I _ _ h) × (h ∘ g = f)) :
is_wfs (llp (rlp I)) (rlp I).
Proof.
use make_is_wfs.
- trivial.
- apply morphism_class_subset_antisymm; intros x y g hg.
* exact (rlp_llp_self _ _ _ _ hg).
* intros a b f hf.
apply (hg _ _ _).
exact (llp_rlp_self _ _ _ _ hf).
- exact h.
Defined.
Lemma retract_argument {M : category} {L' : morphism_class M} (w : wfs M)
(H : ∀ x y (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (L' _ _) g × (wfs_R w _ _) h × h ∘ g = f) :
∏ (a b : M) (f : a --> b), (wfs_L w _ _) f -> ∃ x' y' (f' : x' --> y') (r : retract f' f), (L' _ _) f'.
Proof.
intros a b f hf.
specialize (H _ _ f) as eHf.
simpl in eHf.
use (hinhuniv _ eHf).
intro Hf.
destruct Hf as [z [g [h [hg [hh hgh]]]]].
use (wfs'lp w hf hh g (identity _)).
{
rewrite hgh, id_right.
reflexivity.
}
intro hl.
destruct hl as [l [hl1 hl2]].
assert (r : retract g f).
{
use (make_retract (identity a) (identity a) l h).
use make_is_retract.
- now rewrite id_left.
- assumption.
- rewrite id_left. now symmetry.
- rewrite id_left. now symmetry.
}
apply hinhpr.
exists a, z, g, r.
exact hg.
Defined.
Lemma lp_isos_univ {M : category} {a b x y : M} (f : a --> b) (g : x --> y) :
(morphism_class_isos M _ _ f) -> lp f g.
Proof.
intro H.
set (fiso := make_iso _ H).
change (lp fiso g).
intros h k s.
apply hinhpr.
exists (h ∘ (inv_from_iso fiso)).
split.
* rewrite assoc, iso_inv_after_iso, id_left.
reflexivity.
* rewrite <- assoc, s, assoc.
rewrite iso_after_iso_inv, id_left.
reflexivity.
Defined.
Lemma lp_univ_isos {M : category} {a b x y : M} (f : a --> b) (g : x --> y) :
(morphism_class_isos M _ _ f) -> lp g f.
Proof.
intro H.
set (fiso := make_iso _ H).
change (lp g fiso).
intros h k s.
apply hinhpr.
exists ((inv_from_iso fiso) ∘ k).
split.
* rewrite assoc, <- s, <- assoc, iso_inv_after_iso, id_right.
reflexivity.
* rewrite <- assoc, iso_after_iso_inv, id_right.
reflexivity.
Defined.
Lemma llp_univ {M : category} : llp (morphism_class_univ M) = morphism_class_isos M.
Proof.
apply morphism_class_subset_antisymm; intros a b f H.
-
specialize ((H _ _ f) tt).
use (H (identity _) (identity _)).
{
rewrite id_left, id_right.
reflexivity.
}
intro hl.
destruct hl as [l [hfl hlf]].
unfold morphism_class_isos.
assert (is_z_isomorphism f) as f_z_iso.
{
exists l.
split; assumption.
}
apply is_iso_from_is_z_iso.
exact f_z_iso.
- intros x y g _.
exact (lp_isos_univ f g H).
Defined.
Lemma rlp_isos {M : category} : rlp (morphism_class_isos M) = morphism_class_univ M.
Proof.
apply morphism_class_subset_antisymm.
-
intros x y g H.
unfold morphism_class_univ.
exact tt.
-
rewrite <- llp_univ.
exact (rlp_llp_self _).
Defined.
Lemma wfs_isos_univ {M : category} : is_wfs (morphism_class_isos M) (morphism_class_univ M).
Proof.
use make_is_wfs; try symmetry.
- exact llp_univ.
- exact rlp_isos.
-
intros x y f.
apply hinhpr.
exists x, (identity x), f.
repeat split.
* exact (identity_is_iso M x).
* rewrite id_left.
reflexivity.
Defined.
Definition opp_is_wfs {M : category} {L R : morphism_class M} (w : is_wfs L R) : is_wfs (morphism_class_opp R) (morphism_class_opp L).
Proof.
use make_is_wfs.
- rewrite (is_wfs_rlp w).
exact (opp_rlp_is_llp_opp _).
- rewrite (is_wfs_llp w).
exact (opp_llp_is_rlp_opp _).
- intros x y f.
specialize ((is_wfs_fact w) _ _ (rm_opp_mor f)) as test.
simpl in test.
use (hinhuniv _ test).
intro H.
destruct H as [z [g [h [? [? ?]]]]].
apply hinhpr.
exists (opp_ob z), (opp_mor h), (opp_mor g).
repeat split; assumption.
Defined.
Definition opp_wfs {M : category} (w : wfs M) : wfs (op_cat M).
Proof.
exists (morphism_class_opp (wfs_R w)), (morphism_class_opp (wfs_L w)).
exact (opp_is_wfs (wfs_is_wfs w)).
Defined.
Lemma wfs_L_contains_isos {M : category} (w : wfs M) : (morphism_class_isos M) ⊆ (wfs_L w).
Proof.
rewrite <- llp_univ.
unfold wfs_L.
rewrite (wfs_llp w).
apply llp_anti.
intros x y f hf.
exact tt.
Defined.
Lemma wfs_R_contains_isos {M : category} (w : wfs M) : (morphism_class_isos M) ⊆ (wfs_R w).
Proof.
intros x y f hf.
set (opp_containment := wfs_L_contains_isos (opp_wfs w)).
exact (opp_containment _ _ (opp_mor f) (opp_is_iso _ hf)).
Defined.
Lemma wfs_R_retract {M : category} (w : wfs M)
{a b a' b'} {f : a --> b} {f' : a' --> b'} (r : retract f f') (hf : (wfs_R w _ _) f) : (wfs_R w _ _) f'.
Proof.
use (wfs_L_retract (opp_wfs w) (opp_retract r)).
exact hf.
Defined.
Lemma wfs_closed_pullbacks {M : category} (w : wfs M)
{x y z : M} {p : x --> y} {f : z --> y} (Pb : Pullback f p) : ((wfs_R w _ _) p) -> ((wfs_R w _ _) (PullbackPr1 Pb)).
Proof.
intro p_r.
destruct Pb as [[zfx [f'p p2]] [H isPb]].
simpl in *.
cbn.
unfold wfs_R.
rewrite (wfs_rlp w).
intros a b i i_l.
intros p1 g Hp1g.
unfold wfs_R in p_r.
rewrite (wfs_rlp w) in p_r.
use (p_r _ _ i i_l (p2 ∘ p1) (f ∘ g) _).
{
rewrite <- assoc, <- H, assoc, Hp1g, assoc.
reflexivity.
}
intro hl.
destruct hl as [l [hl1 hl2]].
symmetry in hl2.
destruct (isPb _ g l hl2) as [[gh [hgh1 hgh2]] _].
apply hinhpr.
exists gh.
split.
-
apply (MorphismsIntoPullbackEqual isPb).
* rewrite <-assoc, hgh1, Hp1g.
reflexivity.
* rewrite <- assoc, hgh2, hl1.
reflexivity.
-
exact hgh1.
Defined.
Lemma wfs_closed_pushouts {M : category} (w : wfs M)
{x y z : M} {p : x --> y} {f : x --> z} (Po : Pushout f p) : ((wfs_L w _ _) p) -> ((wfs_L w _ _) (PushoutIn1 Po)).
Proof.
apply (wfs_closed_pullbacks (opp_wfs w)).
Defined.
Lemma wfs_closed_coproducts
(aoc : AxiomOfChoice)
{I : hSet} {M : category} (w : wfs M)
{a b : I -> M} {f : ∏ (i : I), a i --> b i} (hf : ∀ (i : I), (wfs_L w _ _) (f i))
(CCa : Coproduct _ _ a) (CCb : Coproduct _ _ b) :
(wfs_L w _ _) (CoproductOfArrows _ _ CCa CCb f).
Proof.
unfold wfs_L in *.
rewrite (wfs_llp w) in *.
intros x y g hg.
intros h k s.
set (hi := λ i, h ∘ (CoproductIn _ _ CCa i)).
set (ki := λ i, k ∘ (CoproductIn _ _ CCb i)).
assert (∏ i, ∃ li, (li ∘ (f i) = hi i) × (g ∘ li = ki i)) as ilift.
{
intro i.
specialize (hf i _ _ g hg) as H.
specialize (H (hi i) (ki i)).
use H.
unfold hi, ki.
rewrite <- assoc, s, assoc, assoc.
now rewrite (CoproductOfArrowsIn _ _).
}
assert (∥∏ i, ∑ li, (li ∘ (f i) = hi i) × (g ∘ li = ki i)∥) as ilift_aoc.
{
set (aocI := aoc I).
simpl in aocI.
apply (aocI).
exact ilift.
}
assert (∃ (li : (∏ i, (b i --> x))), (∏ i, (li i) ∘ (f i) = hi i × (g ∘ (li i) = ki i))) as ilifts.
{
use (hinhuniv _ ilift_aoc).
intro ilift_aoc_sig.
apply hinhpr.
use tpair.
- intro i.
set (li := ilift_aoc_sig i).
destruct li as [l hl].
exact l.
- intro i.
set (li := ilift_aoc_sig i).
simpl.
destruct li as [l hl].
exact hl.
}
use (hinhuniv _ ilifts).
intro ilift_sig.
destruct ilift_sig as [li hli].
set (hl := isCoproduct_Coproduct _ _ CCb x li).
destruct hl as [[l hl] uniqueness].
apply hinhpr.
exists l.
split; rewrite CoproductArrowEta, (CoproductArrowEta _ _ _ _ _ l).
-
rewrite (precompWithCoproductArrow).
apply CoproductArrowUnique.
intro i.
rewrite CoproductInCommutes.
destruct (hli i) as [hlicomm _].
change (CoproductIn _ _ _ _ · h) with (hi i).
rewrite (hl i).
exact hlicomm.
-
apply CoproductArrowUnique.
intro i.
rewrite assoc.
rewrite CoproductInCommutes.
destruct (hli i) as [_ klicomm].
change (CoproductIn _ _ _ _ · k) with (ki i).
rewrite (hl i).
exact klicomm.
Qed.
Lemma wfs_closed_products
(aoc : AxiomOfChoice)
{I : hSet} {M : category} (w : wfs M)
{a b : I -> M} {f : ∏ (i : I), b i --> a i} (hf : ∀ (i : I), (wfs_R w _ _) (f i))
(CCa : Product _ _ a) (CCb : Product _ _ b) :
(wfs_R w _ _) (ProductOfArrows _ _ CCa CCb f).
Proof.
apply (wfs_closed_coproducts aoc (opp_wfs w)).
exact hf.
Defined.
Definition wfs_llp' {M : category} (w : wfs M) : (morphism_class M) :=
λ {x y : M} (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h ∘ g = f × lp_hProp g f.
Definition wfs_rlp' {M : category} (w : wfs M) : (morphism_class M) :=
λ {x y : M} (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h ∘ g = f × lp_hProp f h.
Lemma llp_iff_lift_with_R {M : category} (w : wfs M) {x y : M} (f : x --> y) : (wfs_llp' w _ _) f <-> (wfs_R w _ _) f.
Proof.
split.
- intro hf.
unfold wfs_R.
rewrite (wfs_rlp w).
intros a b g hg.
intros top bottom comm_total.
use hf.
intro h.
destruct h as [Mf [lf [rf [lf_l [rf_r [fact lp_lff]]]]]].
use (lp_lff (identity _) rf).
{
rewrite id_left.
now symmetry.
}
intro H.
destruct H as [lift_lff [comm_lff1 comm_lff2]].
assert (lp_hProp g rf) as lp_grf.
{
unfold wfs_R in rf_r.
rewrite (wfs_rlp) in rf_r.
exact (rf_r _ _ g hg).
}
use (lp_grf (lf ∘ top) bottom).
{
rewrite <- assoc, fact.
exact comm_total.
}
intro H.
destruct H as [lift_grf [comm_grf1 comm_grf2]].
apply hinhpr.
exists (lift_lff ∘ lift_grf).
split.
* rewrite assoc, comm_grf1, <- assoc, comm_lff1, id_right.
reflexivity.
* rewrite <- assoc, comm_lff2.
exact comm_grf2.
-
intro hf.
use (wfs_fact w _ _ f).
intro h.
destruct h as [z [g [h [g_l [h_r comp]]]]].
apply hinhpr.
exists z, g, h.
repeat split; try assumption.
unfold wfs_R in hf.
rewrite wfs_rlp in hf.
exact (hf _ _ _ g_l).
Defined.
Lemma lp_of_retracts {M : category} {a b x y a' b' x' y' : M}
{f : a --> b} {f' : a' --> b'}
{g : x --> y} {g' : x' --> y'}
(rf : retract f' f) (rg : retract g' g) :
(lp f' g') -> (lp f g).
Proof.
intros Hlp h k Hcomm.
destruct rf as [ia [ra [ib [rb [ha [hb [hif hrf]]]]]]].
destruct rg as [ix [rx [iy [ry [hx [hy [hig hrg]]]]]]].
use Hlp.
- exact (ra · h · ix).
- exact (rb · k · iy).
- rewrite <- assoc, hig, assoc, <- (assoc _ h g), Hcomm, assoc, hrf, assoc, assoc.
reflexivity.
- intro Hl.
destruct Hl as [l [H1 H2]].
apply hinhpr.
exists (ib · l · rx).
split.
* rewrite assoc, assoc, <- hif, <- (assoc _ f' l), H1, assoc, assoc.
now rewrite ha, id_left, <- assoc, hx, id_right.
* rewrite <- assoc, hrg, assoc, <- (assoc _ l g'), H2, assoc, assoc.
now rewrite hb, id_left, <- assoc, hy, id_right.
Defined.
End wfs.