Definition one_types_pb_ump_1 : pb_ump_1 (one_types_pb_cone f g). Proof. intro q. use make_pb_1cell. - exact (λ x, (pb_cone_pr1 q x ,, pb_cone_pr2 q x) ,, !(pr1 (pb_cone_cell q) x)). - use make_invertible_2cell. + intro x ; cbn. apply idpath. + apply one_type_2cell_iso. - use make_invertible_2cell. + intro x ; cbn. apply idpath. + apply one_type_2cell_iso. - abstract (use funextsec ; intro x ; cbn ; unfold homotcomp, homotfun, invhomot ; cbn ; rewrite !pathscomp0rid ; apply pathsinv0inv0). 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.