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.
added this remark on terminology:
The type-theory-literature traditionally refers to such categories generically as display map/fibration categories with such-and-such types, eg.
The definitions in this section are relatively standard in the literature. A display map category which models -types coincides with Joyal’s notion of clan, and a display map category which models -types and -types coincides with his notion of -clan.
added the remark that the definition is due to:
I think we should merge the entry clan into display map.
I am all for finding better – namely more evocative – words for existing definitions (eg. I have sympathy for logos) but I admit with “clan” I am at a loss.
I think we should merge the entry clan into display map.
I agree. The terminology “clan” is less descriptive than existing terminology, and doesn’t appear evocative of its nature.
Is there a more descriptive name for “tribe” as well? You see at least how Joyal was looking to link the two – clan/tribe.
Is there a more descriptive name for “tribe” as well? You see at least how Joyal was looking to link the two – clan/tribe.
Yes, as mentioned on the tribe page, this is the same as a display map category with -types and identity types.
BTW, I had added this remark to tribe already.
I can see that in many situations the term “display category with XYZ-types” may be too clunky
(though it nicely indicates that this is a generic notion where one is not supposed to take credit of originality just for making choices of XYZ…)
on the other hand, we have terms like ΠW-pretopos, so we might as well speak of ΠI-display categories (instead of “tribes, in this case).
Or why not just shorten it to “display”
(which can sensibly refer to the entire category as much as to its class of fibrations):
this would make “tribes” be ΠI-displays. Maybe not too bad.
1 to 10 of 10