Definition has_iso_inserter_ump_eq : UU := ∏ (x : B) (u₁ u₂ : x --> cone) (α : u₁ · iso_inserter_cone_pr1 cone ==> u₂ · iso_inserter_cone_pr1 cone) (p : rassociator _ _ _ • (u₁ ◃ iso_inserter_cone_cell cone) • lassociator _ _ _ • (α ▹ g) = (α ▹ f) • rassociator _ _ _ • (u₂ ◃ iso_inserter_cone_cell cone) • lassociator _ _ _) (φ₁ φ₂ : u₁ ==> u₂) (q₁ : φ₁ ▹ iso_inserter_cone_pr1 cone = α) (q₂ : φ₂ ▹ iso_inserter_cone_pr1 cone = α), φ₁ = φ₂.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.Categories.CatIsoInserter. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms.