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