Does anyone know if there is there a name for the idea that new concepts (such as negative numbers, complex numbers or type constructors in a type system) are only ever introduced into a preexisting "system" so that they can be eliminated later, after helping make some progress?
-
Could the general case be described as two categories linked by an adjunction? ie with the Linear/Non-Linear adjunction, you can introduce terms of one category in the other, so long as you can lawfully "eliminate" them laterhttps://gyazo.com/d83dd0addb3f7f8a7a8a4e926f12f92c …
I was thinking of something more general (and basically more vague and philosophical), but in a CT context, this is spot-on.
