proposition: Proposition is_cartesian_equiv_over_id_unique : isaprop (∑ (gg : ww -->[ g ] L y yy), gg ;; ♯ L ff = hh).
proof: 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_right_disp_var _ @ _ @ !(id_right_disp_var _)). apply maponpaths. etrans. { apply maponpaths. exact (!(transportf_transpose_left (z_iso_disp_after_inv_mor (is_z_iso_unit_over_id HL y yy)))). } refine (!_). etrans. { apply maponpaths. exact (!(transportf_transpose_left (z_iso_disp_after_inv_mor (is_z_iso_unit_over_id HL y yy)))). } refine (!_). rewrite !mor_disp_transportf_prewhisker. apply maponpaths. rewrite !assoc_disp. apply maponpaths. apply maponpaths_2. use (cartesian_factorisation_unique Hff). rewrite !assoc_disp_var. apply maponpaths. etrans. { apply maponpaths. apply (disp_nat_trans_ax_var (disp_nat_z_iso_to_trans_inv (α := nat_z_iso_id _) (η ,, is_z_iso_unit_over_id HL))). } refine (!_). etrans. { apply maponpaths. apply (disp_nat_trans_ax_var (disp_nat_z_iso_to_trans_inv (α := nat_z_iso_id _) (η ,, is_z_iso_unit_over_id HL))). } cbn. rewrite !mor_disp_transportf_prewhisker. apply maponpaths. rewrite !assoc_disp. apply maponpaths. apply maponpaths_2. refine (!(disp_functor_comp_var R _ _) @ _ @ disp_functor_comp_var R _ _). do 2 apply maponpaths. exact (pr2 φ₂ @ !(pr2 φ₁)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq