On Sat, Feb 9, 2019 at 11:53 AM Felix Rech wrote: > One of the motivations for my question was that I actually expect > usability benefits if one worked in a dependent type theory without > judgmental equality that has good support by a proof assistant. > Yes, me too (but I think *a lot* of work needs to be done before we can have a proof assistant based on this idea which provides better usability than the current ones). I agree with your points. But I think "x + 0 = x versus 0 + x = x" is an example where I'd expect that one should be able to produce a conservativity proof and use both at the same time instead of choosing one. I think it's not necessary that we restrict ourselves to computation rules that come from actual definitions; anything that is "constructively conservative" over a weak theory should be allowed. In Agda, one can have additional computation rules, but it's not a safe feature. Nicolai > 1. 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. > 2. 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. > > I would appreciate any comments on this. > > -- > 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. > -- 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.