Lemma inv_ax : disp_nat_trans_axioms (λ (x : C) (xx : D' x), @inv_mor_disp_from_iso _ _ _ _ (identity_iso _ ) _ _ _ (Ha x xx)). *) Local Lemma inv_ax : @disp_nat_trans_axioms C C (functor_identity_data C) (functor_identity_data C) (@nat_trans_id C C (functor_identity_data C)) D' D GG FF (λ (x : C) (xx : D' x), @inv_mor_disp_from_z_iso C D ((functor_identity C) x) ((functor_identity C) x) (@identity_z_iso C ((functor_identity C) x)) (FF x xx) (GG x xx) (alpha x xx) (Ha x xx)). Proof. intros x y f xx yy ff. apply pathsinv0. apply transportf_pathsinv0. apply pathsinv0. set (XR := @z_iso_disp_precomp). specialize (XR _ _ _ _ (identity_z_iso _ ) _ _ (alpha x xx ,, Ha x xx) ). match goal with |[|- ?EE = _ ] => set (E := EE) end. cbn in E. specialize (XR _ (identity x · f) (FF y yy)). set (R := make_weq _ XR). apply (invmaponpathsweq R). unfold R. unfold E. cbn. etrans. apply assoc_disp. etrans. apply maponpaths. apply maponpaths_2. apply (inv_mor_after_z_iso_disp (Ha x xx)). 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 pathsinv0. etrans. apply mor_disp_transportf_prewhisker. etrans. apply maponpaths. apply assoc_disp. etrans. apply transport_f_f. etrans. apply maponpaths. apply maponpaths_2. apply (disp_nat_trans_ax_var alpha). 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. apply (inv_mor_after_z_iso_disp (Ha _ _ )). 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 maponpaths_2. apply homset_property. Qed.
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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. 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.Fiber.