Definition Abs_θ_data_data: ∏ XZ c, pr1 (θ_source Abs_H XZ) c --> pr1 (θ_target Abs_H XZ) c. Proof. intros XZ c. simpl. apply (functor_on_morphisms (functor_data_from_functor _ _ (pr1 XZ))). unfold constant_functor. simpl. apply BinCoproductArrow. + exact (BinCoproductIn1 _ · nat_trans_data_from_nat_trans (pr2 (pr2 XZ)) (BinCoproductObject (CC (TerminalObject terminal) c))). + exact (# (pr1 (pr2 XZ)) (BinCoproductIn2 (CC (TerminalObject terminal) c))). Defined.
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.