Re: [HoTT] Equality in the Model Type Framework

[Michael Shulman <shulman@sandiego.edu>]

On Wed, Jul 4, 2018 at 11:11 AM, Matt Oliveri <atmacen@gmail.com> wrote:
> Really though, I don't think the nice syntactic properties should be a
> concern when designing the categorical semantics of a full blown dependent
> type theory.

Right.  I would figure that nice syntactic properties usually only
apply to the initial/empty theory in a given doctrine, or perhaps more
generally to "free theories" i.e. without added judgmental equations.

> Wait a minute. Looking back at your "What Is an n-Theory?" post, you were
> thinking of things like HoTT and cubical type theory as doctrines. I don't
> understand how this fits with the modal type framework. A mode theory will
> not be enough to specify that kind of doctrine, will it? And if those are
> doctrines, why do theories also get judgmental equations? What are theories
> used for?

Roughly speaking, a doctrine specifies the "kinds of types" available
and how they relate (the judgmental structure), the operations
available on such types (type formers), the structure possessed by
these operations (term formers, intro/elim/etc.), and the laws
satisfied by that structure (computation beta/eta rules).  A theory in
that doctrine asserts the existence of particular types (you could
call them "nullary type formers"), structure possessed by types
(perhaps the particular ones you added, or perhaps ones constructed
using the doctrine operations), and axioms satisfied by that
structure.  So the things that a theory is "allowed to do" are a
subset of the things a doctrine is "allowed to do", but what gets
excluded is the "stuff" at the categorical top dimension, not the
"properties" (equations) at the categorical bottom dimension.  A
theory has to have equations (consider the theory of groups, for
instance, which has axioms for associativity and so on).

Our mode theories do not purport to describe *all* possible doctrines,
only a particularly simple and well-behaved class of them.  That said,
I believe intensional MLTT, at least, should be described by the
"tautological" or "simplest possible" mode theory with just one
comprehension-category mode and enough of the relevant F- and U-types,
including "indexed F-types" that specialize to Id-types.  Axioms like
funext and univalence could then be added in a particular theory.  The
judgmental/dependency structure of cubical TT should also be
describable by a suitably flexible version of our mode theories
(although we might not include that much generality in our first paper
on dependent modal type theory), with one mode for interval variables,
another dependent on it for face formulas, and a third
comprehension-category mode dependent on them for types.  The rest of
cubical TT is special, though.

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