Lemma CoproductIn2Commutes (a b : C) (CC : CoproductCocone a b): ∏ (c : C) (f : a --> c) g, CoproductIn2 CC · CoproductArrow CC f g = g. Proof. intros c f g. exact (binarySum_in_2_eqn CC f g). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.RepresentableFunctors.Representation.