[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \section{Basic rules} Our type theory contains basic types: identity types, dependent product types, dependent sum types, \section{Propositions and the type of all propositions} \section{Sets} \section{Power sets and subtypes} \begin{definition} A **predicate** on $T$ is a family of propositions in the context of the variable $x:T$. $$x:T \vdash P(x) \; \mathrm{type} \quad x:T \vdash p(x):\mathrm{isProp}(P(x))$$ \end{definition} \begin{definition} Given a type $T$, the **power set** of $T$ is defined as the function type from $T$ to the type of all propositions $\Omega$, $\mathcal{P}(T) \coloneqq T \to \Omega$ \end{definition} \begin{definition} A **material subtype** on $T$ is an element of the power set $S:\mathcal{P}(T)$. \end{definition} \begin{definition} The **local membership relation** $x \in_T S$ between elements $x:T$ and material subsets $S:\mathcal{P}(T)$ is defined as $$x \in_T S \coloneqq \mathrm{El}_\Omega(S(x))$$ \end{definition} \begin{theorem} The power set of a type is a set. \end{theorem} \begin{proof} By theorem XXX, if the codomain of a function type is a set, then the function type is a set. The type of all propositions is by definition a set. Since the power set of a type is a function type with codomain the type of all propositions, the power set of a type is a set. \end{proof} \begin{definition} Given a type $T$, the **improper material subtype** on $T$ is the material subtype $\Im_T:\mathcal{P}(T)$ such that for all elements $y:T$, the membership relation $y \in_T \Im_T$ is contractible. \end{definition} \begin{definition} Given a type $T$, there is a binary operation $(-)\cap(-):\mathcal{P}(T) \times \mathcal{P}(T) \to \mathcal{P}(T)$ on the power set of $T$ called the **intersection**, such that for all material subtypes $R:\mathcal{P}(T)$ and $S:\mathcal{P}(T)$ and elements $y:T$, the membership relation $y \in_T R \cap S$ is defined as $$y \in_T R \cap S \coloneqq (y \in_T R) \times (y \in_T S)$$ \end{definition} \begin{definition} Given a type $T$, there is a binary operation $(-)\cup(-):\mathcal{P}(T) \times \mathcal{P}(T) \to \mathcal{P}(T)$ on the power set of $T$ called the **union**, such that for all material subtypes $R:\mathcal{P}(T)$ and $S:\mathcal{P}(T)$ and elements $y:T$, the membership relation $y \in_T R \cup S$ is defined as $$y \in_T R \cup S \coloneqq [(y \in_T R) + (y \in_T S)]$$ where $[T]$ is the propositional truncation of $T$. \end{definition} \begin{definition} Given types $S$ and $T$, a function $f:S \to T$ is an **embedding** if for all elements $y:T$ the type of all elements $x:S$ such that $f(x) =_T y$ is a proposition. $$\mathrm{isEmbedding}(f) \coloneqq \prod_{y:T} \mathrm{isProp}\left(\sum_{x:S} f(x) =_T y\right)$$ \end{definition} \begin{definition} A **structural subtype** of $T$ is a type $S$ with an embedding $i:S \hookrightarrow T$. \end{definition} \begin{definition} Given a type $T$, $T$ is the **improper structural subtype**, with embedding given by the identity function on $T$. \end{definition} \begin{definition} Given a type $T$ and structural subtypes $R$ and $S$ with embeddings $i_R:R \hookrightarrow T$ and $i_S:S \hookrightarrow T$, the **intersection** of $R$ and $S$ is the dependent sum type $$R \cap S \coloneqq \sum_{r:R} \sum_{s:S} i_R(r) =_T i_S(s)$$ \end{definition} \begin{theorem} For every structural subtype of $T$ there is a material subtype on $T$, and for every material subtype on $T$ there is a structural subtype of $T$. \end{theorem} \begin{proof} Given a structural subtype $S$ of $T$ with embedding $i:S \hookrightarrow T$, we define the material subtype $P:\mathcal{P}(T)$ such that for all elements $y:T$, $$\mathrm{El}_\Omega(P(y)) \coloneqq \sum_{x:S} i(x) =_T y$$ The type $\sum_{x:S} i(x) =_T y$ is guaranteed to be a proposition, by definition of an embedding. Conversely, given a material subtype $P:\mathcal{P}(T)$ we define a structural subtype $S$ as the dependent sum type $$S \coloneqq \sum_{y:T} \mathrm{El}_\Omega(P(y))$$ with the embedding $i:S \hookrightarrow T$ defined as the first projection function in the elimination rules for the negative dependent sum type. \end{proof} | material subtype | predicate | structural subtype | |-|-|-| | $S:\mathcal{P}(T)$ | $y:T \vdash y \in_T S \coloneqq \mathrm{El}_\Omega(P(y))$ | $\sum_{y:T} y \in_T S$ | | $\lambda y:T.\mathrm{toElem}(P(y)):\mathcal{P}(T)$ | $y:T \vdash P(y) \qquad y:T \vdash p(y):\mathrm{isProp}(P(y))$ | $\sum_{y:T} P(y)$ | | $\lambda y:T.\mathrm{toElem}\left(\sum_{x:S} i(x) =_T y\right):\mathcal{P}(T)$ | $y:T \vdash i(x) =_T y$ | $S \qquad i:S \hookrightarrow T$ | category: redirected to nlab