Definition φ_adj_traho_of_Hinze_Wu : algebra_mor DD (InitialObject μDD_Initial) ((lifting_from_distr_law τ) (AlgConstr B b)). 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)))). Defined.
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.