Definition δ_genoption_mor (Ze : Ptd) (c : C) : C ⟦ BinCoproductObject (CC A (pr1 Ze c)), pr1 Ze (BinCoproductObject (CC A c)) ⟧. Proof. apply (@BinCoproductArrow _ _ _ (CC A (pr1 Ze c)) (pr1 Ze (BinCoproductObject (CC A c)))). - apply (BinCoproductIn1 (CC A c) · pr2 Ze (BinCoproductObject (CC A c))). - apply (# (pr1 Ze) (BinCoproductIn2 (CC A c))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. 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.whiskering. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.PointedFunctorsComposition.