Definition make_MorphismPair {a b c : C} (f : a --> b) (g : b --> c) : MorphismPair. Proof. use tpair. - exact a. - use tpair. + exact b. + use tpair. * exact c. * use make_dirprod. -- exact f. -- exact g. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Opp.