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
Author: nLab edit announcer Format: MarkdownItexThe van der Berg paper was not the first paper which talks about weak type theory. Theo Winterhalter's thesis talks about weak type theory was published in 2020 before the van der Berg paper was put up on the arXiv in 2021.
Anonymouse
<a href="https://ncatlab.org/nlab/revision/diff/weak+type+theory/6">diff</a>, <a href="https://ncatlab.org/nlab/revision/weak+type+theory/6">v6</a>, <a href="https://ncatlab.org/nlab/show/weak+type+theory">current</a>
The van der Berg paper was not the first paper which talks about weak type theory. Theo Winterhalter’s thesis talks about weak type theory was published in 2020 before the van der Berg paper was put up on the arXiv in 2021.