Definition BinProductArrow {a b : C} (P : BinProductCone a b) {c : C} (f : C⟦c,a⟧) (g : C⟦c,b⟧) : C⟦c,BinProductObject P⟧. Proof. apply (limArrow P). use make_cone. - intro v; induction v; [ apply f | apply g ]. - intros ? ? e; induction e. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.