Definition bincoprod_of_precategory_ob_mor (C₁ C₂ : category) : precategory_ob_mor. Proof. use make_precategory_ob_mor. - exact (C₁ ⨿ C₂). - intros z₁ z₂. induction z₁ as [ x₁ | y₁ ], z₂ as [ x₂ | y₂ ]. + exact (x₁ --> x₂). + exact ∅. + exact ∅. + exact (y₁ --> y₂). Defined.
Require Import UniMath.Foundations.All. 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.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering.