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. 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.
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.