Definition make_isBinProductCone (hsC : has_homsets C) (a b p : C) (pa : C⟦p,a⟧) (pb : C⟦p,b⟧) : (∏ (c : C) (f : C⟦c,a⟧) (g : C⟦c,b⟧), ∃! k : C⟦c,p⟧, k · pa = f × k · pb = g) -> isBinProductCone a b p pa pb. Proof. intros H c cc. simpl in *. set (H' := H c (coneOut cc true) (coneOut cc false)). use tpair. - exists (pr1 (pr1 H')). set (T := pr2 (pr1 H')); simpl in T. abstract (intro u; induction u; simpl; [exact (pr1 T)|exact (pr2 T)]). - abstract (simpl; intros; apply subtypePath; [intro; apply impred;intro; apply hsC|]; simpl; apply path_to_ctr; split; [ apply (pr2 t true) | apply (pr2 t false) ]). 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.