Definition fiber_fun_hset_twosided_disp_cat_comp {x₁ x₂ x₃ : C₁} (f₁ : x₃ --> x₂) (f₂ : x₂ --> x₁) {y₁ y₂ y₃ : C₂} (g₁ : y₁ --> y₂) (g₂ : y₂ --> y₃) (xy : fiber_hset_twosided_disp_cat HD x₁ y₁) : fiber_fun_hset_twosided_disp_cat (f₁ · f₂) (g₁ · g₂) xy = fiber_fun_hset_twosided_disp_cat f₁ g₂ (fiber_fun_hset_twosided_disp_cat f₂ g₁ xy).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration.