Proposition is_left_adjoint_nat_z_iso_triangle_2 : triangle_2_statement (L₂ ,, R ,, η' ,, ε'). Proof. intros x ; cbn. rewrite !assoc'. rewrite <- functor_comp. rewrite assoc. etrans. { do 2 apply maponpaths. apply maponpaths_2. exact (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso τ (R x))). } rewrite id_left. apply (pr222 HL₁). 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.