Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
started something at topos of types.
That name seems a little unfortunate. It sounds to me like a topos built from type theory as a syntactic category. Where are the types in this construction? Also, what is a filter on a category?
Yeah, I don’t know. This terminology was invented by Makkai, and logicians around me stick to it.
Could you maybe add a warning to the entry (I could add one, too, but I expect you can add a more informative one).
The “category of filters” of a category $C$ that Makkai uses has as objects pairs consisting of an object $X$ of $C$ and a filter on $Sub_C(X)$.
Ok, I added a note, with a guess that it is a reference to “types” as used in model theory.
1 to 4 of 4