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