Definition one_types_equifier_ump_2 {X Y : one_types} {f g : X --> Y} (p₁ p₂ : f ==> g) : has_equifier_ump_2 (one_types_equifier_cone p₁ p₂). Proof. intros W u₁ u₂ α. simple refine (_ ,, _). - intro x. use total2_paths_f. + exact (α x). + apply Y. - abstract (use funextsec ; intro x ; cbn ; apply base_total2_paths). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Inserters. Require Import UniMath.Bicategories.Limits.Equifiers.