proposition: Lemma is_nat_trans_Abs_θ_data_data (XZ: [C, C] ⊠ category_Ptd C): is_nat_trans _ _ (Abs_θ_data_data XZ).
proof: 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.
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