Definition one_types_pb_ump_2 : pb_ump_2 (one_types_pb_cone f g). Proof. intros W φ ψ α β r. use iscontraprop1. - abstract (use invproofirrelevance ; intros τ₁ τ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; use funextsec ; intro x ; use homot_hfp_one_type ; [ apply Z | exact (eqtohomot (pr12 τ₁) x @ !(eqtohomot (pr12 τ₂) x)) | exact (eqtohomot (pr22 τ₁) x @ !(eqtohomot (pr22 τ₂) x)) ]). - simple refine (_ ,, _). + intro x. use path_hfp. * exact (α x). * exact (β x). * abstract (pose (eqtohomot r x) as p ; cbn in p ; unfold homotcomp, funhomotsec, homotfun in p ; cbn in p ; rewrite !pathscomp0rid in p ; use hornRotation_lr ; rewrite !path_assoc ; refine (_ @ maponpaths (λ z, z @ _) (!p)) ; rewrite <- !path_assoc ; rewrite pathsinv0l ; rewrite pathscomp0rid ; apply idpath). + split. * abstract (use funextsec ; intro x ; apply maponpaths_hfpg_path_hfp). * abstract (use funextsec ; intro x ; apply maponpaths_hfpg'_path_hfp). 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.