Proposition bicat_to_twosided_disp_cat_axioms : twosided_disp_cat_axioms bicat_to_twosided_disp_cat_data. Proof. repeat split. - intros x₁ x₂ y₁ y₂ f g p q s. induction p, q ; cbn in *. refine (_ @ id2_left _). apply maponpaths_2. etrans. { apply maponpaths_2. rewrite vassocl. rewrite linvunitor_lunitor. apply id2_right. } apply runitor_rinvunitor. - intros x₁ x₂ y₁ y₂ f g p q s. induction p, q ; cbn in *. refine (_ @ id2_right _). rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite vassocr. rewrite rinvunitor_runitor. apply id2_left. } apply lunitor_linvunitor. - intros x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ f₁ f₂ f₃ f₄ p₁ p₂ p₃ q₁ q₂ q₃ s₁ s₂ s₃. induction p₁, p₂, p₃, q₁, q₂, q₃ ; cbn in *. rewrite !vassocr. apply idpath. - intros x₁ x₂ y₁ y₂ f g p q. apply cellset_property. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats.