Hi, I have already written on this topic but I had some thoughts, actually this is related to my explanation of judgemental equality when teaching type theory. In Set Theory we have the element relation and equality and both are propositions, so in some sense dynamic. Eg whether a element relation holds may depend on some assumptions you have made and the same goes for equality. In type theory as in statically typed programming languages typing is a judgement, i.e. it is static (Actually I think there is a nice anology of set theory vs type theory = python vs Haskell). The reason is that we only talk about typed objects and as a consequence a phrase in our language refers to an object whose type is known statically. In particular the type doesn’t depend on some assumptions. If I say that x is a natural number then this is not dependent on some other assumptions I have made. Once I have dependent types this static reasoning needs to be extended. If I define n = 3 and I am checking that (1,2,3) is a vector of size n I need to unfold the definition of n. Actually I am already unfolding the definition of Vec anyway. Hence I am introducing a static equality judgement accompanying my static element judgement. Now what exactly are equalities that are known statically. It seems very natural to include beta equalities and the unfolding of recursive definitions. It is less obvious whether we should include eta equalities because we can only do this for some types and not for all. Hence one of the issues with definitional / judgemental equality is that it is not clear what exactly should be included and what not. With the introduction of HoTT another important aspect of judgemental equality became apparent: it is a universal strict equality. As I have argued it may be a good idea to have a stronger universal strict equality, in particular one which is not a static judgement. However, now we end up with 3 equalities: judgemental, strict and propositional equality (I stick to this term even if propositional equality may not be a proposition). This may make it difficult to convince the non type theorists that type theory is cool. Hence maybe we can only have 2 or 1 equality and reduce judgemental equality to a mere convenience but not a fundamental feature of type theory. Thorsten From: on behalf of Anders Mörtberg Date: Wednesday, 6 February 2019 at 04:13 To: Homotopy Type Theory Subject: [HoTT] Re: Why do we need judgmental equality? Note that judgmental equality is not only a convenience, but it also affects what is provable in your type theory. Consider the interval HIT, it is contractible and hence equivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Unit type. -- Anders On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote: 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. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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.