proposition: Lemma triangle_2_from_1_for_equiv_over {C C' : category} (E : adj_equiv C C') {D : disp_cat C} {D' : disp_cat C'} (AA : disp_adjunction_data E D D') (EE : form_equiv_over (E:=E) AA) : triangle_1_statement_over (A:=E) AA -> triangle_2_statement_over (A:=E) AA.
proof: Proof. destruct AA as [FF [GG [η ε]]]. destruct EE as [Hη Hε]; cbn in Hη, Hε. unfold triangle_1_statement_over, triangle_2_statement_over; 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 η (η _ (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. Time Qed. Lemma triangle_1_from_2_for_equiv_over {C C' : category} (E : adj_equiv C C') {D : disp_cat C} {D' : disp_cat C'} (AA : disp_adjunction_data E D D') (EE : form_equiv_over (E:=E) AA) : triangle_2_statement_over (A:=E) AA -> triangle_1_statement_over (A:=E) AA. Proof. Abort. Definition is_equiv_of_equiv_over {C C' : category} (E : adj_equiv C C') {D : disp_cat C} {D': disp_cat C'} (EE : equiv_over E D D') : is_equiv_over E (left_adj_over EE). Proof. use tpair. - apply (right_adjoint_of_disp_adjunction EE). - apply (axioms_of_equiv_over E EE). Defined.
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