Proposition are_conjoints_coreflections_double_cat_left : transportf_square (id_v_left (identity_v yy · identity_v yy) @ id_v_left (identity_v yy)) (id_v_left (identity_v xx · identity_v xx) @ id_v_left (identity_v xx)) (rinvunitor_h r ⋆v (εε ⋆h ηη ⋆v lunitor_h r)) = id_v_square r. Proof. rewrite transportf_square_coreflections_double_cat. rewrite idto2mor_lwhisker. rewrite idto2mor_rwhisker. rewrite rinvunitor_h_coreflections. rewrite lunitor_h_coreflections. rewrite comp_h_square_coreflections. rewrite !comp_v_square_coreflections. rewrite <- !TwoCategories.rwhisker_vcomp. rewrite <- !TwoCategories.lwhisker_vcomp. rewrite !idto2mor_lwhisker. rewrite !idto2mor_rwhisker. rewrite !idto2mor_lwhisker. rewrite !TwoCategories.vassocr. rewrite !idto2mor_comp. rewrite !TwoCategories.vassocl. rewrite !idto2mor_comp. etrans. { apply maponpaths. apply maponpaths_2. refine (id1_lwhisker _ @ _). apply maponpaths_2. apply maponpaths. apply rwhisker_id1. } unfold two_cat_lunitor, two_cat_runitor, two_cat_rinvunitor, two_cat_linvunitor. rewrite !TwoCategories.vassocr. rewrite !idto2mor_comp. rewrite !TwoCategories.vassocl. etrans. { do 2 apply maponpaths. rewrite !TwoCategories.vassocr. rewrite !idto2mor_comp. apply maponpaths_2. apply maponpaths. refine (id1_lwhisker _ @ _). apply maponpaths_2. apply maponpaths. apply rwhisker_id1. } unfold two_cat_lunitor, two_cat_runitor, two_cat_rinvunitor, two_cat_linvunitor. etrans. { do 2 apply maponpaths. rewrite !TwoCategories.vassocr. rewrite !idto2mor_comp. rewrite !TwoCategories.vassocl. rewrite !idto2mor_comp. apply idpath. } rewrite id_v_square_coreflections. unfold ηη, εε. rewrite <- !TwoCategories.rwhisker_vcomp. rewrite <- !TwoCategories.lwhisker_vcomp. unfold two_cat_runitor, two_cat_rinvunitor. rewrite !idto2mor_lwhisker. rewrite !idto2mor_rwhisker. rewrite !TwoCategories.vassocr. rewrite !idto2mor_comp. rewrite !TwoCategories.vassocl. rewrite !idto2mor_comp. etrans. { apply maponpaths. rewrite !TwoCategories.vassocr. apply maponpaths_2. apply right_triangle. } rewrite !idto2mor_comp. apply maponpaths. apply (homset_property C). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.TwoCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.SquaresTwoCat. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints. Require Import UniMath.Bicategories.DoubleCategories.Examples.SquareDoubleCatTwo. Require Import UniMath.Bicategories.DoubleCategories.Examples.DoubleCatOnDispCat. Import TwoCategories.Notations.