Definition φ_adj_h_x (x : C ⟦ L μDD, B ⟧) (Hyp: # DD (φ_adj h x) · alg_map DD ((lifting_from_distr_law τ)(AlgConstr B b)) = inDD · φ_adj h x): algebra_mor DD (InitialObject μDD_Initial) ((lifting_from_distr_law τ) (AlgConstr B b)). Proof. use tpair. - exact (φ_adj h x). - red. apply pathsinv0. apply Hyp. 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.