Library UniMath.ModelCategories.Generated.OneStepMonad

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.Monads.MonadAlgebras.
Require Import UniMath.CategoryTheory.Monads.Comonads.
Require Import UniMath.CategoryTheory.Monads.ComonadCoalgebras.
Require Import UniMath.CategoryTheory.catiso.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Pushouts.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.SIP.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Opposite.

Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Three.
Require Import UniMath.ModelCategories.MorphismClass.
Require Import UniMath.ModelCategories.Retract.
Require Import UniMath.ModelCategories.Lifting.
Require Import UniMath.ModelCategories.NWFS.
Require Import UniMath.ModelCategories.NWFSisWFS.
Require Import UniMath.ModelCategories.Generated.LiftingWithClass.

Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonadAlgebras.

Local Open Scope cat.
Local Open Scope mor_disp.
Local Open Scope morcls.

Arguments CoproductArrow {_} {_} {_} _ {_}.
Arguments CoproductIn {_} {_} {_} _.
Arguments CoproductInCommutes {_} {_} {_} _ {_}.

We have to do this special stuff, because we come across a lot of equalities between coproduct inclusions, where the indexed objects are not the same (map, lifting problem map --> f) only because the lifting problems are not the same, the maps are in fact the same.
In fact, all the inclusions we do are based on the (co)domain of the map of the lifting problem, and entirely independent of the lifting problem itself. This means that indeed, the inclusions should just be equal.
In theory though, in a general case, the inclusions would not be equal, and differ by some idtoiso (see CoproductIn_idtoiso), since the objects that the inclusions originate from theoretically do not have to be the same.
Lemma CoproductInLiftingProblemsEq
    {C : category} {J : morphism_class C} {f : arrow C}
    {a : total_category (morcls_disp J) -> C} {CCa : Coproduct _ _ (λ lp, a (morcls_lp_map lp))}
    {g : total_category (morcls_disp J)} {S S' : (pr1 g) --> f} :
    S = S' -> CoproductIn CCa (g,, S) = CoproductIn CCa (g,, S').
Show proof.
  intro H.
  induction H.
  reflexivity.

specialize domain / codomain cases
Lemma CoproductInLiftingProblemsEqDom
    {C : category} {J : morphism_class C} {f : arrow C}
    {CCa : Coproduct _ _ (λ lp, arrow_dom (pr1 (morcls_lp_map lp)))}
    {g : total_category (morcls_disp J)} {S S' : (pr1 g) --> f} :
    S = S' -> CoproductIn CCa (g,, S) = CoproductIn CCa (g,, S').
Show proof.
  apply (CoproductInLiftingProblemsEq (a := λ f, arrow_dom (pr1 f))).

Lemma CoproductInLiftingProblemsEqCod
    {C : category} {J : morphism_class C} {f : arrow C}
    {CCa : Coproduct _ _ (λ lp, arrow_cod (pr1 (morcls_lp_map lp)))}
    {g : total_category (morcls_disp J)} {S S' : (pr1 g) --> f} :
    S = S' -> CoproductIn CCa (g,, S) = CoproductIn CCa (g,, S').
Show proof.
  apply (CoproductInLiftingProblemsEq (a := λ f, arrow_cod (pr1 f))).

first try basic apply / use, the more expensive match statement
Ltac morcls_lp_coproduct_in_eq :=
  apply (CoproductInLiftingProblemsEqCod) ||
  apply (CoproductInLiftingProblemsEqDom) ||
  use (CoproductInLiftingProblemsEqCod) ||
  use (CoproductInLiftingProblemsEqDom) ||
    match goal with
    |- CoproductIn _ ?S = CoproductIn _ ?S'
      => apply (CoproductInLiftingProblemsEqCod (S:=pr2 S)) ||
         apply (CoproductInLiftingProblemsEqCod (S':=pr2 S')) ||
         apply (CoproductInLiftingProblemsEqDom (S:=pr2 S)) ||
         apply (CoproductInLiftingProblemsEqDom (S':=pr2 S'))
    end.

Section one_step_monad.

Context {C : category} (J : morphism_class C).
Context (CC : Colims C).

