Library UniMath.ModelCategories.Generated.LiftingWithClass

  intros rldJf g Jg.
  apply (elp_of_retracts (retract_self g) (Rff')).
  exact (rldJf g Jg).

filler lifting problem g --> f commutes with mn and the filler of g --> f --> f' in the right way

Definition right_lifting_data_comp {J : morphism_class C} {f f' : arrow C}
    (δ : right_lifting_data J f) (δ' : right_lifting_data J f') (mn : f --> f') : UU :=
  ∏ (g : arrow C) (H : J _ _ g) (S : g --> f ),
  (filler_map (δ g H _ _ (arrow_mor_comm S))) · (arrow_mor00 mn ) =
    filler_map (δ' g H _ _ (arrow_mor_comm (S · mn))).

Lemma isaprop_lifting_data_comp {J : morphism_class C} {f f'}
    (δ : right_lifting_data J f) (δ' : right_lifting_data J f') (mn : f --> f') :
  isaprop (right_lifting_data_comp δ δ' mn).
Show proof.

do 3 (apply impred; intro).
apply homset_property.

Definition rlp_morcls_disp (J : morphism_class C) : disp_cat (arrow C).
Show proof.

  use disp_cat_from_SIP_data.
  - exact (λ f , right_lifting_data J f).
  - intros f f' δ δ' mn.

    exact (right_lifting_data_comp δ δ' mn).
  -
    intros.
    apply isaprop_lifting_data_comp.
  -
    intros x a g H S.
    abstract (
      etrans; [apply id_right|];

      now rewrite id_right
    ).
  -
    intros f f' f'' δ δ' δ'' S0 S1 mn mn' g2 g2' S2.

    abstract (
      etrans; [apply assoc|];
      etrans; [apply cancel_postcomposition; apply mn|];
      etrans; [apply mn'|];

      now rewrite assoc
    ).

Definition rlp_morcls (J : morphism_class C) : category :=
total_category (rlp_morcls_disp J).

needed later all lifting problems of J wrt. g

Definition morcls_lp (J : morphism_class C) (f : arrow C) : UU :=
    ∑ (g : total_category (morcls_disp J)), (pr1 g ) --> f.

#[reversible] Coercion morcls_lp_diagram {J : morphism_class C} {f : arrow C} (lp : morcls_lp J f) := pr2 lp.
Definition morcls_lp_map {J : morphism_class C} {f : arrow C} (lp : morcls_lp J f) := pr1 lp.

Context (n : nwfs C).
Definition morcls_L_map_structure (J : morphism_class C) : UU :=
  disp_functor (functor_identity _) (morcls_disp J) (nwfs_L_maps n).

Context {J : morphism_class C}.

Definition R_map_rlp_morcls_structure_on_objects (η : morcls_L_map_structure J) :
    ∏ x , (nwfs_R_maps n) x -> (rlp_morcls_disp J) ((functor_identity _) x).
Show proof.

  intros f Rf.
  intros g hg h k S.

  unfold morcls_L_map_structure in η.
  set (Lg := η g hg).

  intros.
  apply (L_map_R_map_elp Lg Rf).

Definition R_map_rlp_morcls_structure_on_displayed_mors (η : morcls_L_map_structure J) :
∏ x y (xx : (nwfs_R_maps n) x) (yy : (nwfs_R_maps n) y) (f : x --> y ),
(xx -->[f ] yy ) -> (R_map_rlp_morcls_structure_on_objects η _ xx -->[ f ] R_map_rlp_morcls_structure_on_objects η _ yy ).
Show proof.

  intros f f' ff ff' S Sisalg g Jg Sgf.
  unfold morcls_L_map_structure in η.
  etrans. apply assoc'.
  etrans. apply assoc'.
  apply pathsinv0.
  etrans. apply assoc'.
  apply cancel_precomposition.
  apply pathsinv0.

  etrans. apply cancel_postcomposition.
          use (section_disp_on_eq_morphisms' (nwfs_fact n) (γ := Sgf)).

  apply pathsinv0.
  etrans. apply cancel_postcomposition.
          use (section_disp_on_eq_morphisms' (nwfs_fact n) (γ := Sgf · S)).
  etrans. apply cancel_postcomposition, maponpaths.
          apply (section_disp_comp (nwfs_fact n)).

  etrans. apply assoc'.
  apply cancel_precomposition.

  destruct ff as [αf αflaws].
  destruct ff' as [αf' αf'laws].
  set (S11 := three_mor11 ((# n)%cat S)).
  change (S11 · arrow_mor00 αf' = arrow_mor00 αf · arrow_mor00 S).

  set (top_line := arrow_mor00_eq Sisalg).
  exact (pathsinv0 top_line).

"this assignation extends to a functor θ: R-Map ⟶ J□", Garner 2007, p18

Definition R_map_rlp_morcls_structure_data (η : morcls_L_map_structure J) :
    disp_functor_data (functor_identity _) (nwfs_R_maps n) (rlp_morcls_disp J) :=
  (R_map_rlp_morcls_structure_on_objects η ,, R_map_rlp_morcls_structure_on_displayed_mors η).

Definition R_map_rlp_morcls_structure_axioms (η : morcls_L_map_structure J) :
    disp_functor_axioms (R_map_rlp_morcls_structure_data η).
Show proof.

unfold disp_functor_axioms.
split; intros; apply isaprop_lifting_data_comp.

Definition R_map_rlp_morcls_structure (η : morcls_L_map_structure J) :
disp_functor (functor_identity _) (nwfs_R_maps n) (rlp_morcls_disp J) :=
(_,, R_map_rlp_morcls_structure_axioms η).

Garner 2008, Definition 3.9 / Garner 2007, p18 we say that n := (L, R, Δ) is cofibrantly generated by (J, η) if θ is an isomorphism of categories

Definition cofibrantly_generated (η : morcls_L_map_structure J) :=
is_equiv_over (_,, identity_functor_is_adj_equivalence) (R_map_rlp_morcls_structure η).

Definition algebraically_free : UU :=
∑ η : morcls_L_map_structure J , cofibrantly_generated η.

Garner 2008, Proposition 3.12 / Garner 2007, p18

Lemma algebraically_free_nwfs_gives_cofibrantly_generated_wfs :
algebraically_free ->
(nwfs_R_maps_class n )^cl = λ x y f , ∥rlp_morcls_disp J f ∥.
Show proof.

  intro H.
  destruct H as [η cofibη].

  apply morcls_eq_impl_morcls_cl_eq.
  {

    intros x' y' g' x y g Hg.
    destruct Hg as [Jg Rgg'].
    use (hinhuniv _ Jg).
    clear Jg; intro Jg.

    apply hinhpr.
    intros f Jf.
    apply (@right_lifting_data_retract J g g').
    - exact Rgg'.
    - exact Jg.
    - exact Jf.
  }

  apply morphism_class_subset_antisymm;
    intros x y f Hf;
    use (hinhuniv _ Hf);
    clear Hf; intro Hf;
    apply hinhpr.
  -
    set (θ := R_map_rlp_morcls_structure η).
    exact (θ f Hf).
  -

    set (θinv := right_adjoint_of_is_equiv_over _ cofibη).
    exact (θinv f Hf).

End preliminaries.

Garner 2007, p19

Section lifting_with_J.
Context {C : category}.
Context (HCC : Colims C).
Context (J : morphism_class C).
Context (f : arrow C).

Local Definition CC :
Coproducts (morcls_lp J f) C.
Show proof.

  apply Coproducts_from_Colims.
  intro d.
  exact (HCC _ d).

Local Definition CCoequalizers : Coequalizers C.
Show proof.

exact (Coequalizers_from_Colims _ HCC).

Local Definition POs : Pushouts C.
Show proof.

  apply Pushouts_from_Coequalizers_BinCoproducts.
  - apply BinCoproducts_from_Colims.
    intro d.
    exact (HCC _ d).
  - intros H z g f'.
    set (coeq := CCoequalizers _ _ g f').
    use tpair.
    * exists (CoequalizerObject _ coeq).
      exact (CoequalizerArrow _ coeq).
    * exists (CoequalizerArrowEq _ coeq).
      intros w h Hw.
      use unique_exists.
      + exact (CoequalizerOut _ coeq _ h Hw).
      + exact (CoequalizerArrowComm _ coeq _ h Hw).
      + intro y; apply homset_property.
      + intros y Hy.
        exact (CoequalizerOutUnique _ _ _ _ _ _ Hy).

Definition morcls_lp_dom_coprod :=
  CC (λ (g : morcls_lp J f ), arrow_dom (pr1 (morcls_lp_map g))).
Definition morcls_lp_cod_coprod :=
  CC (λ (g : morcls_lp J f ), arrow_cod (pr1 (morcls_lp_map g))).

Definition morcls_lp_coprod :=
(CoproductOfArrows' _ _
   morcls_lp_dom_coprod morcls_lp_cod_coprod
   (λ (S : morcls_lp J f ), arrow_mor (pr1 (morcls_lp_map S)))).

the canonical diagram capturing all lifting problems in J

Definition morcls_lp_coprod_diagram : morcls_lp_coprod --> f.
Show proof.

  use mors_to_arrow_mor.
  - exact (CoproductArrow (morcls_lp_dom_coprod) (λ j , arrow_mor00 j)).
  - exact (CoproductArrow (morcls_lp_cod_coprod) (λ j , arrow_mor11 j)).
  - abstract (
      etrans; [apply postcompWithCoproductArrow|];
      apply pathsinv0;
      etrans; [apply precompWithCoproductArrow|];
      apply pathsinv0;
      apply maponpaths;
      apply funextsec;
      intro j;
      exact (arrow_mor_comm j)
    ).

It is possible to show this more generally for any coproduct of maps in J, but this is not really necessary or useful for us.

The proof of this lemma is practically the same as that of wfs_closed_coproducts, but we do not need the axiom of choice here, since we know the actual lifting data.

Lemma lifting_data_impl_lifting_coprod_lp :
right_lifting_data J f -> elp (morcls_lp_coprod) f.
Show proof.

  intro rldJf.
  intros h k S.

  set (hj := λ (j : morcls_lp J f ), (CoproductIn _ j ) · h).
  set (kj := λ (j : morcls_lp J f ), (CoproductIn _ j ) · k).

  assert (∏ (j : morcls_lp J f ), ∑ lj , ((pr1 (morcls_lp_map j)) · lj = hj j ) × (lj · f = kj j )) as jlift.
  {
    intro j.
    use (rldJf (pr1 (morcls_lp_map j)) (pr2 (morcls_lp_map j))).
    etrans. apply assoc'.
    etrans. apply cancel_precomposition. exact S.
    etrans. apply assoc.
    apply pathsinv0.
    etrans. apply assoc.
    apply pathsinv0.
    etrans. apply cancel_postcomposition.
            exact (CoproductOfArrows'In _ _ _ _ _ j).
    reflexivity.
  }

  set (jlifts := foralltototal _ _ jlift).
  destruct jlifts as [lj hlj].
  set (hl := isCoproduct_Coproduct _ _ (morcls_lp_cod_coprod) _ lj).
  destruct hl as [[l hl] uniqueness].

  exists l.
  split; rewrite CoproductArrowEta, (CoproductArrowEta _ _ _ _ _ l).
  -

    etrans. apply (precompWithCoproductArrow).

    apply CoproductArrowUnique.

    intro j.
    etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod)).

    destruct (hlj j) as [hljcomm _].

    apply pathsinv0.
    etrans. exact (pathsinv0 hljcomm).
    etrans. apply cancel_precomposition.
            exact (pathsinv0 (hl j)).
    reflexivity.
  -
    apply CoproductArrowUnique.

    intro j.
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            apply (CoproductInCommutes (morcls_lp_cod_coprod)).

    destruct (hlj j) as [_ kljcomm].

    apply pathsinv0.
    etrans. exact (pathsinv0 kljcomm).
    etrans. apply cancel_postcomposition.
            exact (pathsinv0 (hl j)).
    reflexivity.

we need the actual diagram for the other direction (this does not hold for just any coproduct)

Lemma lifting_coprod_lp_impl_lifting_data :
filler (arrow_mor_comm (morcls_lp_coprod_diagram)) ->
right_lifting_data J f.
Show proof.

  intro l.
  intros g Jg h k H.

  destruct l as [ltot [Hl1 Hl2]].
  simpl in Hl1, Hl2, ltot.

  set (Jtot := total_category (morcls_disp J)).

  set (g' := (g,, Jg) : Jtot).
  set (Hlp := (g',, (make_dirprod h k,, H)) : morcls_lp J f).
  set (codg_in := (CoproductIn (morcls_lp_cod_coprod) Hlp)).
  set (domg_in := (CoproductIn (morcls_lp_dom_coprod) Hlp)).

  exists (codg_in · ltot).
  split.
  -
    assert (h = domg_in · (arrow_mor00 (morcls_lp_coprod_diagram))) as Hh.
    {

      apply pathsinv0.

      exact (CoproductInCommutes (morcls_lp_dom_coprod) _ Hlp).
    }
    apply pathsinv0.
    etrans. exact Hh.
    apply pathsinv0.

    assert (g · codg_in = domg_in · (morcls_lp_coprod )) as Hg.
    {
      unfold codg_in, domg_in, morcls_lp_coprod.
      rewrite (CoproductOfArrows'In _ _ (morcls_lp_dom_coprod)).
      reflexivity.
    }
    etrans. apply assoc.
    etrans. apply maponpaths_2.
            exact Hg.
    etrans. apply assoc'.
    apply cancel_precomposition.
    exact Hl1.
  - etrans. apply assoc'.
    etrans. apply maponpaths.
            exact Hl2.

    apply pathsinv0.

    apply pathsinv0.
    exact (CoproductInCommutes (morcls_lp_cod_coprod) _ Hlp).

Lemma lifting_data_Jg_iff_lifting_coprod_lp :
right_lifting_data J f <->
filler (arrow_mor_comm (morcls_lp_coprod_diagram)).
Show proof.

  split.
  - intro rldJf.
    apply lifting_data_impl_lifting_coprod_lp.
    exact rldJf.
  - apply lifting_coprod_lp_impl_lifting_data.

We turn the diagram

          h_x
    ∑A_x ----> C
     |         |
∑f_x |         | g
     v         v
    ∑B_x ----> D
          k_x

into the pushout diagram

         h_x
    ∑A_x ----> C--\
     |         |  |
∑f_x |     λ1g |  \
     v         v   |
    ∑B_x ---> E1g  | id · g
      \__       \  |
         \_   ρ1g|
      k_x  \_____ \|
                   D

using the pushout property. Inserting an identity morphism gives a diagram

          h_x
    ∑A_x ----> C ====== C
     |         |        |
∑f_x |         | λ1g    |
     v         v        v
    ∑B_x ---> E1g ----> D  ~~> k_x
                   ρ1g

etrans. apply PushoutArrow_PushoutIn2.
reflexivity.

    C ===== C
    |       |
 λ1g|       | g
    v       v
   E1g ---> D
       ρ1g

Definition morcls_lp_coprod_diagram_red : λ1 --> f.
Show proof.

  use mors_to_arrow_mor.
  - exact (identity _).
  - exact ρ1.
  - abstract (
      etrans; [apply id_left|];
      exact (pathsinv0 λ1_ρ1 _compat)
    ).

    λ1g
  C ---> E1g
  |       |
 g|       | ρ1g
  v       v
  D ===== D

Definition morcls_lp_coprod_diagram_red_flipped : f --> ρ1.
Show proof.

  use mors_to_arrow_mor.
  - exact λ1.
  - exact (identity _).
  - abstract (
      apply pathsinv0;
      etrans; [apply id_right|];
      exact (pathsinv0 λ1_ρ1 _compat)
    ).

Lifting w.r.t. the coproduct diagram of J is the same as lifting w.r.t. this reduced diagram (follows from pushout properties)

Lemma lifting_coprod_lp_red_impl_lifting_coprod_lp :
filler (arrow_mor_comm (morcls_lp_coprod_diagram_red)) ->
filler (arrow_mor_comm (morcls_lp_coprod_diagram)).
Show proof.

  intro H.
  destruct H as [l [Hl1 Hl2]].
  exists ((PushoutIn1 morcls_lp_coprod_diagram_pushout ) · l).
  split.
  -
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            apply (PushoutSqrCommutes (morcls_lp_coprod_diagram_pushout)).

    etrans. apply assoc'.
    etrans. apply maponpaths. exact Hl1.
    apply id_right.
  -
    etrans. apply assoc'.
    etrans. apply maponpaths. exact Hl2.

    use PushoutArrow_PushoutIn1.

Lemma lifting_coprod_lp_impl_lifting_coprod_lp_red :
filler (arrow_mor_comm (morcls_lp_coprod_diagram)) ->
filler (arrow_mor_comm (morcls_lp_coprod_diagram_red)).
Show proof.

  intro H.
  destruct H as [l [Hl1 Hl2]].

  assert (H : morcls_lp_coprod · l =
            arrow_mor00 morcls_lp_coprod_diagram · identity _).
  {
    apply pathsinv0.
    etrans. apply id_right.
    exact (pathsinv0 Hl1).
  }


  set (lred := PushoutArrow
                  morcls_lp_coprod_diagram_pushout
                  _ l (identity _) H).
  exists lred.
  split.
  -
    apply PushoutArrow_PushoutIn2.
  -

    use PushoutArrowUnique.
    *
      etrans. apply assoc.
      etrans. apply maponpaths_2.
              apply PushoutArrow_PushoutIn1.
      exact Hl2.
    *
      etrans. apply assoc.
      etrans. apply maponpaths_2.
              apply PushoutArrow_PushoutIn2.
      apply id_left.

almost proposition 12 in Garner, 2007

Lemma lifting_coprod_lp_iff_lifting_coprod_lp_red :
filler (arrow_mor_comm (morcls_lp_coprod_diagram)) <->
filler (arrow_mor_comm (morcls_lp_coprod_diagram_red)).
Show proof.

  split.
  - exact lifting_coprod_lp_impl_lifting_coprod_lp_red.
  - exact lifting_coprod_lp_red_impl_lifting_coprod_lp.

Definition Λ1 : f --> ρ1.
Show proof.

  use mors_to_arrow_mor.
  - exact λ1.
  - exact (identity _).
  - abstract (
      rewrite id_right, <- id_left;
      apply pathsinv0;
      exact (arrow_mor_comm morcls_lp_coprod_diagram_red)
    ).

Lemma lifting_data_Jg_iff_maps :
right_lifting_data J f <->
∑ (γ : ρ1 --> f ), Λ1 · γ = identity _.
Show proof.

  apply (logeq_trans lifting_data_Jg_iff_lifting_coprod_lp).
  apply (logeq_trans lifting_coprod_lp_iff_lifting_coprod_lp_red).

  split; intro H.
  - destruct H as [l [lcomm1 lcomm2]].
    use tpair.
    * use mors_to_arrow_mor.
      + exact l.
      + exact (identity _).
      + abstract (
          etrans; [exact lcomm2|];
          apply pathsinv0;
          apply id_right
        ).
    * use arrow_mor_eq.
      + exact lcomm1.
      + apply id_left.
  - destruct H as [γ γcomm].
    exists (arrow_mor00 γ).
    set (γcomm1 := arrow_mor00_eq γcomm).
    set (γcomm2 := arrow_mor11_eq γcomm).
    split.
    * exact γcomm1.
    * etrans. exact (arrow_mor_comm γ).
      etrans. apply cancel_precomposition.
              etrans. exact (pathsinv0 (id_left _)).
              exact γcomm2.
      apply id_right.

End lifting_with_J.