proposition: 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))).
proof: 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. 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