Lemma is_nat_trans_Abs_θ_data_data (XZ: [C, C] ⊠ category_Ptd C): is_nat_trans _ _ (Abs_θ_data_data XZ). Proof. intros c c' f. unfold Abs_θ_data_data. simpl. rewrite <- functor_comp. rewrite <- functor_comp. apply maponpaths. etrans. { apply precompWithBinCoproductArrow. } etrans; [| apply (!(postcompWithBinCoproductArrow _ _ _ _ _)) ]. simpl. rewrite id_left. rewrite <- assoc. rewrite <- functor_comp. rewrite <- functor_comp. apply maponpaths_12. + assert (NN := nat_trans_ax (pr2 (pr2 XZ)) _ _ (BinCoproductOfArrows C (CC (TerminalObject terminal) c) (CC (TerminalObject terminal) c') (identity (TerminalObject terminal)) f)). match goal with |[ H1: _ = ?f·?g |- _ = ?h · _ ] => intermediate_path (h·(f·g)) end. * rewrite <- NN. clear NN. unfold functor_identity. simpl. rewrite assoc. rewrite BinCoproductOfArrowsIn1. rewrite id_left. apply idpath. * apply idpath. + apply maponpaths. etrans; [| apply (!(BinCoproductOfArrowsIn2 _ _ _ _ _ )) ]. apply idpath. 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.