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: <homotopyt...@
googlegroups.com > on behalf of Felix Rech <s9fe...@gmail.com>
Date: Wednesday, 30 January 2019 at 11:55
To: Homotopy Type Theory <homotopyt...@googlegroups.com >
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