proposition: Lemma triangle_2_from_1_for_equiv_over_id {C} {D D' : disp_cat C} (A : disp_adjunction_id_data D D') (E : form_equiv_over_id A) : triangle_1_statement_over_id A -> triangle_2_statement_over_id A.
proof: Proof. destruct A as [FF [GG [η ε]]]. destruct E as [Hη Hε]; cbn in Hη, Hε. unfold triangle_1_statement_over_id, triangle_2_statement_over_id; cbn. intros T1 x yy. etrans. apply id_left_disp_var. etrans. eapply transportf_bind. eapply cancel_postcomposition_disp. etrans. eapply transportf_transpose_right. apply @pathsinv0. refine (z_iso_disp_after_inv_mor _). refine (disp_functor_on_is_z_iso_disp GG _). apply Hε. eapply transportf_bind. eapply cancel_postcomposition_disp. etrans. apply id_right_disp_var. eapply transportf_bind. etrans. eapply cancel_precomposition_disp. eapply transportf_transpose_right. apply @pathsinv0. refine (z_iso_disp_after_inv_mor _). apply (Hη). eapply transportf_bind, assoc_disp. etrans. eapply transportf_bind. etrans. apply assoc_disp_var. eapply transportf_bind. etrans. apply assoc_disp_var. eapply transportf_bind. eapply cancel_precomposition_disp. etrans. eapply cancel_precomposition_disp. etrans. apply assoc_disp. eapply transportf_bind. etrans. eapply cancel_postcomposition_disp. exact (disp_nat_trans_ax η (♯ GG (ε x yy))). eapply transportf_bind. etrans. apply assoc_disp_var. eapply transportf_bind. eapply cancel_precomposition_disp. cbn. etrans. eapply transportf_transpose_right. apply @pathsinv0, (disp_functor_comp GG). eapply transportf_bind. etrans. apply maponpaths. apply (disp_nat_trans_ax ε). cbn. etrans. apply (disp_functor_transportf _ GG). eapply transportf_bind. apply (disp_functor_comp GG). eapply transportf_bind. etrans. apply assoc_disp. eapply transportf_bind. etrans. eapply cancel_postcomposition_disp. apply (disp_nat_trans_ax η (η x (GG x yy))). cbn. eapply transportf_bind. etrans. apply assoc_disp_var. eapply transportf_bind. eapply cancel_precomposition_disp. etrans. apply assoc_disp. eapply transportf_bind. etrans. eapply cancel_postcomposition_disp. etrans. eapply transportf_transpose_right. apply @pathsinv0, (disp_functor_comp GG). eapply transportf_bind. etrans. apply maponpaths, T1. etrans. apply (disp_functor_transportf _ GG). eapply transportf_bind. apply (disp_functor_id GG). eapply transportf_bind. apply id_left_disp. etrans. eapply transportf_bind. etrans. apply assoc_disp_var. eapply transportf_bind. etrans. eapply cancel_precomposition_disp. etrans. apply assoc_disp. eapply transportf_bind. etrans. eapply cancel_postcomposition_disp. exact (z_iso_disp_after_inv_mor _). eapply transportf_bind. apply id_left_disp. apply maponpaths. exact (z_iso_disp_after_inv_mor _). etrans. apply transport_f_f. unfold transportb. apply maponpaths_2, homset_property. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fiber