[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Shapes as types, to define extension types... \section{Definition} A **marked extensional well-founded relation** is an extensional well-founded relation $a \prec b$ on a set $S$ with a predicate $m(a)$. \section{References} * [[Tom de Jong]], [[Nicolai Kraus]], [[Fredrik Nordvall Forsberg]], [[Chuangjie Xu]], *Set-Theoretic and Type-Theoretic Ordinals Coincide* ([arXiv:2301.10696](https://arxiv.org/abs/2301.10696)) category: redirected to nlab