[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## Definition ## ### Material subtypes Let $\mathbb{2}$ denote the [[boolean domain]], with elements $0:\mathbb{2}$ and $1:\mathbb{2}$, and let $\mathrm{El}_\mathbb{2}$ be defined as $\mathrm{El}_\mathbb{2}(0) \coloneqq \mathbb{0}$ and $\mathrm{El}_\mathbb{2}(1) \coloneqq \mathbb{1}$, where $\mathbb{0}$ is the [[empty type]] and $\mathbb{1}$ is the [[unit type]]. This makes the [[boolean domain]] into a [[Tarski universe]]. The [[univalence axiom]] for the boolean domain then ensures that the boolean domain is a non-contractible set, and likewise ensures that, given a type $A$, the function type $A \to \mathbb{2}$ is a set. \begin{definition} A **material decidable subtype** on $A$ is an element of the function set $B:A \to \mathbb{2}$. \end{definition} \begin{definition} The **local membership relation** $x \in_A B$ between elements $x:A$ and material decidable subtypes $B:A \to \mathbb{2}$ is defined as $$x \in_A B \coloneqq \mathrm{El}_\mathbb{2}(B(x))$$ \end{definition} ### Structural decidable subtypes \begin{definition} A **structural decidable subtype** of $A$ is a type $B$ with a [[decidable]] [[embedding]] $i:B \hookrightarrow_d A$. $A$ is a **decidable supertype** of $B$. \end{definition} ### Comparison between material decidable subtypes, structural decidable subtypes, and decidable predicates In the [[inference rules]] for the [[type of all decidable propositions]], one has an operation $(-)_\mathbb{2}$ which takes a proposition $P$ and turns it into an element of the [[type of all propositions]] $P_\mathbb{2}:\mathbb{2}$. | material subtype | predicate | structural subtype | |-|-|-| | $B:A \to \mathbb{2}$ | $x:A \vdash x \in_A B \coloneqq \mathrm{El}_\mathbb{2}(B(x))$ | $\sum_{x:A} x \in_A B$ | | $\lambda x:A.(B(x))_\mathbb{2}:A \to \mathbb{2}$ | $x:A \vdash B(x) \qquad x:A \vdash p(x):(B(x) \simeq \mathbb{1}) + (B(x) \simeq \mathbb{0})$ | $\sum_{x:A} B(x)$ | | $\lambda x:A.\left(\sum_{y:B} i(y) =_A x\right)_\mathbb{2}:A \to \mathbb{2}$ | $x:A \vdash \sum_{y:B} i(y) =_A x$ | $B \qquad i:B \hookrightarrow_d A$ | category: redirected to nlab