proposition: Proposition idtoiso_2_1_in_bicat_of_univ_cats {C₁ C₂ : bicat_of_univ_cats} {F G : C₁ --> C₂} (p : F = G) (x : pr1 C₁) : pr11 (@idtoiso_2_1 bicat_of_univ_cats C₁ C₂ F G p) x = idtoiso (maponpaths (λ H, pr11 H x) p).
proof: Proof. induction p ; cbn. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.catiso UniMath.CategoryTheory.CategoryEquality UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.AdjointUnique UniMath.Bicategories.Core.Univalence