Proposition is_left_adjoint_nat_z_iso_triangle_1 : triangle_1_statement (L₂ ,, R ,, η' ,, ε'). Proof. intros x ; cbn -[η ε]. etrans. { rewrite !assoc. apply maponpaths_2. exact (nat_trans_ax (nat_z_iso_inv τ) _ _ (η x · #R(τ x))). } rewrite functor_comp. rewrite !assoc'. etrans. { do 2 apply maponpaths. apply (nat_trans_ax ε). } etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (pr122 HL₁). } rewrite id_left. exact (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso τ x)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.whiskering.