Proposition duality_involution_inv_of_2cell_eq {x y : B} {f g : x --> y} (τ : # L f ==> # L g) : ##L (duality_involution_inv_of_2cell τ) = τ. Proof. unfold duality_involution_inv_of_2cell. rewrite !vassocl. refine (psfunctor_vcomp L _ _ @ _). use (vcomp_rcancel (## L(duality_involution_local_equivalence_inv2cell g))). { use (psfunctor_is_iso L (make_invertible_2cell _)). use to_op2_is_invertible_2cell. apply duality_involution_local_equivalence_inv2cell. } rewrite !vassocl. rewrite <- psfunctor_vcomp. etrans. { do 2 apply maponpaths. apply (vcomp_rinv (duality_involution_local_equivalence_inv2cell g)). } etrans. { apply maponpaths. apply (psfunctor_id2 L). } rewrite id2_right. unfold duality_involution_local_equivalence_inv2cell. simpl. refine (psfunctor_vcomp L _ _ @ _). etrans. { apply maponpaths_2. refine (psfunctor_vcomp L _ _ @ _). apply maponpaths_2. refine (psfunctor_vcomp L _ _ @ _). apply maponpaths_2. apply (psfunctor_vcomp L). } refine (!_). etrans. { apply maponpaths. refine (psfunctor_vcomp L _ _ @ _). apply maponpaths_2. refine (psfunctor_vcomp L _ _ @ _). apply maponpaths_2. apply (psfunctor_vcomp L). } rewrite !vassocl. etrans. { apply maponpaths. apply maponpaths_2. exact (psfunctor_rinvunitor L g). } refine (!_). etrans. { apply maponpaths_2. exact (psfunctor_rinvunitor L f). } rewrite !vassocr. refine (!_). etrans. { do 5 apply maponpaths_2. rewrite rinvunitor_natural. rewrite <- rwhisker_hcomp. apply idpath. } rewrite !vassocl. apply maponpaths. etrans. { rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. do 2 apply maponpaths_2. apply (psfunctor_lwhisker L). } etrans. { rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } refine (!_). etrans. { rewrite !vassocr. do 3 apply maponpaths_2. apply (psfunctor_lwhisker L). } rewrite !vassocl. apply maponpaths. use (vcomp_lcancel (#L f ◃ psfunctor_comp L (η y) (ηinv y))). { is_iso. apply property_from_invertible_2cell. } etrans. { rewrite !vassocr. do 2 apply maponpaths_2. exact (psfunctor_lassociator L f (η y) (ηinv y)). } rewrite !vassocl. etrans. { do 2 apply maponpaths. rewrite !vassocr. apply maponpaths_2. apply (psfunctor_rwhisker L). } rewrite !vassocl. etrans. { do 3 apply maponpaths. apply (psfunctor_rwhisker L). } refine (!_). etrans. { rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. apply maponpaths_2. exact (psfunctor_lassociator L g (η y) (ηinv y)). } rewrite !vassocr. rewrite <- rwhisker_rwhisker. rewrite !vassocl. apply maponpaths. etrans. { do 2 apply maponpaths. apply (psfunctor_rwhisker L). } rewrite !vassocr. apply maponpaths_2. rewrite !rwhisker_vcomp. apply maponpaths. rewrite !vassocl. use (vcomp_lcancel (_ ◃ triangle_data_of_duality HL y)). { is_iso. apply property_from_invertible_2cell. } rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. use (vcomp_lcancel (psnaturality_of η (# L f))). { apply property_from_invertible_2cell. } rewrite !vassocr. etrans. { do 3 apply maponpaths_2. exact (!(psnaturality_natural η _ _ _ _ τ)). } cbn -[psfunctor_comp]. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. refine (!_). apply (duality_to_triangle_law HL). } etrans. { rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. apply idpath. } refine (!_). etrans. { rewrite !vassocr. refine (!_). apply maponpaths_2. apply (duality_to_triangle_law HL). } rewrite !vassocl. apply maponpaths. apply (psfunctor_lwhisker L). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. 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.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Properties.ContainsAdjEquiv. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Properties. 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.PseudoFunctors.Examples.OpFunctor. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Transformations.Examples.Associativity. Require Import UniMath.Bicategories.Transformations.Examples.Unitality. Require Import UniMath.Bicategories.Transformations.Examples.Whiskering. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.OtherStructure.DualityInvolution.