-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcsh.tex
180 lines (152 loc) · 6.74 KB
/
csh.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
% LaTeX 2e document, TAC style, 36 pp, Xy-pic ver ?, MikTeX version ?
\documentclass{tac}
\usepackage{subfiles}
\usepackage{amssymb, amsmath, stmaryrd}
\usepackage[backend=bibtex,citestyle=authoryear-icomp]{biblatex}
\usepackage[all]{xy}
\usepackage{url}
\title{Constructive Simplicial Homotopy}
\author{Wouter Pieter Stekelenburg}
\copyrightyear{2015,2016,2017,2018}
\address{Faculty of Mathematics, Informatics and Mechanics\\
University of Warsaw\\
Banacha 2\\
02-097 Warszawa\\
Poland}
\eaddress{[email protected]}
\keywords{realizability, simplicial homotopy, fibrant objects}
\amsclass{03D80, 18G30, 18G55}
\newcommand\hide[1]{}
\newcommand\cat\mathcal
\newcommand\set[1]{\left\{#1\right\}}
\mathrmdef{id}
\mathrmdef{dom}
\mathrmdef{cod}
\newcommand\ri{^*}
\mathbfdef[nno]{N}
\newcommand\dual{^{\mathrm{op}}}
\mathbfdef[simCat]\Delta
\newcommand\s{^{\simCat\dual}}
\newcommand\bang{!}
\newcommand\of{\mathord :}
\newcommand\simplex\Delta
\newcommand\cycle{\partial\Delta}
\newcommand\horn\Lambda
\newcommand\f{_f}
\newcommand\tuplet[1]{\left\langle #1 \right\rangle}
\newcommand\true{\mathtt{true}}
\newcommand\false{\mathtt{false}}
\newcommand\bool{\mathtt{bool}}
\mathrmdef{nat}
\mathssbxdef{Ar}
\mathssbxdef{Ob}
\newcommand\pp{\mathbin\diamond}
\newcommand\norm[1]{\Vert #1 \Vert}
\newcommand\ka\kappa
\newcommand\la\lambda
\mathrmdef{face}
\mathrmdef{colim}
\newcommand\ex{_{\textrm{ex}}}
\newcommand\citep[1]{[\cite{#1}]}
\mathrmdef{dim}
\newcommand\base{\mathbf{U}}
\mathssbxdef[sub]{Sub}
\newcommand\ambient{\mathfrak A}
\mathrmdef{uni}
\newcommand\disc{_{\rm disc}}
\mathrmdef{filler}
\newcommand\traco\omega
\newcommand\product[1]{\Pi #1 .}
\newcommand\coproduct[1]{\Sigma #1 .}
\newcommand\function[1]{\lambda #1 .}
\newcommand\keyword[1]{\emph{#1}\label{#1}}
\newcommand\icat\mathsf
\addbibresource{realizability}
\begin{document}
\begin{abstract} This paper develops the foundations of a constructive
simplicial homotopy that takes the logical limits of the internal languages of
elementary toposes in account. The aim is to develop new models of homotopy
type theory in particular models that are based on simplicial objects of
the effective topos and related categories.
\end{abstract}
\hide{
Three papers:
-simplicial homotopy
-complete categories [how they are preserved]
-the realizability model of HOTT [how to get a fibrant object out of a category]
Idea: reverse the order. definitions--theorem--lemmas. That way the purpose of
the lemmas is set up from the start.
}
\maketitle
\section*{Introduction}
This paper grew out of an attempt to build a \emph{recursive realizability}
model for \emph{homotopy type theory} by doing simplicial homotopy (see
\citep{Hovey99,GJSHT}) in a \emph{realizability topos} (see \citep{MR2479466})
and following the example of \citep{KLV12}.
Realizability toposes make simplicial homotopy harder because they may lack
infinite limits and colimits and their internal logic does not always satisfy
the principle of the excluded middle or the axiom of choice. We face these
challenges with the following tactics.
\begin{enumerate}
\item Replace the external notions of smallness used in the small object
argument with an internal one. A dense full internal subcategory provides
a kind of infinite limit that the internal language can access, while giving a
similar limitation of size.
\item Limit the class of cofibrations. In classical simplicial homotopy theory
every mono\-morphism is a cofibration. To keep classical arguments valid we
demand that certain properties of the monomorphisms are decidable.
\item Strengthen the lifting property. Fibrations come equipped with a
\emph{filler} that gives solutions for a family of basic lifting problems.
\end{enumerate}
\subsection*{Ambient category}
To avoid distracting peculiarities of realizability toposes, this paper works
with a generic \emph{elementary topos} (see definition \ref{topos}).
The exactness of toposes is not vital for the theory developed here, but
since \emph{ex/lex completion} are homotopy categories for 1-dimensional
simplices, I assume that there is no loss of generality in only considering
exact examples. %cite someone?
The minimal requirements include local cartesian closure and a full
dense internal subcategory. I believe that exact completions of
suitable categories are all toposes, based on Menni's work. %cite Menni
The advantage is being able to work with the first order internal language of
toposes.
\subsection*{Intended model} The \emph{category of assemblies}, which is the
category of $\neg\neg$-separated objects of \emph{the effective topos} up to
equivalence, has \emph{strongly} complete internal categories that are
not posets, in particular the \emph{category of modest sets} \citep{MR1097022,
MR2479466,MR1023803}. \emph{Strongly complete} means that the externalization
of the internal category is a complete fibred category. The category of
assemblies is not exact, but the ex/lex completion
preserves strongly complete internal categories. This exact completion is not
the effective topos, but it is a kind of realizability topos and it is
the intended ambient category in this paper \citep{MR1600009}.
The topos with a complete internal category that is not a poset is interesting,
because complete internal categories in Grothendieck toposes are necessarily
posets. This fact is traditionally attributed to Peter Freyd.
In the ex/lex completion \emph{modest fibrations} are fibrations whose
underlying morphisms are families of modest sets or quotients of such families
by modest families of equivalence relations--see \citep{MR1097022,MR1023803,
MR2479466}. There is a \emph{universal modest fibration} (see definition
\ref{universal modest fibration}) which is a \emph{univalent fibration} and
hence a potential model of homotopy type theory.
\subsection*{Conclusion} There are definitions of fibration, cofibration and
their acyclic counterparts (definition \ref{model structure}) in
elementary toposes that make the category of fibrant objects a \emph{model
category} (theorem \ref{model category}). For certain classes of fibrations
\emph{universal fibrations} (definition \ref{universal modest fibration}) are
automatically fibrant (theorem \ref{fibrant universe}).
\subsection*{Acknowledgments}
I am grateful to the Warsaw Center of Mathematics and Computer Science for the
opportunity to do the research leading to this paper. I am also grateful for
discussions with Marek Zawadowski and the seminars on simplicial homotopy
theory he organized during my stay at Warsaw University. Richard Garner, Peter
LeFanu Lumsdaine and Thomas Streicher made helpful comments on early drafts
of this paper.
\subfile{cshintro}
\subfile{cshmodel}
\subfile{cshfactor1}
\subfile{cshfactor2}
\subfile{cshwe}
\subfile{cshdescent}
\printbibliography
\end{document}