Proposition faithful_duality_transpose (x y : B) : faithful (duality_transpose_functor x y). Proof. intros f g τ ; cbn in f, g, τ. use invproofirrelevance. intros φ₁ φ₂. induction φ₁ as [ φ₁ p₁ ]. induction φ₂ as [ φ₂ p₂ ]. cbn in φ₁, φ₂, p₁, p₂. unfold duality_transpose_cell in p₁, p₂. use subtypePath. { intro. apply cellset_property. } cbn. use lwhisker_id_inj. use (vcomp_rcancel (invertible_modcomponent_of (unit_unit_inv_of_duality HL) x ▹ _)). { is_iso. apply property_from_invertible_2cell. } rewrite <- !vcomp_whisker. apply maponpaths. use (vcomp_rcancel (rassociator _ _ _)). { is_iso. } etrans. { refine (!_). apply lwhisker_lwhisker_rassociator. } refine (!_). etrans. { refine (!_). apply lwhisker_lwhisker_rassociator. } refine (!_). do 2 apply maponpaths. use (vcomp_rcancel (psnaturality_of ηinv f)). { apply property_from_invertible_2cell. } refine (psnaturality_natural ηinv _ _ _ _ φ₁ @ _). refine (_ @ !(psnaturality_natural ηinv _ _ _ _ φ₂)). apply maponpaths. cbn. use (vcomp_rcancel ((#L(#L f)) ◃ triangle_data_of_duality_inv HL y)). { is_iso. apply property_from_invertible_2cell. } rewrite !vcomp_whisker. apply maponpaths. use (vcomp_rcancel (psfunctor_comp L _ _)). { apply property_from_invertible_2cell. } refine (!(psfunctor_rwhisker L _ _) @ _ @ psfunctor_rwhisker L _ _). apply maponpaths. exact (maponpaths (λ z, ##R z) (p₁ @ !p₂)). 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.