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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. 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.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.Yoneda. Require Import UniMath.Bicategories.PseudoFunctors.Representable. Require Import UniMath.Bicategories.Core.Examples.Image. Require Import UniMath.Bicategories.PseudoFunctors.Examples.CorestrictImage.