diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf index dca5901..228f173 100644 Binary files a/blueprint/print/print.pdf and b/blueprint/print/print.pdf differ diff --git a/blueprint/src/natural_model.tex b/blueprint/src/natural_model.tex index fea0a66..5661d00 100644 --- a/blueprint/src/natural_model.tex +++ b/blueprint/src/natural_model.tex @@ -1,18 +1,33 @@ +In this section we describe the categorical semantics of +HoTT via Natural Models. +This will not be a detailed account of the syntax of HoTT, +but will be a detailed account of what is needed to interpret such syntax. + +\medskip + +\begin{notation*} + We will have two universe sizes - one small and one large. + We denote the category of small sets as $\set$ and the large sets as $\Set$. + For example, we could take the small sets $\set$ to be those in $\Set$ bounded in cardinality + by some inaccessible cardinal. +\end{notation*} + \subsection{Types} -Assume an inaccessible cardinal $\lambda$. Write $\Set$ for the category of all sets. Say that a set $A$ is $\lambda$-small if $|A| < \lambda$. Write $\Set_\lambda$ for the full -subcategory of $\Set$ spanned by $\lambda$-small sets. +% Assume an inaccessible cardinal $\lambda$. Write $\Set$ for the category of all sets. Say that a set $A$ is $\lambda$-small if $|A| < \lambda$. Write $\Set_\lambda$ for the full +% subcategory of $\Set$ spanned by $\lambda$-small sets. -Let $\mathbb{C}$ be a small category, i.e.~a category whose class of objects is a set and -whose hom-classes are sets. +Let $\catC$ be a small category, i.e.~a category whose class of objects is a $\set$ and +whose hom-classes are from $\set$. % We do not assume that $\mathbb{C}$ is $\lambda$-small for % the moment. - We write $\pshC$ for the category of presheaves over $\catC$, \[ \pshC \defeq [\catC^\op, \Set] \] +\medskip + % Because of the assumption of the existence of $\lambda$, $\pshC$ has additional structure. Let % \[ % \Term \to \Type @@ -22,6 +37,26 @@ \subsection{Types} % \Type(c) \defeq \{ A \co (\catC_{/c})^\op \to \Set_{\lambda} \} % \] +\begin{defn} + Following Awodey \cite{awodey2017naturalmodelshomotopytype}, + we say that a map $\tp : \Term \to \Type$ is presentable when + any fiber of a representable is representable. + In other words, given any $\Ga \in \catC$ and a map $A : \yo (\Ga) \to \Type$, + there is some representable $\Ga \cdot A \in \catC$ and maps $\disp{A} : \Ga \cdot A \to \Ga$ + and $\var_{A} : \yo (\Ga \cdot A) \to \Term$ forming a pullback + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJcXHlvIChcXEdhIFxcY2RvdCBBKSJdLFswLDEsIlxceW8gKFxcR2EpIl0sWzEsMSwiXFxUeXBlIl0sWzEsMCwiXFxUZXJtIl0sWzAsMSwiXFx5byAoXFxkaXNwe0F9KSIsMl0sWzEsMiwiQSIsMl0sWzMsMl0sWzAsMywiXFx2YXJfQSJdXQ== +\[\begin{tikzcd} + {\yo (\Ga \cdot A)} & \Term \\ + {\yo (\Ga)} & \Type + \arrow["{\var_A}", from=1-1, to=1-2] + \arrow["{\yo (\disp{A})}"', from=1-1, to=2-1] + \arrow[from=1-2, to=2-2] + \arrow["A"', from=2-1, to=2-2] +\end{tikzcd}\] +\end{defn} + +\medskip + The Natural Model associated to a presentable map $\tp \co \Term \to \Type$ consists of \begin{itemize} \item contexts as objects $\Gamma, \Delta, \ldots \in \catC$, diff --git a/blueprint/src/refs.bib b/blueprint/src/refs.bib index 84b0cfe..d4386bb 100644 --- a/blueprint/src/refs.bib +++ b/blueprint/src/refs.bib @@ -28,3 +28,13 @@ @misc{joyalnlabmodelstructuresoncat title = {Model structures on Cat}, howpublished = {\url{https://ncatlab.org/joyalscatlab/published/Model+structures+on+Cat}}, } + +@misc{awodey2017naturalmodelshomotopytype, + title={Natural models of homotopy type theory}, + author={Steve Awodey}, + year={2017}, + eprint={1406.3219}, + archivePrefix={arXiv}, + primaryClass={math.CT}, + url={https://arxiv.org/abs/1406.3219}, +} diff --git a/blueprint/src/web.bbl b/blueprint/src/web.bbl index e67c156..ab8efc8 100644 --- a/blueprint/src/web.bbl +++ b/blueprint/src/web.bbl @@ -1,5 +1,9 @@ \begin{thebibliography}{Awo23} +\bibitem[Awo17]{awodey2017naturalmodelshomotopytype} +Steve Awodey. +\newblock Natural models of homotopy type theory, 2017. + \bibitem[Awo23]{awodey2023hofmannstreicheruniverses} Steve Awodey. \newblock On hofmann-streicher universes, 2023.