Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman <shulman@sandiego.edu>]

[-- Attachment #1: Type: text/plain, Size: 2762 bytes --]

On Thu, Dec 1, 2022 at 6:40 AM Andreas Nuyts <andreasnuyts@gmail.com> wrote:

> I think usability is hard to judge because there isn't yet good tool
> support to experiment with. But I believe that it can grow on the user. A
> lock simply means "we've moved into a modal subterm". The position of the
> lock in the context is important in order to keep track of which variables
> were introduced before/after moving into that modal subterm. When using a
> variable, you just need to make sure that the variable's modal annotation
> is ≤ the composition of the locks, i.e. the modality of the position where
> we currently are and where we want to use the variable.
>

This is a reasonable point.

I do think, however, that tool support is not necessary to evaluate
usability.  A really usable theory should also be usable informally, as in
the HoTT Book and my BFP paper.  This is what I have trouble with for
locking modal type theories; but it's certainly possible that I could train
myself to do it.  It certainly takes some mental training to use
split-context modal type theories informally too.

A more serious and mathematical issue is that MTT requires all modalities
to be right adjoints, semantically, because you have to have some operation
to interpret the locking functors on contexts.  (And FitchTT even requires
those left adjoints to themselves be (parametric) right adjoints.)  This
seems a serious restriction on the kinds of situations we can model.

One can argue that the process of interpreting a split-context theory
involves building a new category of contexts (some generalized kind of
comma category, perhaps) that *does* interpret such context operations, and
therefore could also interpret MTT.  But we don't have a general theory of
this yet.

To be precise, given an arbitrary 2-category M of modes, I would like there
to be a corresponding instance of a general modal type theory that can be
interpreted in any M-shaped diagram of suitable categories, with all the
morphisms of M corresponding to syntactic modalities, and not requiring the
existence of any additional adjoints in the semantics.  The LSR fibrational
framework achieves this for simple type theories, but I don't think there
is any published framework that achieves it for dependent type theories.

Best,
Mike

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpzCJLHMmB4ZPCX8Cn0_agLcD5_UZ1KsAkZZ8m0bLqHGKA%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 3546 bytes --]