Lemma idtoiso_2_1_strict_cat {c d : bicat_of_strict_cats} {f g : functor (pr1 c) (pr1 d)} (p : pr1 f = pr1 g) (x : pr1 c) : pr11 (@idtoiso_2_1 bicat_of_strict_cats _ _ f g (functor_eq _ _ (isaset_mor d) f g p)) x = idtoiso (maponpaths (λ q, pr1 q x) p). Proof. induction f as [f Hf]. induction g as [g Hg]. simpl in *. induction p. apply idtoiso_2_1_strict_cat_help. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.Univalence.