Lemma strict_bicat_to_two_cat_to_strict_bicat (C : strict_bicat) : two_cat_to_strict_bicat (strict_bicat_to_two_cat C) = C. Proof. use subtypePath. { intro. apply isaprop_is_strict_bicat. } use subtypePath. { intro. do 4 (apply impred ; intro). apply isapropisaset. } use total2_paths2_f. - use total2_paths2_f. + apply idpath. + cbn. repeat use pathsdirprod ; try apply idpath. * use funextsec. intro x. use funextsec. intro y. use funextsec. intro f. rewrite !idto2mor_idtoiso. apply idtoiso_plunitor. * use funextsec. intro x. use funextsec. intro y. use funextsec. intro f. rewrite !idto2mor_idtoiso. apply idtoiso_prunitor. * use funextsec. intro x. use funextsec. intro y. use funextsec. intro f. rewrite !idto2mor_idtoiso. rewrite idtoiso_2_1_inv ; simpl. refine (!(id2_right _) @ _). use vcomp_move_R_pM. { is_iso. } simpl. refine (!_). etrans. { apply maponpaths_2. apply idtoiso_plunitor. } apply lunitor_linvunitor. * use funextsec. intro x. use funextsec. intro y. use funextsec. intro f. rewrite !idto2mor_idtoiso. rewrite idtoiso_2_1_inv ; simpl. refine (!(id2_right _) @ _). use vcomp_move_R_pM. { is_iso. } simpl. refine (!_). etrans. { apply maponpaths_2. apply idtoiso_prunitor. } apply runitor_rinvunitor. * use funextsec ; intro w. use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro z. use funextsec ; intro f. use funextsec ; intro g. use funextsec ; intro h. rewrite !idto2mor_idtoiso. rewrite idtoiso_2_1_inv ; simpl. refine (!(id2_right _) @ _). use vcomp_move_R_pM. { is_iso. } simpl. refine (!_). etrans. { apply maponpaths_2. apply idtoiso_plassociator. } apply lassociator_rassociator. * use funextsec ; intro w. use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro z. use funextsec ; intro f. use funextsec ; intro g. use funextsec ; intro h. rewrite !idto2mor_idtoiso. apply idtoiso_plassociator. - apply isaprop_prebicat_laws. intros. apply cellset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.TwoCategories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.TransportLaws.