Re: [HoTT] "type-theoretic model structures"

[Michael Shulman <shulman@sandiego.edu>]

Every object in a tribe is fibrant.  (A tribe is not just a display
map category; it also has the categorical structure corresponding to
identity types.)  For purposes of modeling type theory, the
non-fibrant objects are of course irrelevant, since every concrete
context does have a chain of display maps to 1.  And yes, of course,
one doesn't need infinitary structure to model type theory; as I said,
that's one of the differences between a tribe and a type-theoretic
model category, that the latter has infinitary structure but the
former doesn't.

On Mon, Feb 18, 2019 at 12:30 PM Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
>
> Haven't taken pains to examine Andre's treatise at least for the old
> display map categories there was no axiom assuring that for every
> object X there there is a chain of display maps from X to 1.
> So tribes/display map cats are more general model cats, isn't it?
>
> As a model of type theory I don't see any need to have infinitary
> axioms as are common in model cats.
>
> Thomas
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.