functor.eval

Stream: Is there code for X?

[Johan Commelin]

Given two categories $C$ and $D$, and an object $X \in C$, there's a natural functor $\mathrm{Func}(C,D) \to D$ by evaluating functors on $X$. Do we have this functor in mathlib already?

[Mario Carneiro]

that looks like swap(eval) or so

[Johan Commelin]

But there doesn't seem to be a functor.eval in mathlib. So I guess we just don't have it.

[Mario Carneiro]

import category_theory.functor_category

open category_theory

universes v₁ v₂ u₁ u₂

variables (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D]

def eval (A : C) : (C ⥤ D) ⥤ D :=
(functor.flip (functor.id _)).obj A

[Johan Commelin]

Ooh, nice!

[Scott Morrison]

There is src#category_theory.evaluation, very confusingly inside category_theory/prod.lean.

[Johan Commelin]

category_theory/products/basic.lean :wink: