Definition equifier_HLevel {n : nat} {X Y : HLevel n} {f g : pr1 X → pr1 Y} (p₁ p₂ : f ~ g) : HLevel n. Proof. simple refine (_ ,, _). - exact (equifier_type p₁ p₂). - apply isofhlevel_equifier. + exact (pr2 X). + exact (pr2 Y). 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.