Definition fiber_fun_hset_twosided_disp_cat_comp_map {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 -->[ identity _ ][ identity _ ] fiber_fun_hset_twosided_disp_cat f₁ g₂ (fiber_fun_hset_twosided_disp_cat f₂ g₁ xy). Proof. unfold fiber_fun_hset_twosided_disp_cat. use discrete_twosided_opcleaving_opcartesian. pose (h₁ := discrete_twosided_opcleaving_mor _ (pr2 HD') (discrete_twosided_cleaving_ob (pr1 D) (pr1 HD') (discrete_twosided_opcleaving_ob (pr1 D) (pr2 HD') (discrete_twosided_cleaving_ob (pr1 D) (pr1 HD') xy f₂) g₁) f₁) g₂). refine (transportb (λ z, _ -->[ _ ][ z ] _) (id_right _) (_ ;;2 h₁)). use discrete_twosided_cleaving_cartesian. pose (h₂ := discrete_twosided_opcleaving_mor _ (pr2 HD') (discrete_twosided_cleaving_ob (pr1 D) (pr1 HD') xy f₂) g₁). refine (transportb (λ z, _ -->[ z ][ _ ] _) (id_left _ @ !(id_right _)) (transportb (λ z, _ -->[ _ ][ z ] _) (id_right _ @ !(id_left _)) (_ ;;2 h₂))). use discrete_twosided_cleaving_cartesian. pose (h₃ := discrete_twosided_cleaving_mor _ (pr1 HD') xy (f₁ · f₂)). exact (transportb (λ z, _ -->[ _ ][ z ] _) (id_right _) h₃). 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.