Definition G_Thm15 (X : EndC) := coproduct_functor _ _ CPEndC (constant_functor _ _ X) H. *) Local Lemma aux_iso_2_inv_is_nat_trans (Z : Ptd) : is_nat_trans (pr1 (BinCoproductObject (CPEndEndC (constant_functor [C, C] [C, C] (U Z)) (functor_fix_snd_arg [C, C] Ptd [C, C](θ_target H) Z))) ) (functor_composite (ℓ (U Z)) (Const_plus_H (U Z))) (λ X : [C, C], nat_trans_id (BinCoproductObject (CPEndC (U Z) ((θ_target H) (X ⊗ Z))) :functor C C)). Proof. intros X X' α. rewrite (@id_left EndC). rewrite (@id_right EndC). apply nat_trans_eq_alt. intro c; simpl. unfold coproduct_nat_trans_data, coproduct_nat_trans_in1_data, coproduct_nat_trans_in2_data; simpl. apply (maponpaths_12 (BinCoproductOfArrows _ _ _)). + apply idpath. + unfold functor_fix_snd_arg_mor; simpl. revert c. apply nat_trans_eq_pointwise. apply maponpaths. apply nat_trans_eq_alt. intro c. simpl. rewrite (functor_id X). apply id_left. Qed. Local Definition aux_iso_2_inv (Z : Ptd) : EndEndC ⟦ BinCoproductObject (CPEndEndC (constant_functor [C, C] [C, C] (U Z)) (functor_fix_snd_arg [C, C] Ptd [C, C] (θ_target H) Z)), functor_composite (ℓ (U Z) ) (Const_plus_H (U Z)) ⟧. Proof. use tpair. - intro X. exact (nat_trans_id ((@BinCoproductObject EndC (U Z) (θ_target H (X⊗Z)) (CPEndC _ _) ) : functor C C)). - exact (aux_iso_2_inv_is_nat_trans 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.SimplifiedHSS.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.