Definition bicat_to_associator_data : double_associator_data bicat_to_hor_comp. Proof. intros w x y z f g h. use make_iso_twosided_disp. - exact (runitor _ • lassociator _ _ _ • linvunitor _). - simple refine (_ ,, _ ,, _). + exact (runitor _ • rassociator _ _ _ • linvunitor _). + abstract (cbn ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; refine (_ @ id2_right _) ; apply maponpaths ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite linvunitor_lunitor ; rewrite id2_left ; rewrite rinvunitor_runitor ; rewrite id2_left ; apply lassociator_rassociator). + abstract (cbn ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; refine (_ @ id2_right _) ; apply maponpaths ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite linvunitor_lunitor ; rewrite id2_left ; rewrite rinvunitor_runitor ; rewrite id2_left ; apply rassociator_lassociator). Defined.
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.