Hi, what we need is a strict equality on all types. If we would state the laws of type theory just using the equality type we would also need to add coherence laws. Since I would include the laws for substitution (never understood why substitution is different from application) this would include the laws for infinity categories and this would make even basic type theory certainly much more complicated if not unusable. Instead one introduces a 2-level system with strict equality on one level and weak equality on another. For historic and pragmatic reasons this is combined with the computational aspects of type theory which is expressed as judgemental equality. However, there are reasons to separate these concerns, e.g. to work with higher dimensional constructions in type theory such as semi-simplicial types it is helpful to work with hypothetical strict equalities (see our paper (http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). I do think that the computational behaviour of type theory is important too. However, this can be expressed by demandic a form of computational adequacy, that is for every term there is a strictly equal normal form. It is not necessary that strict equality in general is decidable (indeed different applications of type theory may demand different decision procedures). Thorsten From: on behalf of Felix Rech Date: Wednesday, 30 January 2019 at 11:55 To: Homotopy Type Theory Subject: [HoTT] Why do we need judgmental equality? 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.