C : Type u₁
inst✝¹ : Category C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ (coreprF F).app X f = ((coreprF F).app (coreprX F) ≫ F.map f) (𝟙 (coreprX F))
C : Type u₁
inst✝¹ : Category C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ ((coreprW F).app X).hom f = F.map f (coreprx F)
change F.coreprF.app X f = (F.coreprF.app F.coreprX ≫ F.map f) (𝟙 F.coreprX)
C : Type u₁
inst✝¹ : Category C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ (coreprF F).app X f = ((coyoneda.obj (coreprX F).op).map f ≫ (coreprF F).app X) (𝟙 (coreprX F))
C : Type u₁
inst✝¹ : Category C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ (coreprF F).app X f = ((coreprF F).app (coreprX F) ≫ F.map f) (𝟙 (coreprX F))
rw [← F.coreprF.naturality]
C : Type u₁
inst✝¹ : Category C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ (coreprF F).app X f = (coreprF F).app X (𝟙 (coreprX F) ≫ f)
C : Type u₁
inst✝¹ : Category C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ (coreprF F).app X f = ((coyoneda.obj (coreprX F).op).map f ≫ (coreprF F).app X) (𝟙 (coreprX F))
dsimp
no goals
C : Type u₁
inst✝¹ : Category C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ (coreprF F).app X f = (coreprF F).app X (𝟙 (coreprX F) ≫ f)
simp