Category Isotypes

The isotypes project dates back to 2011. I was wondering at that time how to generate a panoply of math/logic types whose models are associated with categories that can in turn be employed to construct the types. In the meantime some fairly simple ideas emerged (wlog types) that required a more explicit technical specification or formulation ‐ category isotypes ‐ in order to proceed with the original naive motivations. In particular, (1) the slides propose a specification for type universes associated with categories and (2) exploit a kind of "univalence", called isovalence for isotype theory, which is inherent for isotypes associated within a given category universe.

The (picture language) isotype shown under the page title above suggests a very relevant metaphor regarding isotypes theory: The diagram logic of categories gives us a picture of the structures associated with types of things associated with and constructed from abstract categories as category isotypes.

I hope to formulate isotype theories in Autolog (via parametric logic of the diagram) and automate some isotype theorems using autolog tools. Logical expressions specifying category diagrams were a big motivation (~2017) in the design of the AUTOLOG language (parametric functors) and in the design of active rules and equality modulators for the Autolog system (pending).

A provisional outline of isotype ideas is presented in the following slides. The examples are currently restricted to categories determined by varieties of algebras (and called varietal isotypes).

HTML SLIDES
In the presentation window, press the ? key to see keyboard viewing shortcuts.

(pdf version: pdf slides)