proposition: Lemma yoneda_unit_component_mod_component_is_nat_trans (η : pstrans (representable B_is_univalent_2_1 X) F) (Z : op1_bicat B) (f₁ f₂ : B ⟦ Z , X ⟧) (α : f₁ ==> f₂) : # (η Z : _ ⟶ _) α · yoneda_unit_component_mod_component_nat_component η Z f₂ = (yoneda_unit_component_mod_component_nat_component η Z f₁) · (## F α : _ ⟹ _) ((η X : _ ⟶ _) (id₁ X)).
proof: Proof. cbn ; unfold yoneda_unit_component_mod_component_nat_component. pose (nat_trans_eq_pointwise (psnaturality_inv_natural η _ _ _ _ α) (id₁ X)). cbn in p. refine (!_). etrans. { refine (!(assoc _ _ _) @ _). apply maponpaths. exact (nat_trans_eq_pointwise (psnaturality_inv_natural η _ _ _ _ α) (id₁ X)). } cbn. refine (assoc _ _ _ @ _ @ !(assoc _ _ _)). apply maponpaths_2. refine (!(functor_comp _ _ _) @ _ @ functor_comp _ _ _). apply maponpaths. refine (!_). refine (rinvunitor_natural _ @ _). apply maponpaths. refine (!_). apply rwhisker_hcomp. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Examples.OpMorBicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Morphisms.Properties UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.UnivalenceOp UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Properties UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.Modifications.Modification UniMath.Bicategories.PseudoFunctors.Yoneda UniMath.Bicategories.PseudoFunctors.Representable UniMath.Bicategories.Core.Examples.Image UniMath.Bicategories.PseudoFunctors.Examples.CorestrictImage