Author: nLab edit announcer Format: MarkdownItexthe concept of a weak type theory as a dependent type theory where all type formers are weak in the sense that they use identity types instead of judgmental equality in the computation and uniqueness rules
Anonymouse
<a href="https://ncatlab.org/nlab/revision/weak+type+theory/1">v1</a>, <a href="https://ncatlab.org/nlab/show/weak+type+theory">current</a>
the concept of a weak type theory as a dependent type theory where all type formers are weak in the sense that they use identity types instead of judgmental equality in the computation and uniqueness rules