Lemma z_iso_disp_precomp {C : category} {D : disp_cat C} {x y : C} (f : z_iso x y) {xx : D x} {yy} (ff : z_iso_disp f xx yy) : forall (y' : C) (f' : y --> y') (yy' : D y'), isweq (fun ff' : yy -->[ f' ] yy' => pr1 ff ;; ff'). Proof. intros y' f' yy'. use isweq_iso. + intro X. set (XR := (pr1 (pr2 ff)) ;; X). set (XR' := transportf _ (assoc _ _ _ ) XR). set (XRRT := transportf _ (maponpaths (λ xyz, xyz · f') (z_iso_after_z_iso_inv f)) XR'). set (XRRT' := transportf _ (id_left _ ) XRRT). apply XRRT'. + intros. simpl. etrans. apply transport_f_f. etrans. apply transport_f_f. etrans. apply maponpaths. apply assoc_disp. etrans. apply transport_f_f. etrans. apply maponpaths. apply maponpaths_2. apply (pr2 (pr2 ff)). etrans. apply maponpaths. apply mor_disp_transportf_postwhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply id_left_disp. etrans. apply transport_f_f. apply transportf_comp_lemma_hset. apply C. apply idpath. + intros; simpl. etrans. apply maponpaths. apply transport_f_f. etrans. apply mor_disp_transportf_prewhisker. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply assoc_disp. etrans. apply transport_f_f. etrans. apply maponpaths. apply maponpaths_2. assert (XR := pr2 (pr2 (pr2 ff))). simpl in XR. apply XR. etrans. apply maponpaths. apply mor_disp_transportf_postwhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply id_left_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.