Proposition comp_is_left_adjoint_triangle_1 : triangle_1_statement (L₁ ∙ L₂ ,, R' ,, η' ,, ε'). Proof. intro x. cbn -[η₁ η₂ ε₁ ε₂]. rewrite !assoc. rewrite <- functor_comp. etrans. { apply maponpaths_2. apply maponpaths. rewrite functor_comp. rewrite !assoc'. apply maponpaths. apply (nat_trans_ax ε₁). } cbn -[η₁ η₂ ε₁ ε₂]. rewrite !assoc. etrans. { apply maponpaths_2. apply maponpaths. apply maponpaths_2. apply (pr122 HL₁). } rewrite id_left. apply (pr122 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.