![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
anhinga_draftsI am continuing the last three postings in this blog, and jumping to Section 5.3 of Vickers' text.
One can take a category and interpret it as a predicate theory. All objects A are interpreted as sorts, XA, and all arrows f : A → B are interpreted as functional symbols, uf : XA → XB.
Then for every object A one imposes an axiom (∀x:XA) uidA (x) = x.
And for every pair of morphisms f : A → B, g : B → C one considers the morphism h = g o f and imposes an axiom (∀x:XA) ug (uf (x)) = uh (x).
One often imposes additional axioms as well. Of course, this is a lot of sorts, functional symbols, and axioms. If one at least wants them to form sets rather than proper classes, one has to start with a small category.
Also we can't assume that objects are sets which have elements, so what would (∀x:XA) even mean? One can think about this purely formally (until one starts to consider models of the theories), or one can recall from a first post in this series than a generalized point of A is simply a morphism x to A, then f (x) should be thought of as f o x, and one can think about quantifiers ranging over these generalized points.
One can take a category and interpret it as a predicate theory. All objects A are interpreted as sorts, XA, and all arrows f : A → B are interpreted as functional symbols, uf : XA → XB.
Then for every object A one imposes an axiom (∀x:XA) uidA (x) = x.
And for every pair of morphisms f : A → B, g : B → C one considers the morphism h = g o f and imposes an axiom (∀x:XA) ug (uf (x)) = uh (x).
One often imposes additional axioms as well. Of course, this is a lot of sorts, functional symbols, and axioms. If one at least wants them to form sets rather than proper classes, one has to start with a small category.
Also we can't assume that objects are sets which have elements, so what would (∀x:XA) even mean? One can think about this purely formally (until one starts to consider models of the theories), or one can recall from a first post in this series than a generalized point of A is simply a morphism x to A, then f (x) should be thought of as f o x, and one can think about quantifiers ranging over these generalized points.
