proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.TwoCategories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Categories.HSET.All UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.TransportLaws