Definition PullbCone {a b c : C} (f : C ⟦b,a⟧) (g : C⟦c,a⟧) (d : C) (f' : C ⟦d, b⟧) (g' : C ⟦d,c⟧) (H : f' · f = g'· g) : cone (pullback_diagram f g) d. Proof. use make_cone. - use three_rec_dep; try assumption. apply (f' · f). - use three_rec_dep; use three_rec_dep. + exact (empty_rect _ ). + intro x; apply idpath. + exact (empty_rect _ ). + exact (empty_rect _ ). + exact (empty_rect _ ). + exact (empty_rect _ ). + exact (empty_rect _ ). + intro x; apply (!H). + exact (empty_rect _ ). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.