Lemma inv_triangle_1_statement_over_id : triangle_1_statement_over_id inv_adjunction_data. Proof. intros x xx. cbn. set (XR:= @z_iso_disp_precomp). set (Gepsxxx := (♯ GG (ε x xx))). set (RG := @disp_functor_on_is_z_iso_disp _ _ (functor_identity C)). specialize (RG _ _ GG). specialize (RG _ _ _ _ (identity_z_iso _ ) (ε x xx)). specialize (RG (is_z_iso_counit_over_id (pr2 isEquiv) x xx)). transparent assert (Ge : (z_iso_disp (identity_z_iso x) (GG _ (FF _ (GG _ xx))) (GG _ xx))). { apply (make_z_iso_disp (f:=identity_z_iso _ ) Gepsxxx). eapply is_z_iso_disp_independent_of_is_z_iso. apply RG. } match goal with |[|- ?EE = _ ] => set (E := EE) end. cbn in E. specialize (XR _ _ _ _ _ _ _ Ge). specialize (XR _ (identity x · identity x ) (GG x xx)). apply (invmaponpathsweq (make_weq _ XR)). unfold E; clear E. cbn. clear RG XR Ge. unfold Gepsxxx. etrans. apply assoc_disp. etrans. apply maponpaths. apply maponpaths_2. eapply pathsinv0. apply (disp_functor_comp_var GG). etrans. apply maponpaths. apply mor_disp_transportf_postwhisker. etrans. apply transport_f_f. etrans. apply maponpaths. apply maponpaths_2. apply maponpaths. apply (inv_mor_after_z_iso_disp (is_z_iso_counit_over_id (pr2 isEquiv) x xx)). etrans. apply maponpaths. apply maponpaths_2. apply (disp_functor_transportf _ GG). etrans. apply maponpaths. apply mor_disp_transportf_postwhisker. etrans. apply ( transport_f_f _ _ _ _ ). etrans. apply maponpaths. apply maponpaths_2. apply (disp_functor_id GG). 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. match goal with |[|- transportf _ ?EE _ = _ ] => generalize EE end. intro EE. set (XR:= @z_iso_disp_precomp). set (etaGxxx := η _ (GG x xx)). transparent assert (Ge : (z_iso_disp (identity_z_iso x) (GG _ xx) (GG _ (FF _ (GG _ xx))) )). { apply (make_z_iso_disp (f:=identity_z_iso _ ) etaGxxx). eapply is_z_iso_disp_independent_of_is_z_iso. apply (is_z_iso_unit_over_id (pr2 isEquiv) ). } match goal with |[|- ?EE = _ ] => set (E := EE) end. cbn in E. specialize (XR _ _ _ _ _ _ _ Ge). specialize (XR _ (identity x · (identity x · identity x) ) (GG x xx)). apply (invmaponpathsweq (make_weq _ XR)). cbn. unfold etaGxxx. unfold E. clear E. clear XR Ge etaGxxx. clear Gepsxxx. etrans. apply mor_disp_transportf_prewhisker. etrans. apply maponpaths. apply (inv_mor_after_z_iso_disp (is_z_iso_unit_over_id (pr2 isEquiv) x _ )). etrans. apply transport_f_f. apply pathsinv0. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply mor_disp_transportf_prewhisker. etrans. apply maponpaths. apply maponpaths. apply id_right_disp. etrans. apply maponpaths. apply mor_disp_transportf_prewhisker. etrans. apply transport_f_f. set (XR := triangle_2_over_id isEquiv). unfold triangle_1_statement_over_id in XR. cbn in XR. etrans. apply maponpaths. apply XR. 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.