Definition discrete_twosided_disp_cat_to_opcleaving (HD : discrete_twosided_disp_cat D) (HD' : discrete_twosided_opcleaving) : twosided_opcleaving D. Proof. intros x y₁ y₂ xy₁ g. simple refine (_ ,, _ ,, _). - exact (pr1 (HD' x y₁ y₂ xy₁ g)). - exact (pr12 (HD' x y₁ y₂ xy₁ g)). - apply (discrete_twosided_opcartesian_is_opcartesian HD). exact (pr22 (HD' x y₁ y₂ xy₁ g)). 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.