proposition: 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: 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.
imports: UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Adjunctions.Core