Definition set_rel_double_cat_hor_comp_data : hor_comp_data set_rel_disp_cat. Proof. use make_hor_comp_data. - refine (λ (X Y Z : hSet) R₁ R₂ x z, make_hSet (∑ (y : Y), R₁ x y × R₂ y z) _). abstract (use isaset_total2 ; [ apply setproperty | ] ; intro ; apply isasetdirprod ; apply setproperty). - exact (λ (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : hSet) (f : X₁ → X₂) (g : Y₁ → Y₂) (h : Z₁ → Z₂) (R₁ : X₁ → Y₁ → hSet) (S₁ : Y₁ → Z₁ → hSet) (R₂ : X₂ → Y₂ → hSet) (S₂ : Y₂ → Z₂ → hSet) (fR : ∏ (x : X₁) (y : Y₁), R₁ x y → R₂ (f x) (g y)) (gR : ∏ (x : Y₁) (y : Z₁), S₁ x y → S₂ (g x) (h y)) (x : X₁) (z : Z₁) (p : ∑ (y : Y₁), R₁ x y × S₁ y z), g (pr1 p) ,, fR _ _ (pr12 p) ,, gR _ _ (pr22 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.