Definition twosided_opcleaving_mor (H : twosided_opcleaving) {x : C₁} {y₁ y₂ : C₂} (xy₁ : D x y₁) (g : y₁ --> y₂) : xy₁ -->[ identity _ ][ g ] twosided_opcleaving_ob H xy₁ g := pr12 (H x y₁ y₂ xy₁ g).
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.