Definition has_equifiers_one_types : has_equifiers one_types. Proof. intros X Y f g p₁ p₂. simple refine (_ ,, _ ,, _ ,, _). - exact (equifier_HLevel p₁ p₂). - exact (one_types_equifier_pr1 p₁ p₂). - exact (one_types_equifier_eq p₁ p₂). - simple refine (_ ,, _ ,, _). + exact (one_types_equifier_ump_1 p₁ p₂). + exact (one_types_equifier_ump_2 p₁ p₂). + exact (one_types_equifier_ump_eq p₁ p₂). 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.