Definition one_types_equifier_ump_1 {X Y : one_types} {f g : X --> Y} (p₁ p₂ : f ==> g) : has_equifier_ump_1 (one_types_equifier_cone p₁ p₂). Proof. intro q. use make_equifier_1cell. - refine (λ x, equifier_cone_pr1 q x ,, _). abstract (exact (eqtohomot (equifier_cone_eq q) x)). - use make_invertible_2cell. + exact (λ x, idpath _). + apply one_type_2cell_iso. 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.