proposition: Proposition faithful_duality_transpose (x y : B) : faithful (duality_transpose_functor x y).
proof: 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.
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