\tableofcontents \section{Idea} There is a relation between [[category theory]] and [[dependent type theory]] which states that the [[internal logic]] or [[syntax]] of any [[category]] is a [[dependent type theory]] and the [[semantics]] of any dependent type theory is a [[category]]. In particular, this means that every model of [[ETCS]], or every [[well-pointed topos]] with a [[natural numbers object]] and whose epimorphisms are split, has an associated [[dependent type theory]]. In this article, we present a model of dependent type theory whose types behave as the objects of ETCS do, and whose terms behave as the global elements of ETCS do. \section{Presentation} The [[dependent type theory]] we shall be presenting here is similar to [[objective type theory]] of [[Benno van den Berg]] and [[Martijn den Besten]], in that it doesn’t have [[definitional equality]]. The lack of definitional equality means that the theory is both simpler, and behaves more like traditional formulations of [[ETCS]], which usually also doesn’t have definitional equality. \subsection{Judgments and contexts} The dependent type theory model of ETCS consists of three judgments: set judgments $A \; \mathrm{set}$, where we judge $A$ to be a set, membership judgments, where we judge $a$ to be an element of $A$, $a \in A$, and context judgments, where we judge $\Gamma$ to be a context, $\Gamma \; \mathrm{ctx}$. Contexts are lists of membership judgments $a \in A$, $b \in B$, $c \in C$, et cetera, and are formalized by the rules for the empty context and extending the context by a membership judgment $$\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{set}}{(\Gamma, a \in A) \; \mathrm{ctx}}$$ \subsection{Structural rules} The structural rules of this theory include the [[variable rule]], the [[weakening rule]], and the [[substitution rule]]. The variable rule states that we may derive a membership judgment if the membership judgment is in the context already: $$\frac{\vdash \Gamma, a \in A, \Delta \; \mathrm{ctx}}{\vdash \Gamma, a \in A, \Delta \vdash a \in A}$$ Let $\mathcal{J}$ be any arbitrary judgment. Then we have the following rules: The weakening rule: $$\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{set}}{\Gamma, a \in A, \Delta \vdash \mathcal{J}}$$ The substitution rule: $$\frac{\Gamma \vdash a \in A \quad \Gamma, b in A, \Delta \vdash \mathcal{J}}{\Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}$$ The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations. \subsection{Indexed sets and indexed elements} An indexed set is a set $B$ in the context of the variable judgment $x \in A$, $x \in A \vdash B \; \mathrm{set}$, they are usually written as $B(x)$ to indicate its dependence upon $x$. An indexed element is an element $b \in B$ in the context of the variable judgment $x \in A$, $x \in A \vdash b \in B$. Sections are likewise usually written as $b(x)$ to indicate its dependence upon $x$. \subsection{Equality} Equality of elements of a set is represented by a set. This in other [[dependent type theories]] is called a [[identity type]] or a path type. Equality of proofs comes with a formation rule, an introduction rule, an elimination rule, and a computation rule: Formation rule for equality of elements: $$\frac{\Gamma \vdash A \; \mathrm{set}}{\Gamma, a \in A, b \in A \vdash a =_A b \; \mathrm{set}}$$ Introduction rule for equality of elements: $$\frac{\Gamma \vdash A \; \mathrm{set}}{\Gamma, a \in A \vdash \mathrm{refl}_A(a) \in a =_A a}$$ Elimination rule for equality of elements: $$\frac{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{set} \quad \Gamma, a \in A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t \in C(a, a, \mathrm{refl}_A(a))}{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash J(t, a, b, p) \in C(a, b, p)}$$ Computation rules for equality of elements: $$\frac{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash C(a, b, p) \; \mathrm{set} \quad \Gamma, a \in A, \Delta(a, a, \mathrm{refl}_A(a)) \vdash t \in C(a, a, \mathrm{refl}_A(a))}{\Gamma, a \in A, b \in A, p \in a =_A b, \Delta(a, b, p) \vdash \beta_{=_A}(a) \in J(t, a, a, \mathrm{refl}(a)) =_{C(a, a, \mathrm{refl}_A(a))} t}$$ Uniqueness rules for equality of elements: $$\frac{\Gamma\vdash A \; \mathrm{set} \quad \Gamma \vdash a \in A \quad \Gamma \vdash p \in a =_A a}{\Gamma\vdash K(a, p) \in p =_{a =_A a} refl_A(a)}$$ \subsection{Definitions of elements} Parts of the following section is adapted from [[Egbert Rijke]]'s [[Introduction to Homotopy Type Theory]]: We can make definitions at the end of a derivation if the conclusion is a certain element of a set in context, where we have a derivation $$\frac{\mathcal{D}}{\Gamma \vdash a \in A}$$ if we wish to make a definition $b \coloneqq a$, then we can extend the derivation tree with $$\frac{\Gamma \vdash a \in A}{\Gamma \vdash b \coloneqq a \in A}$$ The effect of such a definition is that we have extended our type theory with a new constant $b$, for which the following inference rules are valid $$\frac{\mathcal{D}}{b \in A} \qquad \frac{\mathcal{D}}{\mathrm{defeq}(a, b) \in b =_A a}$$ \subsection{Function sets} Formation rules for function sets: $$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma \vdash B \; \mathrm{set}}{\Gamma \vdash B^A \; \mathrm{set}}$$ Introduction rules for function sets: $$\frac{\Gamma, x \in A \vdash b(x) \in B}{\Gamma \vdash (x \mapsto b(x)) \in B^A}$$ Elimination rules for function sets: $$\frac{\Gamma \vdash f \in B^A \quad \Gamma \vdash a \in A}{\Gamma \vdash f(a) \in B}$$ Computation rules for function sets: $$\frac{\Gamma, x \in A \vdash b(x) \in B \quad \Gamma \vdash a \in A}{\Gamma \vdash \beta_{\mathrm{func}} \in (x \mapsto b(x))(a) =_{B} b}$$ Uniqueness rules for function sets: $$\frac{\Gamma \vdash f \in B^A}{\Gamma \vdash \eta_{\mathrm{func}} \in f =_{B^A} (x \to f(x))}$$ \subsection{Indexed product sets} Formation rules for Pi types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \prod_{x:A} B(x) \; \mathrm{type}}$$ Introduction rules for Pi types: $$\frac{\Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\prod_{x:A} B(x)}$$ Elimination rules for Pi types: $$\frac{\Gamma \vdash f:\prod{x:A} B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B[a/x]}$$ Computation rules for Pi types: $$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_\Pi:\lambda(x:A).b(x)(a) =_{B[a/x]} b[a/x]}$$ Uniqueness rules for Pi types: $$\frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash \eta_\Pi:f =_{\prod_{x:A} B(x)} \lambda(x).f(x)}$$ \subsection{Product types} We use the negative presentation for product types. Formation rules for product types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \times B \; \mathrm{type}}$$ Introduction rules for product types: $$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash (a, b):A \times B}$$ Elimination rules for product types: $$\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_2(z):B}$$ Computation rules for product types: $$\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\times 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \beta_{\times 2}:\pi_2(a, b) =_B b}$$ Uniqueness rules for product types: $$\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \eta_\times:z =_{A \times B} (\pi_1(z), \pi_2(z))}$$ \subsection{Sigma types} We use the negative presentation for sigma types. Formation rules for Sigma types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}$$ Introduction rules for Sigma types: $$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B[a/x]}{\Gamma \vdash (a, b):\sum_{x:A} B(x)}$$ Elimination rules for Sigma types: $$\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_2(z):B(\pi_1(z))}$$ Computation rules for Sigma types: $$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 1}:\pi_1(a, b) =_A a} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \beta_{\Sigma 2}:\pi_2(a, b) =_{B\pi_1(a, b)} b}$$ Uniqueness rules for Sigma types: $$\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \eta_\Sigma:z =_{\sum_{x:A} B(x)} (\pi_1(z), \pi_2(z))}$$ \section{Pullbacks} Given two functions $f \in A^B$ and $g \in A^C$, the [[pullback]] of $f$ and $g$ is given by the set $$\biguplus_{b \in B} \biguplus_{c \in C} f(b) =_A g(c)$$ \section{Singleton} Use the negative presentation of a unit type. ... Thus, the [[dependent type theory]] models a [[locally cartesian closed category]] with [[pullbacks]] and a [[terminal object]], and the category is thus [[finitely complete]] and [[cartesian closed]] \section{Set of truth values} \section{References} * *Homotopy Type Theory: Univalent Foundations of Mathematics*, The Univalent Foundations Program, Institute for Advanced Study, 2013. ([web](http://homotopytypetheory.org/book/), [pdf](http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf)) * Egbert Rijke, *Introduction to Homotopy Type Theory*, Cambridge Studies in Advanced Mathematics, Cambridge University Press ([pdf](https://raw.githubusercontent.com/martinescardo/HoTTEST-Summer-School/main/HoTT/hott-intro.pdf)) (478 pages) * Benno van den Berg, Martijn den Besten, *Quadratic type checking for objective type theory* ([arXiv:2102.00905](https://arxiv.org/abs/2102.00905)) \section{See also} * [[homotopy type theory]]