Definition one_types_inserter_ump_2 {X Y : one_types} (f g : X --> Y) : has_inserter_ump_2 (one_types_inserter_cone f g). Proof. intros W u₁ u₂ p r. simple refine (_ ,, _). - intro x. use total2_paths_f. + exact (p x). + abstract (rewrite transportf_paths_FlFr ; use path_inv_rotate_ll ; pose (eqtohomot r x) as r' ; cbn in r' ; unfold homotcomp, funhomotsec, homotfun in r' ; cbn in r' ; rewrite !pathscomp0rid in r' ; exact r'). - abstract (use funextsec ; intro x ; cbn ; unfold homotfun ; apply base_total2_paths). 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.