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