Definition z_iso_disp_comp {C : category} {D : disp_cat C} {x y z : C} {f : z_iso x y} {g : z_iso y z} {xx : D x} {yy : D y} {zz : D z} (ff : z_iso_disp f xx yy) (gg : z_iso_disp g yy zz) : z_iso_disp (z_iso_comp f g) xx zz. Proof. use tpair. - apply (ff ;; gg). - use tpair. + apply (transportb (mor_disp zz xx) (maponpaths pr1 (z_iso_inv_of_z_iso_comp _ _ _ f g))). cbn. apply (inv_mor_disp_from_z_iso gg ;; inv_mor_disp_from_z_iso ff). + split. * etrans. apply mor_disp_transportf_postwhisker. etrans. apply maponpaths. apply assoc_disp_var. etrans. apply maponpaths, maponpaths, maponpaths. apply assoc_disp. etrans. apply maponpaths, maponpaths, maponpaths, maponpaths. eapply (maponpaths (λ x, x ;; gg)). apply z_iso_disp_after_inv_mor. etrans. apply transport_f_f. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. etrans. apply maponpaths, maponpaths. apply mor_disp_transportf_postwhisker. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. etrans. apply maponpaths, maponpaths. apply id_left_disp. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply z_iso_disp_after_inv_mor. etrans. apply transport_f_f. apply transportf_comp_lemma; apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. * cbn. simpl. etrans. apply assoc_disp_var. etrans. apply maponpaths, maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply maponpaths, maponpaths, maponpaths. apply assoc_disp. etrans. apply maponpaths, maponpaths, maponpaths, maponpaths. eapply (maponpaths (λ x, x ;; inv_mor_disp_from_z_iso ff )). apply inv_mor_after_z_iso_disp. etrans. apply maponpaths, maponpaths, maponpaths, maponpaths. apply mor_disp_transportf_postwhisker. etrans. apply maponpaths, maponpaths, maponpaths, maponpaths, maponpaths. apply id_left_disp. etrans. apply maponpaths, maponpaths. apply transport_f_f. etrans. apply maponpaths, maponpaths. apply transport_f_f. etrans. apply maponpaths, maponpaths. apply transport_f_f. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply inv_mor_after_z_iso_disp. etrans. apply transport_f_f. apply transportf_comp_lemma; apply transportf_comp_lemma_hset; try apply homset_property; 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.