Definition ptd_compose (Z Z' : ptd_obj C) : category_Ptd C. Proof. exists (functor_compose (pr1 Z:[C, C]) (pr1 Z':[C, C])). apply (# (functorial_composition _ _ _) (((ptd_pt _ Z: [C, C]⟦functor_identity C,pr1 Z⟧) ,, (ptd_pt _ Z': [C, C]⟦functor_identity C,pr1 Z'⟧)) : category_binproduct [C, C] [C, C] ⟦(functor_identity C,,functor_identity C),(pr1 Z,,pr1 Z')⟧)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.HorizontalComposition.