Definition thetahat (Z : Ptd) (f : Z --> ptdInitAlg) : EndEndC ⟦ functor_composite Id_H (ℓ (U Z)), functor_composite (ℓ (U Z)) (Ghat) ⟧. Proof. exact (iso1' Z · thetahat_0 Z f · iso2' Z). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. 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.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation.