Definition set_rel_double_cat_associator_data : double_associator_data set_rel_double_cat_hor_comp. Proof. refine (λ (W X Y Z : hSet) (R₁ : W → X → hSet) (R₂ : X → Y → hSet) (R₃ : Y → Z → hSet), _). use to_iso_set_rel_disp_cat. intros w z. cbn. use weq_iso. - simple refine (λ p, _ ,, (_ ,, _ ,, _) ,, _). + exact (pr1 (pr22 p)). + exact (pr1 p). + exact (pr12 p). + exact (pr12 (pr22 p)). + exact (pr22 (pr22 p)). - simple refine (λ p, _ ,, _ ,, (_ ,, _ ,, _)). + exact (pr1 (pr12 p)). + exact (pr12 (pr12 p)). + exact (pr1 p). + exact (pr22 (pr12 p)). + exact (pr22 p). - abstract (intro p ; apply idpath). - abstract (intro p ; apply idpath). 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.