Proposition comp_is_left_adjoint_triangle_2 : triangle_2_statement (L₁ ∙ L₂ ,, R' ,, η' ,, ε'). Proof. intro x. cbn -[η₁ η₂ ε₁ ε₂]. rewrite !assoc'. rewrite <- functor_comp. etrans. { do 2 apply maponpaths. rewrite functor_comp. rewrite !assoc. apply maponpaths_2. refine (!_). apply (nat_trans_ax η₂). } cbn -[η₁ η₂ ε₁ ε₂]. rewrite !assoc'. etrans. { do 3 apply maponpaths. apply (pr222 HL₂). } rewrite id_right. 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.