Definition is_cartesian_equiv_over_id_fact : ww -->[ g ] L y yy. Proof. pose (cartesian_factorisation Hff _ (transportf (λ z, _ -->[ z ] _) (id_right _) (♯R hh ;; inv_mor_disp_from_z_iso (is_z_iso_unit_over_id HL x xx)))) as m. exact (transportf (λ z, _ -->[ z ] _) (id_left _) (inv_mor_disp_from_z_iso (is_z_iso_counit_over_id HL w ww) ;; ♯L m)). 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.