Representable functors in concrete categories

This file provides some API for the situation (F ⋙ forget D).RepresentableBy Y.

def CategoryTheory.Functor.RepresentableBy.homEquiv' {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor Cᵒᵖ D} {CD : D → Type u_3} {FD : D → D → Type u_4} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {Y : C} (α : (F.comp (forget D)).RepresentableBy Y) {X : C} : (X ⟶ Y) ≃ ToType (F.obj (Opposite.op X))

The natural bijection (X ⟶ Y) ≃ F.obj (op X).

Equations

• α.homEquiv' = α.homEquiv

theorem CategoryTheory.Functor.RepresentableBy.homEquiv'_comp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor Cᵒᵖ D} {CD : D → Type u_3} {FD : D → D → Type u_4} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] {Y : C} (α : (F.comp (forget D)).RepresentableBy Y) {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y) : α.homEquiv' (CategoryStruct.comp f g) = (ConcreteCategory.hom (F.map f.op)) (α.homEquiv' g)