Definition rel_double_cat_associator_data : double_associator_data rel_double_cat_hor_comp. Proof. intros W X Y Z R₁ R₂ R₃. use to_iso_rel_disp_cat. intros w z. split. - use factor_through_squash_hProp. intros ( x & p₁ & q ). revert q. use factor_through_squash_hProp. intros ( y & p₂ & p₃ ). use hinhpr. refine (y ,, _ ,, _). + use hinhpr. exact (x ,, p₁ ,, p₂). + exact p₃. - use factor_through_squash_hProp. intros ( y & q & p₃ ). revert q. use factor_through_squash_hProp. intros ( x & p₁ & p₂ ). use hinhpr. refine (x ,, _ ,, _). + exact p₁. + use hinhpr. exact (y ,, p₂ ,, p₃). 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.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Relations. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Categories.Rel. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. 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.SymmetricUnivalent. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints.