Library UniMath.CategoryTheory.CategoricalRecursionSchemes

Author : Hichem Saghrouni Internship at IRIT, 2018 Under the supervision of Ralph Matthes
Later continued by Ralph Matthes (R.M.), see the end of this comment.
Work on the paper HINZE, R. and WU, N., 2016. Unifying structured recursion schemes: An Extended Study. Journal of Functional Programming, vol. 26, https://doi.org/10.1017/S0956796815000258.
The purpose of this file is to formalize in UniMath the recursion scheme presented by Hinze and Wu, with their original approach making use of liftings and conjugates.
For this, we formalize the notions of
  • Distributive Laws, which are natural transformations between
compositions of functors
  • Conjugates, which induce a binary relation between distributive laws,
defined by certain identities found in this document
  • Liftings, which constitute a specific type of functors between F-Algebras
These constructions finally allow us to follow the proof by Hinze and Wu of their theorem (found under "Theorem 5.2 (Adjoint folds)" in their paper) and thus reprove it formally.
Added by R.M.: how canonically defined liftings compose

Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.Adjunctions.Core.

Local Open Scope cat.

Section DefDistrLaw.

Context {C C' D D' : precategory} (F : functor C D) (F' : functor C' D')
          (H : functor C' C) (K : functor D' D).

the definition of Hinze and Wu - no other laws required for being considered a distributive law
Definition DistrLaw : UU :=
  nat_trans (H ∙ F) (F' ∙ K).

a small help for later type-checking
Definition DistrLaw_data : UU :=
  nat_trans_data (H ∙ F) (F' ∙ K).

End DefDistrLaw.

Section OperationsDistrLaws.

Definition comp_distr_laws {C C' C'' D D' D'' : category}{F : functor C D}{F' : functor C' D'}
  {F'' : functor C'' D''}{H : functor C' C}{H' : functor C'' C'}{K : functor D' D}{K' : functor D'' D'}
  (lambda : DistrLaw F F' H K) (lambda' : DistrLaw F' F'' H' K') :
  DistrLaw F F'' (H' ∙ H ) (K' ∙ K).
Show proof.
  red.
  apply (nat_trans_comp _ _ _ (α_functors _ _ _)).
  use (nat_trans_comp _ _ _ _ (α_functors _ _ _)).
  apply (nat_trans_comp _ _ _ (pre_whisker H' lambda)).
  apply (nat_trans_comp _ _ _ (α_functors_inv _ _ _)).
  exact (post_whisker lambda' K).

Definition id_distr_law {C D : category} (F : functor C D) :
  DistrLaw F F (functor_identity C) (functor_identity D).
Show proof.
  red.
  apply (nat_trans_comp _ _ _ (λ_functors _)).
  apply ρ_functors_inv.

Lemma comp_distr_laws_assoc {C C' C'' C''' D D' D'' D''' : category} {F : functor C D}
      {F' : functor C' D'} {F'' : functor C'' D''} {F''' : functor C''' D'''}
      {H : functor C' C} {H' : functor C'' C'} {H'' : functor C''' C''}
      {K : functor D' D} {K' : functor D'' D'} {K'' : functor D''' D''}
      (lambda : DistrLaw F F' H K)
      (lambda' : DistrLaw F' F'' H' K') (lambda'' : DistrLaw F'' F''' H'' K'') :
  comp_distr_laws (comp_distr_laws lambda lambda') lambda'' =
                comp_distr_laws lambda (comp_distr_laws lambda' lambda'').
Show proof.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  repeat rewrite id_left.
  repeat rewrite id_right.
  set (aux1 := nat_trans_ax lambda).
  eapply pathscomp0.   { apply pathsinv0.
    apply assoc.
  }
  apply cancel_precomposition.
  apply pathsinv0.
  etrans.
  { apply functor_comp. }
  apply cancel_precomposition.
  apply idpath.


Definition id_distr_law_left {C D : category} (F : functor C D) :
  ∏ (C' D' : category) (F' : functor C' D') (H : functor C' C) (K : functor D' D)
    (lambda : DistrLaw F F' H K),
  comp_distr_laws (id_distr_law F) lambda = lambda.
Show proof.
  intros C' D'.
  intros F' H K.
  intro lambda.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  repeat rewrite id_left.
  apply id_right.


Definition id_distr_law_right {C' D' : category} (F' : functor C' D') :
  ∏ (C D : category) (F : functor C D) (H : functor C' C) (K : functor D' D)
    (lambda : DistrLaw F F' H K),
  comp_distr_laws lambda (id_distr_law F') = lambda.
Show proof.
  intros C D.
  intros F H K.
  intro lambda.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  repeat rewrite id_left.
  rewrite id_right.
  etrans.
  { apply cancel_precomposition.
    apply functor_id.
  }
  apply id_right.

End OperationsDistrLaws.

Section Conjugates.

Lemma adjuncts_mutually_inverse1 {C D : category} {A : D} {B : C}
      {L : functor D C} {R : functor C D} (h : are_adjoints L R)
      (f : L A --> B) (g : A --> R B) :
  f = φ_adj_inv h g -> φ_adj h f = g.
Show proof.
  intro p.
  set (η := unit_from_are_adjoints h).
  set (ε := counit_from_are_adjoints h).
  set (triangle_right := triangle_id_right_ad h).
  change (unit_from_are_adjoints h) with η in triangle_right.
  change (counit_from_are_adjoints h) with ε in triangle_right.
  unfold φ_adj.
  assert (hyp : f = (φ_adj_inv h g)).
  - exact p.
  - rewrite hyp.
    unfold φ_adj_inv.
    rewrite functor_comp.
    change (# R (# L g)) with (# (L ∙ R) g).
    rewrite assoc.
    set (Hη := nat_trans_ax η).
    etrans.
    { apply cancel_postcomposition.
      apply pathsinv0.
      apply Hη.
    }
    rewrite <- id_right.
    rewrite <- assoc.
    apply cancel_precomposition.
    exact (triangle_right B).

Lemma adjuncts_mutually_inverse2 {C D : category} {A : D} {B : C}
      {L : functor D C} {R : functor C D} (h : are_adjoints L R)
      (f : L A --> B) (g : A --> R B) :
  φ_adj h f = g -> f = φ_adj_inv h g.
Show proof.
  intro p.
  set (η := unit_from_are_adjoints h).
  set (ε := counit_from_are_adjoints h).
  set (triangle_left := triangle_id_left_ad h).
  unfold φ_adj_inv.
  assert (hyp : g = (φ_adj h f)).
  - apply pathsinv0.
    exact p.
  - rewrite hyp.
    unfold φ_adj.
    rewrite functor_comp.
    change ( # L (# R f)) with (# (R ∙ L) f).
    rewrite <- assoc.
    set (Hε := nat_trans_ax ε).
    apply pathsinv0.
    etrans.
    { apply cancel_precomposition.
      apply Hε.
    }
    rewrite <- id_left.
    rewrite assoc.
    apply cancel_postcomposition.
    exact (triangle_left A).


Definition are_conjugates {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'}{H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R')
           (σ : DistrLaw L' L K H) (τ : DistrLaw K H R R') : UU :=
  ∏ (A : D) (B : C) (f : (L A) --> B),
  φ_adj h' (nat_trans_data_from_nat_trans σ A · #H f) = #K (φ_adj h f) · nat_trans_data_from_nat_trans τ B.

Definition are_conjugates' {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R')
           (σ : DistrLaw L' L K H) (τ : DistrLaw K H R R') : UU :=
  ∏ (A : D) (B : C) (g : A --> R B),
  nat_trans_data_from_nat_trans σ A · #H (φ_adj_inv h g) = φ_adj_inv h' (#K g · nat_trans_data_from_nat_trans τ B ).


Lemma isaprop_are_conjugates {C C' D D' : category} {L : functor D C} {R : functor C D}
      {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
      (h : are_adjoints L R) (h' : are_adjoints L' R')
      (σ : DistrLaw L' L K H) (τ : DistrLaw K H R R') :
  isaprop (are_conjugates h h' σ τ).
Show proof.
  apply impred; intro d.
  apply impred; intro c.
  apply impred; intro f.
  apply homset_property.

Lemma isaprop_are_conjugates' {C C' D D' : category} {L : functor D C} {R : functor C D}
      {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
      (h : are_adjoints L R) (h' : are_adjoints L' R')
      (σ : DistrLaw L' L K H) (τ : DistrLaw K H R R') :
  isaprop (are_conjugates' h h' σ τ).
Show proof.
  apply impred; intro d.
  apply impred; intro c.
  apply impred; intro g.
  apply homset_property.

Lemma are_conjugates_is_are_conjugates' {C C' D D' : category}
      {L : functor D C} {R : functor C D} {L' : functor D' C'} {R' : functor C' D'}
      {H : functor C C'} {K : functor D D' } (h : are_adjoints L R) (h' : are_adjoints L' R')
      (σ : DistrLaw L' L K H) (τ : DistrLaw K H R R') :
  are_conjugates h h' σ τ = are_conjugates' h h' σ τ.
Show proof.
  apply propositionalUnivalenceAxiom.
  - apply isaprop_are_conjugates.
  - apply isaprop_are_conjugates'.
  -
    red.
    intro P.
    red in P.
    intros A B g.
    set (hyp := (P A B (φ_adj_inv h g))).
    apply adjuncts_mutually_inverse2 in hyp.
    assert (hyp2 : # K (φ_adj h (φ_adj_inv h g)) = # K g).
    + apply maponpaths.
      apply φ_adj_after_φ_adj_inv.
    + apply pathsinv0 in hyp.
      eapply pathscomp0 in hyp.
      2 : {
        apply maponpaths.
        apply cancel_postcomposition.
        apply pathsinv0.
        apply hyp2.
      }
      apply pathsinv0 in hyp.
      exact hyp.
  -
    red.
    intro P.
    red in P.
    intros A B f.
    set (hyp := (P A B (φ_adj h f))).
    apply (adjuncts_mutually_inverse1 h' (pr1 σ A · # H (φ_adj_inv h (φ_adj h f))) (# K (φ_adj h f) · pr1 τ B)) in hyp.
    eapply pathscomp0 in hyp.
    2 : {
      apply maponpaths.
      apply cancel_precomposition.
      apply maponpaths.
      apply pathsinv0.
      apply φ_adj_inv_after_φ_adj.
    }
    exact hyp.

Definition σ_data_from_τ {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R')
           (τ : DistrLaw K H R R') : DistrLaw_data L' L K H :=
  λ A : D, φ_adj_inv h' (#K (unit_from_are_adjoints h A) · nat_trans_data_from_nat_trans τ (L A)).

Lemma is_nat_trans_σ_data_from_τ {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R')
           (τ : DistrLaw K H R R') : is_nat_trans _ _ (σ_data_from_τ h h' τ).
Show proof.
  red.
  intros d d' f.
  unfold σ_data_from_τ.
  etrans.
  { apply pathsinv0.
    simpl.
    apply φ_adj_inv_natural_precomp.
  }
  
  apply pathsinv0.
  etrans.
  { apply pathsinv0.
    simpl.
    apply φ_adj_inv_natural_postcomp.
  }
  apply maponpaths.
  apply pathsinv0.
  etrans.
  rewrite assoc.
  rewrite <- functor_comp.
  2: {
    set (Hτ := nat_trans_ax τ).
    change (# R' (# H (# L f))) with ( # (H ∙ R') (#L f)).
    rewrite <- assoc.
    apply cancel_precomposition.
    apply Hτ.
  }

  rewrite assoc.
  apply cancel_postcomposition.
  change (# (R ∙ K) (# L f)) with (# K (# (L ∙ R) f)).
  etrans.
  2 : {
    use functor_comp.
  }
  apply maponpaths.
  set (Hη := nat_trans_ax (unit_from_are_adjoints h)).
  apply Hη.

Definition σ_from_τ {C C' D D' : category} {L : functor D C} {R : functor C D}
  {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
  (h : are_adjoints L R) (h' : are_adjoints L' R') (τ : DistrLaw K H R R') : DistrLaw L' L K H.
Show proof.
  apply (make_nat_trans _ _ (σ_data_from_τ h h' τ)).
  apply is_nat_trans_σ_data_from_τ.

Lemma σ_from_τ_is_conjugate {C C' D D' : category} {L : functor D C}
      {R : functor C D} {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
      (h : are_adjoints L R) (h' : are_adjoints L' R')
      (hs : has_homsets C') (τ : DistrLaw K H R R') :
  are_conjugates' h h' (σ_from_τ h h' τ) τ.
Show proof.
  red.
  intros A B g.
  unfold σ_from_τ.
  simpl.
  unfold σ_data_from_τ.
  set (η := (unit_from_are_adjoints h)).
  etrans.
  { apply pathsinv0.
    apply φ_adj_inv_natural_postcomp.
  }
  apply maponpaths.
  set (Hτ := nat_trans_ax τ).
  etrans.
  { rewrite <- assoc.
    apply cancel_precomposition.
    apply pathsinv0.
    apply Hτ.
  }
  rewrite assoc.
  apply cancel_postcomposition.
  change (# (R ∙ K) (φ_adj_inv h g)) with (# K (# R (φ_adj_inv h g))).
  etrans.
  { apply pathsinv0.
    use functor_comp.
  }
  apply maponpaths.
  change (nat_trans_data_from_nat_trans η A · # R (φ_adj_inv h g)) with (φ_adj h (φ_adj_inv h g)).
  apply φ_adj_after_φ_adj_inv.

Definition τ_data_from_σ {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R') (σ : DistrLaw L' L K H) :
  DistrLaw_data K H R R' :=
  λ B : C, φ_adj h' (nat_trans_data_from_nat_trans σ (R B) · #H (counit_from_are_adjoints h B)).

Lemma is_nat_trans_τ_data_from_σ {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R') (σ : DistrLaw L' L K H) :
  is_nat_trans _ _ (τ_data_from_σ h h' σ).
Show proof.
  red.
  intros c c' f.
  unfold τ_data_from_σ.
  etrans.
  { apply pathsinv0.
    simpl.
    apply φ_adj_natural_precomp.
  }
  apply pathsinv0.
  etrans.
  { apply pathsinv0.
    simpl.
    apply φ_adj_natural_postcomp.
  }
  apply maponpaths.
  etrans.
  2: {
    set (Hσ := nat_trans_ax σ).
    change (# L' (# K (# R f))) with ( # (K ∙ L') (#R f)).
    rewrite assoc.
    apply cancel_postcomposition.
    apply pathsinv0.
    apply Hσ.
  }
  rewrite <- assoc.
  rewrite <- functor_comp.
  rewrite <- assoc.
  apply cancel_precomposition.
  change (# (L ∙ H) (# R f)) with (# H (# (R ∙ L) f)).
  etrans.
  2: { apply (functor_comp H). }
  apply maponpaths.
  set (Hη := nat_trans_ax (counit_from_are_adjoints h)).
  apply pathsinv0.
  apply Hη.

Definition τ_from_σ {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R') (σ : DistrLaw L' L K H) :
  DistrLaw K H R R'.
Show proof.
  apply (make_nat_trans _ _ (τ_data_from_σ h h' σ)).
  apply is_nat_trans_τ_data_from_σ.

Lemma τ_from_σ_is_conjugate {C C' D D' : category} {L : functor D C} {R : functor C D}
           {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' }
           (h : are_adjoints L R) (h' : are_adjoints L' R') (hs : has_homsets C') (σ : DistrLaw L' L K H) : are_conjugates h h' σ (τ_from_σ h h' σ).
Show proof.
  red.
  intros A B g.
  unfold τ_from_σ; simpl.
  unfold τ_data_from_σ.
  set (ε := (counit_from_are_adjoints h)).
  etrans.
  2: { apply φ_adj_natural_precomp. }
  apply maponpaths.
  etrans.
  2: { set (Hσ := nat_trans_ax σ).
    rewrite assoc.
    apply cancel_postcomposition.
    apply pathsinv0.
    apply Hσ.
  }
  rewrite <- assoc.
  apply cancel_precomposition.
  change (# (L ∙ H) (φ_adj h g)) with (# H (# L (φ_adj h g))).
  etrans.
  2: { apply (functor_comp H). }
  apply maponpaths.
  apply pathsinv0.
  apply φ_adj_inv_after_φ_adj.

End Conjugates.

Section Liftings.

Definition is_lifting {C D: category} {F: functor C C} {G: functor D D} (H: functor C D) (HH: functor (FunctorAlg F) (FunctorAlg G)): UU.
Show proof.
  set (UF := forget_algebras F).
  set (UG := forget_algebras G).
  exact (UF ∙ H = HH ∙ UG).

Definition lifting_from_distr_law_data_on_ob {C D: category} {F: functor C C} {G: functor D D} {H: functor C D} (lambda : DistrLaw G F H H): FunctorAlg F → FunctorAlg G.
Show proof.
  intro Aa.
  set (A := alg_carrier _ Aa).
  set (a := alg_map _ Aa).
  set (B := H A).
  set (b := nat_trans_data_from_nat_trans lambda A · (# H a)).
  use tpair.
  - exact B.
  - exact b.

Lemma lifting_from_distr_law_data_aux {C D: category} {F: functor C C} {G: functor D D} {H: functor C D} (lambda : DistrLaw G F H H)(Aa Bb : algebra_ob F)(h : algebra_mor F Aa Bb)
  : is_algebra_mor G (lifting_from_distr_law_data_on_ob lambda Aa)
                     (lifting_from_distr_law_data_on_ob lambda Bb) (#H h).
Show proof.
  unfold is_algebra_mor.
  simpl.
  set (ax := nat_trans_ax lambda).
  apply pathsinv0.
  etrans.
  { rewrite assoc.
    apply cancel_postcomposition.
    apply ax. }
  rewrite <- assoc.
  apply pathsinv0.
  rewrite <- assoc.
  apply cancel_precomposition.
  set (h_commutes := algebra_mor_commutes _ _ _ h).
  rewrite <- functor_comp.
  apply pathsinv0.
  change (# (F ∙ H) h) with (# H (# F h)).
  etrans.
  { apply pathsinv0.
    apply (functor_comp H). }
  apply maponpaths.
  apply pathsinv0.
  apply h_commutes.

Definition lifting_from_distr_law_data {C D: category} {F: functor C C} {G: functor D D} {H: functor C D} (lambda : DistrLaw G F H H): functor_data (FunctorAlg F) (FunctorAlg G).
Show proof.
  use make_functor_data.
  - apply (lifting_from_distr_law_data_on_ob lambda).
  - cbn.
    intros Aa Bb.
    intro h.
    unfold algebra_mor.
    use tpair.
    + exact (#H (pr1 h)).
    + apply lifting_from_distr_law_data_aux.

Lemma is_functor_lifting_from_distr_law_data {C D: category} {F: functor C C} {G: functor D D} {H: functor C D} (lambda : DistrLaw G F H H): is_functor (lifting_from_distr_law_data lambda).
Show proof.
  split.
  - intro Aa.
    unfold lifting_from_distr_law_data.
    cbn.
    UniMath.MoreFoundations.Tactics.show_id_type.
    use total2_paths_f.
    2: { apply homset_property. }

    

    cbn.
    apply functor_id.
  - intros Aa Bb Cc f g.
    unfold lifting_from_distr_law_data.
    cbn.
    UniMath.MoreFoundations.Tactics.show_id_type.
    use total2_paths_f.
    2: { apply homset_property. }
    cbn.
    apply functor_comp.

Definition lifting_from_distr_law {C D: category} {F: functor C C} {G: functor D D} {H: functor C D} (lambda : DistrLaw G F H H): functor (FunctorAlg F) (FunctorAlg G).
Show proof.
  use tpair.
  - apply (lifting_from_distr_law_data lambda).
  - apply is_functor_lifting_from_distr_law_data.

Lemma lifting_from_distr_law_is_lifting {C D: category} {F: functor C C} {G: functor D D} (H: functor C D) (lambda : DistrLaw G F H H):
  is_lifting H (lifting_from_distr_law lambda ).
Show proof.
  unfold is_lifting.
  set (Hλ := lifting_from_distr_law lambda).
  apply functor_eq.
  - apply D.
  - apply idpath.

a simple preparation for the next lemma - strictly speaking, not even needed
Ltac get_sides_of_eq := match goal with |- @paths _ ?L ?R => set (left := L); set (right := R) end.

Arguments idtomor {_ _ _ } _.

unnamed result by Hinze & Wu, mentioned in their Sect. 3.2.1
Lemma liftings_from_distr_laws_compose {C C' C'': category}
      {F: functor C C} {F': functor C' C'} {F'': functor C'' C''}
      {H: functor C C'} {H': functor C' C''}
      (lambda : DistrLaw F' F H H)(lambda' : DistrLaw F'' F' H' H'):
  lifting_from_distr_law lambda ∙ lifting_from_distr_law lambda' =
  lifting_from_distr_law (H := H ∙ H') (comp_distr_laws lambda' lambda).
Show proof.
  apply functor_eq.
  { apply homset_property. }
  simpl.
  get_sides_of_eq.
  set (left' := functor_composite_data (lifting_from_distr_law_data lambda)
            (lifting_from_distr_law_data lambda')).
  set (right' := lifting_from_distr_law_data (comp_distr_laws lambda' lambda)
   : functor_data (FunctorAlg F) (FunctorAlg F'')).
  transparent assert (okonobs: (functor_on_objects left' ~ functor_on_objects right')).
  { intro alg.
    cbn. unfold lifting_from_distr_law_data_on_ob. cbn.
    apply (maponpaths (λ p, tpair _ (H' (H (alg_carrier F alg))) p )).
    abstract ( repeat rewrite id_left; rewrite id_right; rewrite <- assoc; apply maponpaths; apply functor_comp ).
  }
  
  apply (functor_data_eq_from_nat_trans _ _ _ _ okonobs).
  red.
  intros alg1 alg2 m.
  apply algebra_mor_eq.
  simpl.
  etrans.
  { apply cancel_precomposition.
    UniMath.MoreFoundations.Tactics.show_id_type.
    apply (idtomor_FunctorAlg_commutes _ _ _ (okonobs alg2)).
  }
  etrans.
  2: {
    apply cancel_postcomposition.
    UniMath.MoreFoundations.Tactics.show_id_type.
    apply pathsinv0.
    apply (idtomor_FunctorAlg_commutes _ _ _ (okonobs alg1)).
  }
  assert (Hyp: (idtomor (maponpaths (alg_carrier F'') (okonobs alg1)) = identity _) ×
               (idtomor (maponpaths (alg_carrier F'') (okonobs alg2)) = identity _)).
  { unfold okonobs; split.
    - etrans.
      { apply maponpaths.
        apply (maponpathscomp (λ p :
       C'' ⟦ F'' (H' (H (alg_carrier F alg1))), H' (H (alg_carrier F alg1)) ⟧,
       tpair (fun X: C'' => C'' ⟦ F'' X, X ⟧)
             (H' (H (alg_carrier F alg1))) p)
                              (alg_carrier F'')).
      }
      unfold funcomp.
      simpl.
      rewrite UniMath.MoreFoundations.PartA.maponpaths_for_constant_function.
      apply idpath.
    - etrans.
      { apply maponpaths.
        apply (maponpathscomp (λ p :
       C'' ⟦ F'' (H' (H (alg_carrier F alg2))), H' (H (alg_carrier F alg2)) ⟧,
       tpair (fun X: C'' => C'' ⟦ F'' X, X ⟧)
             (H' (H (alg_carrier F alg2))) p)
                              (alg_carrier F'')).
      }
      unfold funcomp.
      simpl.
      rewrite UniMath.MoreFoundations.PartA.maponpaths_for_constant_function.
      apply idpath.
  }
  induction Hyp as [Hyp1 Hyp2].
  rewrite Hyp1. rewrite Hyp2.
  rewrite id_right.
  apply pathsinv0.
  apply id_left.

End Liftings.

Section AdjointFolds.


Local Notation "↓ f" := (mor_from_algebra_mor _ f) (at level 3, format "↓ f").

Context {C D: category}
  {L: functor D C} {R: functor C D} (h : are_adjoints L R) {CC: functor C C} {DD: functor D D}
  (μDD_Initial : Initial (FunctorAlg DD))
  {σ: DistrLaw L L DD CC} {τ: DistrLaw DD CC R R} (hh: are_conjugates h h σ τ)
  {B: C} (b: CC B --> B).

Let AF := FunctorAlg CC.

Definition AlgConstr (A : C) (a : CC A --> A) : AF.
Show proof.
  exists B.
  exact b.

Let μDD: D := alg_carrier _ (InitialObject μDD_Initial).
Let inDD: DD(μDD) --> μDD := alg_map _ (InitialObject μDD_Initial).

Definition traho_of_Hinze_Wu : L μDD --> B.
Show proof.
  set (x := φ_adj_inv h ↓(InitialArrow μDD_Initial (lifting_from_distr_law τ (AlgConstr B b)))).
  exact x.

Definition φ_adj_traho_of_Hinze_Wu : algebra_mor DD (InitialObject μDD_Initial)
                                                 ((lifting_from_distr_law τ) (AlgConstr B b)).
Show proof.
  use tpair.
  - exact (φ_adj h traho_of_Hinze_Wu).
  - red.
    unfold traho_of_Hinze_Wu.
    rewrite φ_adj_after_φ_adj_inv.
    apply (algebra_mor_commutes _ _ _ (InitialArrow μDD_Initial (lifting_from_distr_law_data_on_ob τ (AlgConstr B b)))).

Lemma traho_of_Hinze_Wu_ok : #L inDD · traho_of_Hinze_Wu =
                             nat_trans_data_from_nat_trans σ μDD · # CC traho_of_Hinze_Wu · b.
Show proof.
  etrans.
  apply pathsinv0.
  use φ_adj_inv_after_φ_adj .
  exact R.
  exact h.
  apply pathsinv0.
  etrans.
  apply pathsinv0.
  use φ_adj_inv_after_φ_adj .
  exact R.
  exact h.
  apply maponpaths.

  etrans.
  use φ_adj_natural_postcomp.
  apply pathsinv0.
  etrans.
  use φ_adj_natural_precomp.
  apply pathsinv0.
  etrans.
  apply cancel_postcomposition.
  use hh .

  rewrite <- assoc.
  change (nat_trans_data_from_nat_trans τ B · # R b) with
      (alg_map DD ((lifting_from_distr_law τ) (AlgConstr B b))).

  apply pathsinv0.
  apply (algebra_mor_commutes DD _ _ φ_adj_traho_of_Hinze_Wu).

Definition φ_adj_h_x (x : C ⟦ L μDD, B ⟧)
  (Hyp: # DD (φ_adj h x) · alg_map DD ((lifting_from_distr_law τ)(AlgConstr B b)) =
        inDD · φ_adj h x):
  algebra_mor DD (InitialObject μDD_Initial) ((lifting_from_distr_law τ) (AlgConstr B b)).
Show proof.
  use tpair.
  - exact (φ_adj h x).
  - red.
    apply pathsinv0.
    apply Hyp.

Lemma φ_adj_h_x_equals_initial_arrow (x : C ⟦ L μDD, B ⟧) :
  # DD (φ_adj h x) · alg_map DD((lifting_from_distr_law τ)(AlgConstr B b)) =
  inDD · φ_adj h x ->
  φ_adj h x = ↓ (InitialArrow μDD_Initial ((lifting_from_distr_law τ) (AlgConstr B b))).
Show proof.
  intro Hyp.
  set (aux := InitialArrowUnique μDD_Initial _ (φ_adj_h_x x Hyp)).
  set (aux' := mor_from_algebra_mor _ (φ_adj_h_x x Hyp)).
  simpl in aux'.
  change (φ_adj h x) with (mor_from_algebra_mor _ (φ_adj_h_x x Hyp)).
  rewrite aux.
  apply idpath.

The following formalizes Theorem 5.2 (Adjoint folds) of Hinze and Wu.
Theorem TheoremOfHinzeAndWu :
  iscontr (∑ x : L μDD --> B, #L inDD · x = nat_trans_data_from_nat_trans σ μDD · # CC x · b).
Show proof.
  red.
  exists (traho_of_Hinze_Wu,, traho_of_Hinze_Wu_ok).

  intro t.
  induction t as [x hyp].
  assert (same: x = traho_of_Hinze_Wu).
  2: {
    apply subtypePath.
    + intro.
      simpl.
      apply C.
    + simpl.
      exact same.
  }

  etrans.
  { apply pathsinv0.
    apply (φ_adj_inv_after_φ_adj h).
  }
  etrans.
  2: {
    apply (φ_adj_inv_after_φ_adj h).
  }
  apply maponpaths.
  unfold traho_of_Hinze_Wu.
  rewrite (φ_adj_after_φ_adj_inv h).

  apply φ_adj_h_x_equals_initial_arrow.
  simpl.

  etrans.
  { rewrite assoc.
    apply cancel_postcomposition.
    apply pathsinv0.
    apply hh.
  }
  etrans.
  { apply pathsinv0.
    apply φ_adj_natural_postcomp.
  }
  etrans.
  2 : {
    apply φ_adj_natural_precomp.
  }
  apply maponpaths.
  apply pathsinv0.
  exact hyp.


End AdjointFolds.