# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeMar 1st 2012

started something at topos of types.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeMar 1st 2012

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?

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeMar 1st 2012

Yeah, I don’t know. This terminology was invented by Makkai, and logicians around me stick to it.

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)$.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeMar 1st 2012

Ok, I added a note, with a guess that it is a reference to “types” as used in model theory.