Definition fiber_fun_hset_twosided_disp_cat_id_map {x : C₁} {y : C₂} (xy : fiber_hset_twosided_disp_cat HD x y) : fiber_fun_hset_twosided_disp_cat (identity x) (identity y) xy -->[ identity _ ][ identity _ ] xy. Proof. unfold fiber_fun_hset_twosided_disp_cat. use discrete_twosided_opcleaving_opcartesian. refine (transportb (λ z, _ -->[ z ][ _ ] _) _ (transportb (λ z, _ -->[ _ ][ z ] _) _ (discrete_twosided_cleaving_mor _ (pr1 HD') xy (identity x)))). - exact (id_right _). - exact (id_right _). Defined.
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.