Definition isofhlevel_equifier {n : nat} {X Y : UU} (HX : isofhlevel n X) (HY : isofhlevel n Y) {f g : X → Y} (p₁ p₂ : f ~ g) : isofhlevel n (equifier_type p₁ p₂). Proof. use isofhlevel_equifier_help. - exact HX. - apply hlevelntosn. apply hlevelntosn. exact HY. 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.