Proposition is_opcartesian_equiv_over_id_unique : isaprop (∑ (gg : L x xx -->[ g ] ww), ♯L ff ;; gg = hh). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply D₂. } use (invmaponpathsweq (make_weq _ (is_equiv_over_id_to_ff _ (equiv_inv _ HL) _ _ _ _ _))). cbn. refine (id_left_disp_var _ @ _ @ !(id_left_disp_var _)). apply maponpaths. etrans. { apply maponpaths_2. exact (!(transportf_transpose_left (z_iso_disp_after_inv_mor (is_z_iso_unit_over_id HL _ _)))). } refine (!_). etrans. { apply maponpaths_2. exact (!(transportf_transpose_left (z_iso_disp_after_inv_mor (is_z_iso_unit_over_id HL _ _)))). } refine (!_). rewrite !mor_disp_transportf_postwhisker. apply maponpaths. rewrite !assoc_disp_var. do 2 apply maponpaths. use (opcartesian_factorisation_unique Hff). rewrite !assoc_disp. apply maponpaths. etrans. { apply maponpaths_2. exact (disp_nat_trans_ax η ff). } refine (!_). etrans. { apply maponpaths_2. exact (disp_nat_trans_ax η ff). } cbn. unfold transportb. rewrite !mor_disp_transportf_postwhisker. apply maponpaths. rewrite !assoc_disp_var. do 2 apply maponpaths. refine (!(disp_functor_comp_var R _ _) @ _ @ disp_functor_comp_var R _ _). do 2 apply maponpaths. exact (pr2 φ₂ @ !(pr2 φ₁)). Qed.
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.