proposition: Lemma is_nat_trans_Abs_θ_data: is_nat_trans _ _ Abs_θ_data.
proof: Proof. red. intros XZ XZ' αβ. destruct XZ as [X [Z e]]. destruct XZ' as [X' [Z' e']]. destruct αβ as [α β]. simpl in *. apply nat_trans_eq; [apply homset_property |]. intro c. simpl. unfold constant_functor. simpl. rewrite assoc. unfold Abs_θ_data_data. simpl. rewrite (nat_trans_ax α). etrans. 2: { apply cancel_postcomposition. apply functor_comp. } rewrite (nat_trans_ax α). rewrite <- assoc. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } apply maponpaths. unfold constant_functor_data. simpl. etrans; [ apply precompWithBinCoproductArrow |]. rewrite id_left. etrans. 2: { eapply pathsinv0. apply postcompWithBinCoproductArrow. } apply BinCoproductArrowUnique. - rewrite BinCoproductIn1Commutes. rewrite <- assoc. apply maponpaths. apply pathsinv0, (ptd_mor_commutes _ β). - rewrite BinCoproductIn2Commutes. apply pathsinv0, (nat_trans_ax β). Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.PrecategoryBinProduct UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.BinSumOfSignatures UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits