Definition bicat_to_lunitor_data : double_lunitor_data bicat_to_hor_id bicat_to_hor_comp. Proof. intros x y f. use make_iso_twosided_disp. - exact (runitor _). - simple refine (_ ,, _ ,, _). + exact (runitor _ • linvunitor _ • linvunitor _). + abstract (cbn ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; refine (_ @ id2_left _) ; apply maponpaths_2 ; rewrite !vassocl ; rewrite (maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite rinvunitor_runitor ; rewrite id2_left ; apply lunitor_linvunitor). + abstract (cbn ; rewrite !vassocl ; apply maponpaths ; refine (_ @ id2_right _) ; apply maponpaths ; rewrite rinvunitor_runitor ; rewrite id2_right ; apply linvunitor_lunitor). 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.