Owen Lynch on Nostr: There's a succession of different categorical structures that correspond to larger ...

There's a succession of different categorical structures that correspond to larger and larger fragments of first-order logic:

- finite limit
- regular
- extensive
- topos (geometric logic)

We can think about a finite limit category as a clan (e.g. a model of dependent type theory with sigma types) where we have added extensional equality types.

If we instead add intensional equality types, we get to tribes. Thus, perhaps it makes sense to think about tribes as "intensional finite limit categories." Is there any work on moving up this hierarchy? That is, obviously people study adding pi types and fancy stuff to tribes, but is there a notion of a regular tribe? My guess is that a regular tribe interprets hProp-truncation, but I don't know what to think about further than that.