Definition rel_double_cat_hor_comp_data : hor_comp_data rel_disp_cat. Proof. use make_hor_comp_data. - exact (λ (X Y Z : hSet) R₁ R₂ x z, ∃ (y : Y), R₁ x y × R₂ y z). - abstract (refine (λ (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : hSet) (f : X₁ → X₂) (g : Y₁ → Y₂) (h : Z₁ → Z₂) (R₁ : X₁ → Y₁ → hProp) (S₁ : Y₁ → Z₁ → hProp) (R₂ : X₂ → Y₂ → hProp) (S₂ : Y₂ → Z₂ → hProp) fR gR x z, _) ; use factor_through_squash_hProp ; intros ( y & p & q ) ; use hinhpr ; exact (g y ,, fR _ _ p ,, gR _ _ q)). 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.