proposition: Lemma bicat_of_strict_cats_is_strict_bicat : is_strict_bicat bicat_of_strict_cats.
proof: Proof. use make_is_strict_bicat. - intros c d. repeat use isaset_total2. + apply funspace_isaset. apply d. + intro f ; simpl. repeat (use impred_isaset ; intro). apply (isaset_mor d). + intro. apply isasetaprop. apply isaprop_is_functor. apply d. - repeat use tpair. + intros c d f. use functor_eq. { apply d. } apply idpath. + intros c d f. use functor_eq. { apply d. } apply idpath. + intros a b c d f g h. use functor_eq. { apply d. } apply idpath. + intros c d f. use nat_trans_eq. { apply d. } intro x. etrans. { apply idtoiso_2_1_strict_cat. } apply idpath. + intros c d f. use nat_trans_eq. { apply d. } intro x. etrans. { apply idtoiso_2_1_strict_cat. } apply idpath. + intros a b c d f g h. use nat_trans_eq. { apply d. } intro x. etrans. { apply idtoiso_2_1_strict_cat. } apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Setcategories 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.Strictness UniMath.Bicategories.Core.Univalence