Lemma bicat_of_strict_cats_is_strict_bicat : is_strict_bicat bicat_of_strict_cats. 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.
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.