Definition traho_of_Hinze_Wu : L μDD --> B. Proof. set (x := φ_adj_inv h ↓(InitialArrow μDD_Initial (lifting_from_distr_law τ (AlgConstr B b)))). exact x. 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.