Definition isofhlevel_inserter {n : nat} {X Y : UU} (HX : isofhlevel n X) (HY : isofhlevel n Y) (f g : X → Y) : isofhlevel n (inserter_type f g). Proof. use isofhlevel_inserter_help. - exact HX. - 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.