the problem is not to find an internal language, it is to find a sharp one
The problem is not to find and internal language but to find a ‘sharp’ one. While it is relatively easy to find construct a ‘dull’ free structure by adding all of its constructing pieces as generators and then quotienting by all of its axioms, this is rarely the theory we want to use.
Instead, we want to find an internal language with as few primitives as possible (so that most constructions are derived from a core) and with as few ad-hoc quotienting as possible (so that most of the bureaucracy of dealing with the structure is invisible, trivial during computations).
References.
Tags: opinion,
category theory,
categorical logic.
Back:
internal language.