Lemma z_iso_disp_postcomp {C : category} {D : disp_cat C} {x y : C} (i : z_iso x y) {xx : D x} {yy} (ii : z_iso_disp i xx yy) : forall (x' : C) (f' : x' --> x) (xx' : D x'), isweq (fun ff : xx' -->[ f' ] xx => ff ;; ii)%mor_disp. Proof. intros y' f' yy'. use isweq_iso. + intro X. set (XR := X ;; (pr1 (pr2 ii))). set (XR' := transportf (λ x, _ -->[ x ] _) (!assoc _ _ _ ) XR). set (XRRT := transportf (λ x, _ -->[ x ] _ ) (maponpaths (λ xyz, _ · xyz) (z_iso_inv_after_z_iso _ )) XR'). set (XRRT' := transportf _ (id_right _ ) XRRT). apply XRRT'. + intros. simpl. etrans. apply transport_f_f. etrans. apply transport_f_f. etrans. apply maponpaths. apply assoc_disp_var. etrans. apply transport_f_f. etrans. apply maponpaths. apply maponpaths. apply (pr2 (pr2 (pr2 ii))). etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply id_right_disp. etrans. apply transport_f_f. apply transportf_comp_lemma_hset. apply C. apply idpath. + intros; simpl. etrans. apply maponpaths_2. apply transport_f_f. etrans. apply mor_disp_transportf_postwhisker. etrans. apply maponpaths. apply mor_disp_transportf_postwhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply assoc_disp_var. etrans. apply transport_f_f. etrans. apply maponpaths. apply maponpaths. assert (XR := pr1 (pr2 (pr2 ii))). simpl in XR. apply XR. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply id_right_disp. etrans. apply transport_f_f. apply transportf_comp_lemma_hset. apply C. apply idpath. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core.