Definition pushout_graph : graph. Proof. exists three. use three_rec. - apply three_rec. + apply empty. + apply unit. + apply unit. - apply (λ _, empty). - apply three_rec. + apply empty. + apply empty. + apply empty. 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. Require Import UniMath.CategoryTheory.Limits.Pushouts.