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.