Definition has_inserters_one_types : has_inserters one_types. Proof. intros X Y f g. simple refine (_ ,, _ ,, _ ,, _). - exact (inserter_HLevel f g). - exact (inserter_type_pr1 f g). - exact (inserter_type_path f g). - simple refine (_ ,, _ ,, _). + exact (one_types_inserter_ump_1 f g). + exact (one_types_inserter_ump_2 f g). + exact (one_types_inserter_ump_eq f g). 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.