appendix sectionnotation
Observational type theory
| symbol | meaning | first |
|---|---|---|
| symbol | meaning | first |
| observational equality at |
chapter 33 | |
| cast between observationally equal types | chapter 79 | |
| implementation name for strict propositions | chapter 34 | |
| universe of strict propositions at level |
chapter 79 |