Lemma is_nat_trans_Abs_θ_data: is_nat_trans _ _ Abs_θ_data. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.BinSumOfSignatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.