Garner 2008, section 5.2 (functor K)
Definition morcls_coprod_functor_data : functor_data (arrow C) (arrow C).
Show proof.
  use make_functor_data.
  -
    intro f.
    exact (morcls_lp_coprod CC J f).
  -
    intros f f' γ.
    use mors_to_arrow_mor.
    * use CoproductOfArrowsInclusion.
      +
        intro lpJf.
        destruct lpJf as [g S].
        exists g.
        exact (S · γ).
      +
        intro. exact (identity _).
    * use CoproductOfArrowsInclusion.
      +
        intro lpJf.
        destruct lpJf as [g S].
        exists g.
        exact (S · γ).
      + intro. exact (identity _).
    *
      abstract (
        
        
        
        etrans; [use CoproductOfArrowsInclusion_comp|];
        apply pathsinv0;
        etrans; [use CoproductOfArrowsInclusion_comp|];
        
        
        apply maponpaths;
        apply funextsec;
        intro;
        etrans; [apply id_right|];
        apply pathsinv0;
        etrans; [apply id_left|];
        reflexivity
      ).

Definition morcls_coprod_functor_is_functor : is_functor morcls_coprod_functor_data.
Show proof.
  split.
  - intro f.
    use arrow_mor_eq; apply pathsinv0, Coproduct_endo_is_identity; intro.
    * etrans.
      apply (CoproductOfArrowsInclusionIn _ (morcls_lp_dom_coprod CC J f)).
      etrans. apply id_left.
      morcls_lp_coproduct_in_eq.
      etrans. apply id_right.
      reflexivity.
    * etrans.
      apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J f)).
      etrans. apply id_left.
      morcls_lp_coproduct_in_eq.
      apply id_right.
  - intros g f h S T.
    use arrow_mor_eq; apply pathsinv0.
    * etrans. use CoproductOfArrowsInclusion_comp.
      etrans. apply maponpaths.
              apply funextsec.
              intro.
              apply id_right.

      apply CoproductArrowUnique.
      intro.
      etrans. use (CoproductOfArrowsInclusionIn _ _ _ _ i).
      etrans. apply id_left.
      apply pathsinv0.
      etrans. apply id_left.
      morcls_lp_coproduct_in_eq.
      etrans. apply assoc.
      reflexivity.
    * etrans. use CoproductOfArrowsInclusion_comp.
      etrans. apply maponpaths.
              apply funextsec.
              intro.
              apply id_right.

      apply CoproductArrowUnique.
      intro.
      etrans. use (CoproductOfArrowsInclusionIn _ _ _ _ i).
      etrans. apply id_left.
      apply pathsinv0.
      etrans. apply id_left.
      morcls_lp_coproduct_in_eq.
      apply assoc.

K in Garner
Definition morcls_coprod_functor : functor (arrow C) (arrow C) :=
    (_,, morcls_coprod_functor_is_functor).

Definition morcls_coprod_nat_trans_data :
    nat_trans_data morcls_coprod_functor (functor_identity _).
Show proof.
  intro f.
  exact (morcls_lp_coprod_diagram CC J f).

Definition morcls_coprod_nat_trans_is_nat_trans :
    is_nat_trans _ _ morcls_coprod_nat_trans_data.
Show proof.
  intros f f' γ.
  use arrow_mor_eq.
  - etrans. use precompWithCoproductArrowInclusion.
    apply pathsinv0.
    etrans. apply postcompWithCoproductArrow.
    apply maponpaths.
    apply funextsec.
    intro i.
    apply pathsinv0.
    apply id_left.
  - etrans. use precompWithCoproductArrowInclusion.
    apply pathsinv0.
    etrans. apply postcompWithCoproductArrow.
    apply maponpaths.
    apply funextsec.
    intro i.
    apply pathsinv0.
    apply id_left.

φ in Garner 2007, p23
Definition morcls_coprod_nat_trans :
    nat_trans morcls_coprod_functor (functor_identity _) :=
  (_,, morcls_coprod_nat_trans_is_nat_trans).

Arguments CoproductObject {_} {_} {_}.

Lemma commuting_cube_construction {f f' : arrow C}
    {aa : CoproductObject (morcls_lp_dom_coprod CC J _)
          --> CoproductObject (morcls_lp_dom_coprod CC J _)}
    {bb : CoproductObject (morcls_lp_cod_coprod CC J f)
          --> CoproductObject (morcls_lp_cod_coprod CC J f')}
    {cc : arrow_dom f --> arrow_dom f'}
    (leftface : (morcls_coprod_functor f) · bb = aa · (morcls_coprod_functor f'))
    (topface : arrow_mor00 (morcls_lp_coprod_diagram CC J f) · cc =
                aa · arrow_mor00 (morcls_lp_coprod_diagram CC J f')) :
  E1 CC J f --> E1 CC J f'.
Show proof.
  set (CE1f' := cc · (λ1 CC J f')).
  set (BE1f' := bb · (PushoutIn1 (morcls_lp_coprod_diagram_pushout CC J f'))).

  use (PushoutArrow
       (morcls_lp_coprod_diagram_pushout CC J f)
       _ BE1f' CE1f').

  abstract (
    
    
    
    etrans; [apply assoc|];

    
    etrans; [apply cancel_postcomposition; exact leftface|];
    etrans; [apply assoc'|];

    
    apply pathsinv0;
    etrans; [apply assoc|];
    etrans; [apply cancel_postcomposition; exact topface|];

    
    etrans; [apply assoc'|];
    apply cancel_precomposition;

    
    apply pathsinv0;
    exact (PushoutSqrCommutes (morcls_lp_coprod_diagram_pushout CC J f'))
  ).

Lemma commuting_cube_bottom_face {f f' : arrow C}
    {aa : CoproductObject (morcls_lp_dom_coprod CC J f)
          --> CoproductObject (morcls_lp_dom_coprod CC J f')}
    {bb : CoproductObject (morcls_lp_cod_coprod CC J f)
          --> CoproductObject (morcls_lp_cod_coprod CC J f')}
    {cc : arrow_dom f --> arrow_dom f'}
    {leftface : (morcls_coprod_functor f) · bb = aa · (morcls_coprod_functor f')}
    {topface : arrow_mor00 (morcls_lp_coprod_diagram CC J f) · cc =
                aa · arrow_mor00 (morcls_lp_coprod_diagram CC J f')} :
  PushoutIn1 (morcls_lp_coprod_diagram_pushout CC J f) · commuting_cube_construction leftface topface =
  bb · PushoutIn1 (morcls_lp_coprod_diagram_pushout CC J f').
Show proof.
  etrans. apply PushoutArrow_PushoutIn1.
  reflexivity.

Lemma commuting_cube_right_face {f f' : arrow C}
    {aa : CoproductObject (morcls_lp_dom_coprod CC J f)
          --> CoproductObject (morcls_lp_dom_coprod CC J f')}
    {bb : CoproductObject (morcls_lp_cod_coprod CC J f)
          --> CoproductObject (morcls_lp_cod_coprod CC J f')}
    {cc : arrow_dom f --> arrow_dom f'}
    {leftface : (morcls_coprod_functor f) · bb = aa · (morcls_coprod_functor f')}
    {topface : arrow_mor00 (morcls_lp_coprod_diagram CC J f) · cc =
                aa · arrow_mor00 (morcls_lp_coprod_diagram CC J f')} :
  cc · λ1 CC J f' =
  λ1 CC J f · commuting_cube_construction leftface topface.
Show proof.
  apply pathsinv0.
  etrans. apply PushoutArrow_PushoutIn2.
  reflexivity.

Lemma commuting_cube_construction_eq {f f' : arrow C}
    {aa : CoproductObject (morcls_lp_dom_coprod CC J f)
          --> CoproductObject (morcls_lp_dom_coprod CC J f')}
    {bb : CoproductObject (morcls_lp_cod_coprod CC J f)
          --> CoproductObject (morcls_lp_cod_coprod CC J f')}
    {cc : arrow_dom f --> arrow_dom f'}
    {aa' : CoproductObject (morcls_lp_dom_coprod CC J f)
           --> CoproductObject (morcls_lp_dom_coprod CC J f')}
    {bb' : CoproductObject (morcls_lp_cod_coprod CC J f)
           --> CoproductObject (morcls_lp_cod_coprod CC J f')}
    {cc' : arrow_dom f --> arrow_dom f'}
    (leftface : (morcls_coprod_functor f) · bb = aa · (morcls_coprod_functor f'))
    (topface : arrow_mor00 (morcls_lp_coprod_diagram CC J f) · cc =
                aa · arrow_mor00 (morcls_lp_coprod_diagram CC J f'))
    (leftface' : (morcls_coprod_functor f) · bb' = aa' · (morcls_coprod_functor f'))
    (topface' : arrow_mor00 (morcls_lp_coprod_diagram CC J f) · cc' =
                 aa' · arrow_mor00 (morcls_lp_coprod_diagram CC J f')) :
  bb = bb' -> cc = cc' -> commuting_cube_construction leftface topface = commuting_cube_construction leftface' topface'.
Show proof.
  intros Hb Hc.
  use PushoutArrowUnique.
  - etrans. apply PushoutArrow_PushoutIn1.
    apply cancel_postcomposition.
    exact Hb.
  - etrans. apply PushoutArrow_PushoutIn2.
    apply cancel_postcomposition.
    exact Hc.

one step comonad functor L1 sends f to λ1f
Definition one_step_comonad_functor_data : functor_data (arrow C) (arrow C).
Show proof.
  use make_functor_data.
  - intro f.
    exact (λ1 CC J f).
  - intros f f' γ.
    set (Kγ := (#morcls_coprod_functor)%cat γ).
    set (φγ := nat_trans_ax morcls_coprod_nat_trans f f' γ).
    set (φγ00 := arrow_mor00_eq φγ).

    use mors_to_arrow_mor.
    * exact (arrow_mor00 γ).
    * use commuting_cube_construction.
      + exact (arrow_mor00 Kγ).
      + exact (arrow_mor11 Kγ).
      + exact (arrow_mor00 γ).
      + abstract (exact (pathsinv0 (arrow_mor_comm Kγ))).
      + abstract (exact (pathsinv0 φγ00)).
    *
      
      
      abstract (
        apply commuting_cube_right_face
      ).

Definition one_step_comonad_functor_is_functor : is_functor one_step_comonad_functor_data.
Show proof.
  split.
  - intro f.
    use arrow_mor_eq.
    *
      reflexivity.
    *
      apply pathsinv0, PushoutArrowUnique.
      + etrans. apply id_right.
        apply pathsinv0.
        etrans. apply cancel_postcomposition.
                apply maponpaths.
                apply functor_id.
        apply id_left.
      + etrans. apply id_right.
        apply pathsinv0.
        apply id_left.
  - intros g f h S T.
    use arrow_mor_eq.
    * reflexivity.
    * apply pathsinv0, PushoutArrowUnique.
      + apply pathsinv0.
        etrans. apply cancel_postcomposition.
                apply maponpaths.
                apply functor_comp.
        apply pathsinv0.
        etrans. apply assoc.
        etrans. apply cancel_postcomposition.
                use PushoutArrow_PushoutIn1.
        etrans. apply assoc'.
        etrans. apply cancel_precomposition.
                use PushoutArrow_PushoutIn1.
        apply assoc.
      +
        etrans. apply assoc.
        etrans. apply cancel_postcomposition.
                use PushoutArrow_PushoutIn2.
        etrans. apply assoc'.
        etrans. apply cancel_precomposition.
                use PushoutArrow_PushoutIn2.
        apply assoc.

Definition one_step_comonad_functor : functor (arrow C) (arrow C) :=
    (_,, one_step_comonad_functor_is_functor).

Lemma one_step_comonad_ρ1_compat {f f' : arrow C} (γ : f --> f') :
    arrow_mor11 (#(one_step_comonad_functor) γ)%cat · ρ1 CC J f' =
      ρ1 CC J f · arrow_mor11 γ.
Show proof.
  use (MorphismsOutofPushoutEqual
        (isPushout_Pushout (morcls_lp_coprod_diagram_pushout CC J f))).
  -
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            use PushoutArrow_PushoutIn1.
    etrans. apply assoc'.
    etrans. apply cancel_precomposition.
            use PushoutArrow_PushoutIn1.
    etrans. apply precompWithCoproductArrowInclusion.

    apply pathsinv0.
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            apply PushoutArrow_PushoutIn1.
    etrans. apply postcompWithCoproductArrow.

    apply maponpaths.
    apply funextsec.
    intro.
    apply pathsinv0.
    apply id_left.
  - etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            use PushoutArrow_PushoutIn2.
    etrans. apply assoc'.
    etrans. apply cancel_precomposition.
            use PushoutArrow_PushoutIn2.

    apply pathsinv0.
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            apply PushoutArrow_PushoutIn2.

    apply pathsinv0.
    exact (arrow_mor_comm γ).

Definition one_step_factorization_data : section_disp_data (three_disp C).
Show proof.
  use tpair.
  - intro f.
    exists (E1 CC J f).
    exists (λ1 CC J f), (ρ1 CC J f).
    abstract (
      apply λ1_ρ1_compat
    ).
  - intros f f' γ.
    set (L1γ := (#(one_step_comonad_functor) γ)%cat).
    exists (arrow_mor11 L1γ).
    abstract (
      split; apply pathsinv0; [
        
        exact (arrow_mor_comm L1γ)
      |
        apply one_step_comonad_ρ1_compat
      ]
    ).

Definition one_step_factorization_axioms : section_disp_axioms one_step_factorization_data.
Show proof.

  split.
  - intro f.
    apply subtypePath; [intro; apply isapropdirprod; apply homset_property|].
    set (one_step_comonad_id := functor_id (one_step_comonad_functor) f).
    set (bottom := arrow_mor11_eq one_step_comonad_id).
    exact bottom.
  - intros g1 g2 g3 γ12 γ23.
    apply subtypePath; [intro; apply isapropdirprod; apply homset_property|].
    set (one_step_comonad_comp := functor_comp (one_step_comonad_functor) γ12 γ23).
    set (bottom := arrow_mor11_eq one_step_comonad_comp).
    exact bottom.

Definition one_step_factorization : functorial_factorization C :=
    (_,, one_step_factorization_axioms).


Definition one_step_monad_functor_data : functor_data (arrow C) (arrow C).
Show proof.
  use make_functor_data.
  - intro f.
    exact (ρ1 CC J f).
  - intros f f' γ.

    use mors_to_arrow_mor.
    * exact (arrow_mor11 (#one_step_comonad_functor γ)%cat).
    * exact (arrow_mor11 γ).
    * abstract (
        exact (one_step_comonad_ρ1_compat _)
      ).

Definition one_step_monad_functor_is_functor : is_functor one_step_monad_functor_data.
Show proof.
  split.
  - intro f.
    use arrow_mor_eq.
    *
      apply pathsinv0, PushoutArrowUnique.
      + etrans. apply id_right.
        apply pathsinv0.
        etrans. apply cancel_postcomposition.
                apply maponpaths.
                apply functor_id.
        apply id_left.
      + etrans. apply id_right.
        apply pathsinv0.
        apply id_left.
    *
      reflexivity.
  - intros g f h S T.
    apply subtypePath; [intro; apply homset_property|].
    apply pathsdirprod.
    * etrans. apply maponpaths.
              apply (functor_comp one_step_comonad_functor).
      reflexivity.
    * reflexivity.

Definition one_step_monad_functor : functor (arrow C) (arrow C) :=
    (_,, one_step_monad_functor_is_functor).

Send λ1 f --> f along 
      C ====== C
      |        |
  λ1f |   L1   | f
      v        v
    E1f ----> D
          ρ1f
Definition one_step_comonad_counit_data : nat_trans_data (one_step_comonad_functor) (functor_identity _).
Show proof.
  intro f.
  use mors_to_arrow_mor.
  - exact (identity _).
  - exact (ρ1 CC J f).
  - abstract (exact (arrow_mor_comm (morcls_lp_coprod_diagram_red CC J f))).

Definition one_step_comonad_counit_is_nat_trans : is_nat_trans _ _ one_step_comonad_counit_data.
Show proof.
  intros f f' γ.
  use arrow_mor_eq.
  - etrans. apply id_right.
    apply pathsinv0.
    apply id_left.
  -
    
    use (MorphismsOutofPushoutEqual
          (isPushout_Pushout (morcls_lp_coprod_diagram_pushout CC J f))).
    *
      etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              use PushoutArrow_PushoutIn1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              use PushoutArrow_PushoutIn1.
      apply pathsinv0.
      etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              use PushoutArrow_PushoutIn1.

      set (φax := nat_trans_ax morcls_coprod_nat_trans f f' γ).
      set (bottom_square := arrow_mor11_eq φax).
      apply pathsinv0.
      exact (bottom_square).
    *
      etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              use PushoutArrow_PushoutIn2.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              use PushoutArrow_PushoutIn2.
      apply pathsinv0.
      etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              use PushoutArrow_PushoutIn2.

      apply pathsinv0.
      exact (arrow_mor_comm γ).

Definition one_step_comonad_counit : nat_trans (one_step_comonad_functor) (functor_identity _) :=
    (_,, one_step_comonad_counit_is_nat_trans).

Send f --> ρ1 f along 
        λ1f
    C ----> E1f
    |        |
f   |   R1   | ρ1f
    v        v
    D ====== D
Definition one_step_monad_unit_data : nat_trans_data (functor_identity _) (one_step_monad_functor).
Show proof.
  intro f.
  use mors_to_arrow_mor.
  - exact (λ1 CC J f).
  - exact (identity _).
  - abstract (exact (arrow_mor_comm (morcls_lp_coprod_diagram_red_flipped CC J f))).

Definition one_step_monad_unit_is_nat_trans : is_nat_trans _ _ one_step_monad_unit_data.
Show proof.
  intros f f' γ.
  use arrow_mor_eq.
  - apply pathsinv0.
    apply PushoutArrow_PushoutIn2.
  - etrans. apply id_right.
    apply pathsinv0.
    apply id_left.

Definition one_step_monad_unit : nat_trans (functor_identity _) (one_step_monad_functor) :=
    (_,, one_step_monad_unit_is_nat_trans).

ψf in Garner The inclusion of lifting problems is induced by S_f → S{L1f} : x ↦ (g_x -- in_x -> Kf = ∑f -- ϵf -> L1f) where ϵf is morcls_lp_coprod_diagram_red: 
            ∑h
  A ---> ∑A ---> X
  |      |       |
g |    ∑g|       | λ1f
  v      v       v
  B ---> ∑B ---> E1f
Definition morcls_lp_coprod_L1_inclusion (f : arrow C) :
    morcls_lp J f -> morcls_lp J (λ1 CC J f).
Show proof.
  intro S.
  exists (pr1 S).
  transparent assert (rhs_mor : (morcls_lp_coprod CC J f --> λ1 CC J f)).
  {
    use mors_to_arrow_mor.
    - exact (arrow_mor00 (morcls_lp_coprod_diagram CC J f)).
    - exact (PushoutIn1 (morcls_lp_coprod_diagram_pushout CC J f)).
    - abstract (
        set (rhs := PushoutSqrCommutes (morcls_lp_coprod_diagram_pushout CC J f));
        exact (pathsinv0 rhs)
      ).
  }
  apply (postcompose rhs_mor).

  use mors_to_arrow_mor.
  - exact (CoproductIn (morcls_lp_dom_coprod CC J f) S).
  - exact (CoproductIn (morcls_lp_cod_coprod CC J f) S).
  - abstract (exact (CoproductInCommutes _ _ S)).

δf in Garner
Definition morcls_lp_coprod_L1_map (f : arrow C) :
    (morcls_lp_coprod CC J f) --> (morcls_lp_coprod CC J (λ1 CC J f)).
Show proof.
  use mors_to_arrow_mor;
    try exact (CoproductOfArrowsInclusion
              (morcls_lp_coprod_L1_inclusion f) _ _
              (λ _, (identity _))).

  abstract (
    etrans; [use precompWithCoproductArrowInclusion|];
    
    apply pathsinv0;
    etrans; [use postcompWithCoproductArrow|];
    
    apply maponpaths;
    apply funextsec;
    intro S;
    apply pathsinv0;
    etrans; [apply id_left|];
    apply pathsinv0;
    etrans; [apply assoc'|];
    etrans; [apply cancel_precomposition; exact (CoproductOfArrowsInclusionIn _ _ _ _ S)|];
    etrans; [apply cancel_precomposition; apply id_left|];
    reflexivity
  ).

The map on morphisms becomes the right face from the cube induced by 
        ∑h
    ∑A ------> C
      |\          =
∑f=Kg|  \     ∑h'  =
      |    ∑A' -----> C
      v δf |
    ∑B    |Kλf       |
      \   |=     PO    λ1f
        \ v∑λf f     v
          ∑B  - - - > E1f
Definition one_step_comonad_mul_data :
    nat_trans_data
      (fact_L one_step_factorization)
      (functor_composite (fact_L one_step_factorization) (fact_L one_step_factorization)).
Show proof.
  intro f.
  set (δf := morcls_lp_coprod_L1_map f).

  use mors_to_arrow_mor.
  - exact (identity _).
  - use commuting_cube_construction.
    * exact (arrow_mor00 δf).
    * exact (arrow_mor11 δf).
    * exact (identity _).
    *
      exact (pathsinv0 (arrow_mor_comm δf)).
    *
      abstract (
        etrans; [apply id_right|];
        apply pathsinv0;
        etrans; [apply precompWithCoproductArrowInclusion|];
        
        apply (maponpaths (CoproductArrow _));
        apply funextsec;
        intro S;
        etrans; [apply id_left|];
        exact (CoproductInCommutes _ _ S)
      ).
  -
    abstract (
      use commuting_cube_right_face
    ).

Definition one_step_comonad_mul_is_nat_trans : is_nat_trans _ _ one_step_comonad_mul_data.
Show proof.
  intros f f' γ.
  use arrow_mor_eq.
  -
    etrans. apply id_right.
    apply pathsinv0.
    apply id_left.
  -
    use (MorphismsOutofPushoutEqual
      (isPushout_Pushout (morcls_lp_coprod_diagram_pushout CC J f))).
    *
      etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              use PushoutArrow_PushoutIn1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply assoc.

      apply pathsinv0.
      etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply assoc.

      apply cancel_postcomposition.
      etrans. use CoproductOfArrowsInclusion_comp.
      apply pathsinv0.
      etrans. use CoproductOfArrowsInclusion_comp.

      use CoproductArrowUnique.
      intro.
      etrans. apply (CoproductInCommutes (morcls_lp_cod_coprod CC J f)).
      etrans. apply assoc'.
      do 2 (etrans; [apply id_left|]).
      apply pathsinv0.
      etrans. apply assoc'.
      do 2 (etrans; [apply id_left|]).

      morcls_lp_coproduct_in_eq.

      use arrow_mor_eq.
      + etrans. apply cancel_postcomposition.
                apply (CoproductInCommutes (morcls_lp_dom_coprod CC J f)).
        apply pathsinv0.
        etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J f') _ (_,, _)).
        reflexivity.
      + etrans. apply assoc'.
        etrans. apply cancel_precomposition.
                apply PushoutArrow_PushoutIn1.

        etrans. apply assoc.
        etrans. apply cancel_postcomposition.
                apply (CoproductInCommutes (morcls_lp_cod_coprod CC J f)).
        etrans. apply assoc'.
        apply id_left.
    * etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              use PushoutArrow_PushoutIn2.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn2.

      etrans. apply cancel_precomposition.
              apply id_left.
      apply pathsinv0.
      etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              apply PushoutArrow_PushoutIn2.
      etrans. etrans. apply assoc'.
              apply cancel_precomposition.
              apply PushoutArrow_PushoutIn2.
      apply id_left.

Definition one_step_comonad_mul :
    nat_trans
      (fact_L one_step_factorization)
      (functor_composite (fact_L one_step_factorization) (fact_L one_step_factorization)) :=
  (_,, one_step_comonad_mul_is_nat_trans).


Definition one_step_comonad_data : disp_Comonad_data _ :=
    L_monad_data one_step_factorization one_step_comonad_mul.

Local Lemma one_step_comonad_assoc_law11 (f : arrow C) :
  arrow_mor11 (
    disp_δ one_step_comonad_data f
    · (# (fact_L one_step_factorization))%cat (disp_δ one_step_comonad_data f)
  ) =
  arrow_mor11 (
    disp_δ one_step_comonad_data f
    · disp_δ one_step_comonad_data (fact_L one_step_factorization f)
  ).
Show proof.
  use (MorphismsOutofPushoutEqual (isPushout_Pushout (morcls_lp_coprod_diagram_pushout CC J f))).
  - etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            use PushoutArrow_PushoutIn1.
    etrans. apply assoc'.
    etrans. apply cancel_precomposition.
            apply PushoutArrow_PushoutIn1.
    etrans. apply assoc.

    apply pathsinv0.
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            apply PushoutArrow_PushoutIn1.
    etrans. apply assoc'.
    etrans. apply cancel_precomposition.
            apply PushoutArrow_PushoutIn1.
    etrans. apply assoc.
    apply cancel_postcomposition.

    use CoproductArrow_eq.
    intro S.
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            use (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J f)).
    etrans. apply cancel_postcomposition.
            apply id_left.
    etrans. use (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J (fact_L one_step_factorization f)) _ _ (morcls_lp_coprod_L1_inclusion f S)).
    etrans. apply id_left.
    apply pathsinv0.
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            use (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J f)).
    etrans. apply assoc'.
    etrans. apply id_left.
    etrans. use (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J (fact_L one_step_factorization f)) _ _ (morcls_lp_coprod_L1_inclusion f S)).
    etrans. apply id_left.
    morcls_lp_coproduct_in_eq.
    use arrow_mor_eq.
    * etrans. apply id_right.
      etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J f)).
      apply pathsinv0.
      etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J (λ1 CC J f)) _ (morcls_lp_coprod_L1_inclusion f S)).
      etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J f)).
      reflexivity.
    * etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply assoc.
      apply cancel_postcomposition.
      etrans. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J f)).
      apply id_left.
  - etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            apply PushoutArrow_PushoutIn2.
    etrans. apply assoc'.
    etrans. apply id_left.
    etrans. apply PushoutArrow_PushoutIn2.
    etrans. apply id_left.
    apply pathsinv0.
    etrans. apply assoc.
    etrans. apply cancel_postcomposition.
            apply PushoutArrow_PushoutIn2.
    etrans. apply assoc'.
    etrans. apply id_left.
    etrans. apply PushoutArrow_PushoutIn2.
    apply id_left.

Definition one_step_comonad_laws :
    disp_Comonad_laws one_step_comonad_data.
Show proof.
  repeat split; intro f; use arrow_mor_eq.
  - apply id_left.
  - apply pathsinv0.
    use PushoutEndo_is_identity.
    * etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply precompWithCoproductArrowInclusion.
      apply pathsinv0.

      use CoproductArrowUnique.
      intro.
      apply pathsinv0.
      apply id_left.
    * etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              apply PushoutArrow_PushoutIn2.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn2.
      apply id_left.
  - apply id_left.
  - apply pathsinv0.
    use PushoutEndo_is_identity.
    * etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn1.
      etrans. apply assoc.

      apply pathsinv0.
      etrans. exact (pathsinv0 (id_left _)).
      apply cancel_postcomposition.

      apply pathsinv0.
      etrans. use CoproductOfArrowsInclusion_comp.
      apply pathsinv0.

      use Coproduct_endo_is_identity.
      intro S.
      etrans. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J f)).
      etrans. apply cancel_postcomposition.
              apply id_left.
      etrans. apply id_left.
      morcls_lp_coproduct_in_eq.

      use arrow_mor_eq.
      + etrans. apply assoc'.
        etrans. apply cancel_precomposition.
                apply id_right.
        etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J f) _ S).
        reflexivity.
      + etrans. apply assoc'.
        etrans. apply cancel_precomposition.
                apply PushoutArrow_PushoutIn1.

        etrans. apply (CoproductInCommutes (morcls_lp_cod_coprod CC J f) _ S).
        reflexivity.
    * etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              apply PushoutArrow_PushoutIn2.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              apply PushoutArrow_PushoutIn2.
      etrans. apply assoc.

      etrans. apply assoc'.
      etrans. apply id_left.
      apply id_left.
  - reflexivity.
  - exact (one_step_comonad_assoc_law11 f).

Definition one_step_comonad :
    lnwfs_over one_step_factorization :=
  (one_step_comonad_mul,, one_step_comonad_laws).

End one_step_monad.