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

[Jon Sterling <jon@jonmsterling.com>]

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/92CA5128-A764-47EA-8ECD-B6931F7EA7AF%40jonmsterling.com.