In a brief note nlab mentions functors can be thought of maps between nerves. https://ncatlab.org/nlab/show/functor#definition I don't really get this definition.
I'm interested because I'm playing around with some foundational math and thought it might be easier to manipulate functors defined in terms of nerves instead of the usual way around. I also feel like the definition might work better with higher category theory.
In my little Coq library , ignoring some extraneous details, I define a functor the usual way basically something like:
Record functor (C D: Category) := {
fobj: object C -> object D ;
map: forall A B, hom A B -> hom (fobj A) (fobj B)
}.
And also satisfying the usual conditions.
My intuition is the definition in terms of nerves is that instead of record fields one would number off types of n-cells.
Definition functor A B := forall (n: ncell), cell n A -> cell n B.
Only having 0 and one cells. But I'm having trouble with the exact types.