Definition arrow_to_discrete_twosided_fibration_data : twosided_disp_functor_data (functor_identity C) (functor_identity C) (arrow_twosided_disp_cat C) D. Proof. simple refine (_ ,, _). - exact (λ x y f, discrete_twosided_cleaving_ob _ (pr122 D) (idD y) f). - cbn ; intros x₁ x₂ y₁ y₂ g₁ g₂ f₁ f₂ p. use discrete_twosided_cleaving_cartesian. refine (transportb (λ z, _ -->[ z ][ _ ] _) p (transportb (λ z, _ -->[ _ ][ z ] _) (id_right _ @ !(id_left _)) (discrete_twosided_cleaving_mor (pr1 D) (pr122 D) (idD y₁) g₁ ;;2 _))). apply f_idD. 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.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.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor.