[HoTT] Re: Why do we need judgmental equality?

[Matt Oliveri <atmacen@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2441 bytes --]

On Saturday, February 9, 2019 at 6:53:15 AM UTC-5, Felix Rech wrote:
>
> Judgmental equality cannot be taken as assumptions. If one wants to use 
> judgmental equalities then one has to give concrete definitions that 
> satisfy those equalities and cannot hide the definition details. This makes 
> it impossible to change definitions later on without breaking constructions 
> that depend on them.
>

I worry that this will indeed be a modularity problem in practice. You 
generally can't specify behavior strictly at the interface between 
subsystems. Semantic purists would point out that such an interface 
wouldn't make sense anyway, unless the subsystem's type is an hset, and you 
use paths. In general, you should specify a bunch of coherences. Aside from 
being way harder though, we don't know how to do it in general, because of 
the infinite object problem.

With a 2-level theory, you could at least have second-class module 
signatures with strict equality.

In nontrivial definitions, judgmental equalities seem more arbitrary than 
> natural. If we define addition of natural numbers for example then we can 
> choose between x + 0 = x and 0 + x = x as judgmental equality but we cannot 
> have both. This makes it hard to find the right definitions and to predict 
> their behavior.
> Another motivation was of course that it would simplify the implementation 
> of proof checkers and parts of the metatheory.
>

This problem is solved by the special case of 2-level theories where strict 
equality is reflective (like extensional type theory (ETT)). What this does 
for you in practice is that you never have to see coercions between e.g. 
types (F (x + 0)) and (F (0 + x)), since they can be proven judgmentally 
equal by induction. (What I mean is that there's no record in terms of 
rewriting with nat equality. Not that all such reasoning can be done 
automatically. (It presumably is easy to automate both plus-zero rewrites 
though.))

Without reflective equality, strict equality doesn't seem to provide any 
benefit over paths in this case, because you need a coercion, and paths 
between nats are already unique.

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

[-- Attachment #1.2: Type: text/html, Size: 2959 bytes --]