restrictedULiftYonedaHomEquiv'_symm_app_naturality_left

English

Naturality holds for the symmetry of restrictedULiftYonedaHomEquiv' on the left.

Русский

Естественность сохраняется для симметрии restrictedULiftYonedaHomEquiv' слева.

LaTeX

$$$\text{restrictedULiftYonedaHomEquiv}'\ A\ P\ E\;\text{symm}_{app}\;\text{(f)} = \text{(symm app)}\;\text{(f)}$$$

Lean4

@[reassoc]
theorem restrictedULiftYonedaHomEquiv'_symm_app_naturality_left {P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)} (f : P ⟶ Q) (E : ℰ)
    (g : Q ⟶ (restrictedULiftYoneda.{max w v₁} A).obj E) (p : CostructuredArrow uliftYoneda.{max w v₂} P) :
    ((restrictedULiftYonedaHomEquiv' A P E).symm (f ≫ g)).app p =
      ((restrictedULiftYonedaHomEquiv' A Q E).symm g).app ((CostructuredArrow.map f).obj p) :=
  rfl

Похожие утверждения