Lemma is_modification_duality_triangle_lem {x y : B} (f : x --> y) : ((((rassociator (id₁ (L x)) (η (L x)) (#L (#L (#L f))) • (id₁ (L x) ◃ psnaturality_of η (# L f))) • lassociator (id₁ (L x)) (#L f) (η (L y))) • ((lunitor (#L f) • rinvunitor (#L f)) ▹ η (L y))) • rassociator ((pr211 L) x y f) (id₁ (L y)) (η (L y))) • (#L f ◃ (lunitor (unit_of_duality d (L y)) • (t y • (linvunitor (#L (η y)) • rinvunitor (id₁ (L y) · #L(η y)))))) = ((lunitor (η (L x)) • (t x • (linvunitor (#L (η x)) • rinvunitor (id₁ (L x) · # L (η x))))) ▹ #L (#L (#L f))) • ((((rassociator (id₁ (L x) · #L (η x)) (id₁ (L (L (L x)))) (#L (#L (#L f))) • (id₁ (L x) · # L(η x) ◃ (lunitor (#L (#L (#L f))) • rinvunitor (#L (#L (#L f)))))) • lassociator (id₁ (L x) · # L (η x)) (#L (#L (#L f))) (id₁ (L (L (L y))))) • (((((rassociator (id₁ (L x)) (#L (η x)) (#L (#L (#L f))) • (id₁ (L x) ◃ ((psfunctor_comp L (η x) (#L (#L f)) • ##L ((psnaturality_of η f) ^-1)) • (psfunctor_comp L f (η y)) ^-1))) • lassociator (id₁ (L x)) (#L f) (#L (η y))) • ((lunitor (#L f) • rinvunitor (#L f)) ▹ #L (η y))) • rassociator (#L f) (id₁ (L y)) (#L (η y))) ▹ id₁ (L (L (L y))))) • rassociator (#L f) (id₁ (L y) · # L (η y)) (id₁ (L (L (L y))))). Proof. rewrite !vassocl. etrans. { rewrite <- rwhisker_vcomp. rewrite !vassocr. do 3 apply maponpaths_2. rewrite !vassocl. rewrite lunitor_triangle. rewrite vcomp_lunitor. apply idpath. } etrans. { rewrite !vassocl. do 3 apply maponpaths. rewrite !vassocr. rewrite rwhisker_hcomp. rewrite <- triangle_r_inv. rewrite <- lwhisker_hcomp. rewrite lwhisker_vcomp. rewrite !vassocr. rewrite linvunitor_lunitor. rewrite id2_left. apply idpath. } etrans. { rewrite !vassocr. rewrite <- lunitor_triangle. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } refine (!_). etrans. { rewrite <- rwhisker_vcomp. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { rewrite <- rwhisker_vcomp. rewrite !vassocl. apply maponpaths. rewrite <- !rwhisker_vcomp. rewrite <- !lwhisker_vcomp. rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite lunitor_lwhisker. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite rinvunitor_runitor. rewrite id2_rwhisker. rewrite id2_left. rewrite rinvunitor_triangle. do 6 apply maponpaths_2. rewrite rwhisker_hcomp. rewrite <- rinvunitor_natural. apply idpath. } etrans. { rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite !rwhisker_vcomp. rewrite rwhisker_hcomp. rewrite <- rinvunitor_natural. rewrite !vassocl. apply idpath. } rewrite !vassocl. rewrite <- left_unit_inv_assoc. apply idpath. } rewrite !vassocr. rewrite <- lwhisker_vcomp. rewrite !vassocr. apply maponpaths_2. etrans. { rewrite !vassocl. do 8 apply maponpaths. rewrite rwhisker_hcomp. rewrite <- triangle_r_inv. rewrite <- lwhisker_hcomp. apply idpath. } rewrite !vassocr. rewrite <- lwhisker_vcomp. rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. etrans. { rewrite lunitor_triangle. do 3 apply maponpaths. rewrite !vassocr. rewrite !lwhisker_vcomp. rewrite vcomp_lunitor. rewrite !vassocl. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. do 3 apply maponpaths_2. rewrite !vassocl. rewrite <- lunitor_triangle. etrans. { apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. apply id2_left. } rewrite rwhisker_vcomp. rewrite linvunitor_lunitor. apply id2_rwhisker. } rewrite id2_left. rewrite !vassocr. use vcomp_move_R_Mp ; [ is_iso | ]. use vcomp_move_R_Mp. { use (psfunctor_is_iso L (make_invertible_2cell _)). use to_op2_is_invertible_2cell. apply (inv_of_invertible_2cell (psnaturality_of (unit_of_duality d) f)). } exact (duality_to_triangle_law f). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Op2OfPseudoFunctor. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Transformations.Examples.Unitality. Require Import UniMath.Bicategories.Transformations.Examples.Associativity. Require Import UniMath.Bicategories.Transformations.Examples.Whiskering. Require Import UniMath.Bicategories.Modifications.Modification. Section CounitFromDualityInvolution. End CounitFromDualityInvolution.