case w.h.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E₁ E₂ : ℰ
g : E₁ ⟶ E₂
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k : c.pt ⟶ E₁
x : Cᵒᵖ
X : P.obj x
⊢ (↑(restrictYonedaHomEquiv A P E₂ t) (k ≫ g)).app x X =
    (↑(restrictYonedaHomEquiv A P E₁ t) k ≫ (restrictedYoneda A).map g).app x X
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E₁ E₂ : ℰ
g : E₁ ⟶ E₂
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k : c.pt ⟶ E₁
⊢ ↑(restrictYonedaHomEquiv A P E₂ t) (k ≫ g) = ↑(restrictYonedaHomEquiv A P E₁ t) k ≫ (restrictedYoneda A).map g
ext x X
no goals
case w.h.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type u₁
E₁ E₂ : ℰ
g : E₁ ⟶ E₂
c : Cocone ((CategoryOfElements.π P).leftOp ⋙ A)
t : IsColimit c
k : c.pt ⟶ E₁
x : Cᵒᵖ
X : P.obj x
⊢ (↑(restrictYonedaHomEquiv A P E₂ t) (k ≫ g)).app x X =
    (↑(restrictYonedaHomEquiv A P E₁ t) k ≫ (restrictedYoneda A).map g).app x X
apply (assoc _ _ _).symm