Definition pullback_diagram {a b c : C} (f : C ⟦b,a⟧) (g : C⟦c,a⟧) : diagram pullback_graph C. Proof. exists (three_rec b a c). use three_rec_dep. - use three_rec_dep; simpl. + apply fromempty. + intro x; assumption. + apply fromempty. - intro x; apply fromempty. - use three_rec_dep; simpl. + apply fromempty. + intro x; assumption. + apply fromempty. 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.