Definition is_opcartesian_equiv_over_id_fact : L x xx -->[ g ] ww. Proof. pose (opcartesian_factorisation Hff _ (transportf (λ z, _ -->[ z ] _) (id_left _) (η y yy ;; ♯R hh))) as m. exact (transportf (λ z, _ -->[ z ] _) (id_right _) (♯L m ;; ε w ww)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq.