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. 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). Qed.
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.