proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.UnivalenceOp UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Morphisms.FullyFaithful UniMath.Bicategories.Morphisms.Properties.ContainsAdjEquiv UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.Examples.OpCellBicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Properties UniMath.Bicategories.PseudoFunctors.Examples.Identity UniMath.Bicategories.PseudoFunctors.Examples.Composition UniMath.Bicategories.PseudoFunctors.Examples.Op2OfPseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.OpFunctor UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.Transformations.Examples.Associativity UniMath.Bicategories.Transformations.Examples.Unitality UniMath.Bicategories.Transformations.Examples.Whiskering UniMath.Bicategories.Modifications.Modification UniMath.Bicategories.OtherStructure.DualityInvolution