C : Type u₁
inst✝¹ : Category C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ (reprF F).app X f = ((reprF F).app (reprX F).op ≫ F.map f.op) (𝟙 (reprX F))
C : Type u₁
inst✝¹ : Category C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ ((reprW F).app X).hom f = F.map f.op (reprx F)
change F.reprF.app X f = (F.reprF.app (op F.reprX) ≫ F.map f.op) (𝟙 F.reprX)
C : Type u₁
inst✝¹ : Category C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ (reprF F).app X f = ((yoneda.obj (reprX F)).map f.op ≫ (reprF F).app X.unop.op) (𝟙 (reprX F))
C : Type u₁
inst✝¹ : Category C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ (reprF F).app X f = ((reprF F).app (reprX F).op ≫ F.map f.op) (𝟙 (reprX F))
rw [← F.reprF.naturality]
C : Type u₁
inst✝¹ : Category C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ (reprF F).app X f = (reprF F).app X (f ≫ 𝟙 (reprX F))
C : Type u₁
inst✝¹ : Category C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ (reprF F).app X f = ((yoneda.obj (reprX F)).map f.op ≫ (reprF F).app X.unop.op) (𝟙 (reprX F))
dsimp
no goals
C : Type u₁
inst✝¹ : Category C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ (reprF F).app X f = (reprF F).app X (f ≫ 𝟙 (reprX F))
simp