The type checking rules are nonlinear (reuses metavariables). For example, for function application, the type of the argument needs to "equal" the domain of the function. What equality is that? It gets called judgmental equality. It's there in some sense even if it's just syntactic equality. But it seems really really hard to have judgmental equality be just syntactic equality, in a dependent type system. It would also be unnatural, from a computational perspective; the judgmental equations are saying something about the computational behavior of the system. On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: > > In section 1.1 of the HoTT book it says "In type theory there is also a > need for an equality judgment." Currently it seems to me like one could, in > principle, replace substitution along judgmental equality with explicit > transports if one added a few sensible rules to the type theory. Is there a > fundamental reason why the equality judgment is still necessary? > > Thanks, > Felix Rech > -- 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.