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

[Andreas Nuyts <andreasnuyts@gmail.com>]

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

Hi everyone,

I finally found time to read up on this lengthy conversation.

Jon wrote:

    It is revealing that nobody has proposed a notion of **model** of
    type theory in which the admissible structural rules do not hold;
    this would be the necessary form taken by any evidence for the
    thesis that it is important for structural rules to not be derivable.


I think, on the contrary, that such models are not acknowledged as being 
models, because the language without substitution is in general not 
really the language of interest. An example of a model disrespecting 
substitution is the prettyprinter by Allais, Atkey, Chapman, McBride & 
McKinna (2021):
https://doi.org/10.1017/S0956796820000076
Indeed, substitution is no longer possible after prettyprinting, but all 
other language constructs are supported. Note that if a substitution 
operation is unavailable in a model, then the β-rule for functions 
cannot even be stated in that model, let alone asked to hold. So a model 
that fails to have a substitution operation necessarily also disrespects 
the equational theory of a language with such a β-rule. Prettyprinting 
indeed disrespects βη-equality.

Mike wrote:

    MTT is also not equivalent to split-context theories, and IMHO is
    less pleasant to work with in practice.


I'm reluctant to postulate here that any split-context theory is 
equivalent to some instance of MTT, but I would be quite surprised if 
you ever face any practical problems when abandoning a split-context 
system in favour of MTT. If you're thinking in particular about a system 
with crisp and non-crisp variables: such a system is implemented by 
Andrea in agda-flat. At the last Agda meeting, we have been 
investigating how mature the current modality system in Agda is and how 
feasible it is to support full MTT. One thing we observed is that - of 
all the parallel modality systems implemented in Agda - the cohesive one 
(of which only the flat and non-flat modalities are exposed to the user) 
is actually the one that adheres to the discipline of MTT (by having a 
third "squash" modality that effectively removes variables from the 
context).
Both regarding usability and equivalence, do not be misled by the 
invasive-looking locks. These locks have two confluent histories:
- there is a history of fitch-style logics,
- there is a history of modal logics with left-division. When 
implementing Menkar, which was intended as a proof assistant for general 
multimode systems with left division, I observed at some point that the 
left division of all modalities in the context actually never needs to 
be computed and can thus be regarded as a context /constructor/, rather 
than as an operation (i.e. admissibility of left division was not 
required, in none of the senses of the word mentioned so far). Modal 
Agda does use an eagerly computed left division. These systems with left 
division are very closely related to dual context systems.

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.

I am happy to discuss this matter further if you have any questions or 
doubts.

Best regards,
Andreas Nuyts

On 18.11.22 18:14, Michael Shulman wrote:
> That's an interesting question.  I was thinking of operations and 
> equalities, and annotations are neither of those, but I can see that 
> they're somewhat similar in spirit.  But I find it even more difficult 
> to imagine how to define this phenomenon precisely in a way that would 
> include them...
>
> On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling <jon@jonmsterling.com> wrote:
>
>     On 18 Nov 2022, at 11:56, Michael Shulman wrote:
>
>     > Thanks.  It does sound like we mostly agree.  I would probably
>     argue that
>     > even for type theories in development, where we don't yet know
>     that full
>     > definitional equality is decidable -- or intrinsically
>     ill-behaved type
>     > theories like Lean, or Agda with non-confluent rewrite rules, where
>     > definitional equality *isn't* decidable -- there is still value
>     in being
>     > able to reduce just substitutions.  But I think that's a
>     relatively minor
>     > point.
>     >
>     > Maybe we can work out some way to use words so that this underlying
>     > agreement is evident.  For instance, can we find a third word to use
>     > alongside "admissible" and "derivable" to refer to
>     operations/equalities
>     > like substitution and its theory, which hold in all reasonable
>     models, and
>     > can be made admissible in some presentations, but more
>     importantly can be
>     > eliminated in an equality-checking algorithm?
>     >
>
>     Cool, it's a relief to start getting this cleared up! I really
>     agree with you that there is a need for terminology to describe
>     the situation you mention, and maybe even more, there is a need to
>     define this phenomenon...
>
>     I wonder if we can think of more concrete examples of this. For
>     instance, in many versions of syntax (like bidirectional ones) we
>     can choose to drop certain annotations because they will be
>     available as part of the flow of information in the elaboration
>     algorithm. Would these be an example of the phenomenon you are
>     describing, or is it something different?
>
>     Best,
>     Jon
>
> -- 
> 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/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com 
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.

-- 
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/4d352fc9-c4d3-2304-1510-17cd653513a8%40gmail.com.

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