Lemma triangle_2_from_1 {C D} (A : adjunction_data C D) (E : forms_equivalence A) : triangle_1_statement A -> triangle_2_statement A. Proof. destruct A as [F [G [η ε]]]. destruct E as [Hη Hε]; cbn in Hη, Hε. unfold triangle_1_statement, triangle_2_statement; cbn. intros T1 x. assert (etaH := nat_trans_ax η); cbn in etaH. assert (epsH := nat_trans_ax ε); cbn in epsH. apply (invmaponpathsweq (make_weq _ (z_iso_comp_left_isweq (_,,Hη _ ) _ ))). cbn. apply pathsinv0. etrans. apply id_left. etrans. apply (! id_right _ ). apply pathsinv0. apply (z_iso_inv_to_left _ _ _ (_,,Hη _ )). apply (invmaponpathsweq (make_weq _ (z_iso_comp_left_isweq (functor_on_z_iso G (_,,Hε _ )) _ ))). cbn. set (XR' := functor_on_z_iso G (_,,Hε x)). cbn in XR'. apply pathsinv0. etrans. apply id_left. etrans. apply (! id_right _ ). apply pathsinv0. apply (z_iso_inv_to_left _ _ _ XR'). unfold XR'; clear XR'. repeat rewrite assoc. set (i := inv_from_z_iso (functor_on_z_iso G (ε x ,, Hε x))). set (i' := inv_from_z_iso (η (G x) ,, Hη (G x))). etrans. apply cancel_postcomposition. repeat rewrite <- assoc. rewrite etaH. apply idpath. etrans. repeat rewrite <- assoc. rewrite <- functor_comp. rewrite (epsH). rewrite functor_comp. apply idpath. etrans. apply maponpaths. apply maponpaths. repeat rewrite assoc. rewrite etaH. apply cancel_postcomposition. rewrite <- assoc. rewrite <- functor_comp. rewrite T1. rewrite functor_id. apply id_right. etrans. apply maponpaths. rewrite assoc. apply cancel_postcomposition. use (z_iso_after_z_iso_inv (_ ,, Hη _ )). rewrite id_left. apply (z_iso_after_z_iso_inv ). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core.