diff --git a/.cspell.json b/.cspell.json
index 16ef8c311..5fc8c1bd8 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -14,7 +14,9 @@
"ndash",
"emptyset",
"varnothing",
- "mdash"
+ "mdash",
+ "comphaus",
+ "esbuild"
],
"words": [
"abelian",
@@ -26,6 +28,7 @@
"anneaux",
"Artin",
"Auslander",
+ "axiomatization",
"bijection",
"bijections",
"bijective",
@@ -36,6 +39,7 @@
"Catabase",
"catdat",
"Catégories",
+ "Čech",
"clopen",
"Clowder",
"coaccessible",
@@ -59,6 +63,7 @@
"coequalizes",
"coexponentials",
"cofiltered",
+ "cofiltering",
"cofinitary",
"cofull",
"cogenerates",
@@ -71,9 +76,11 @@
"colimits",
"comonad",
"comonadic",
+ "compactification",
"conormal",
"copower",
"copowers",
+ "copresentability",
"copresentable",
"coprime",
"coproduct",
@@ -157,6 +164,7 @@
"Mathoverflow",
"metrizable",
"Moerdijk",
+ "monadicity",
"monic",
"monoid",
"monoidal",
@@ -205,11 +213,16 @@
"semigroup",
"semigroups",
"semisimple",
+ "Serre",
"setoid",
"Sheafifiable",
"simplicial",
"subalgebra",
+ "subbasic",
+ "subbasis",
+ "subcollection",
"subconjugated",
+ "subcover",
"submanifold",
"submonoid",
"subobject",
@@ -229,10 +242,13 @@
"surjectivity",
"Tarski",
"tensoring",
+ "Tietze",
"topoi",
"Turso",
+ "Tychonoff",
"unital",
"unitalization",
+ "Urysohn",
"vercel",
"Vite",
"Wedderburn",
diff --git a/databases/catdat/data/categories/CompHaus.yaml b/databases/catdat/data/categories/CompHaus.yaml
new file mode 100644
index 000000000..fcbde4b2d
--- /dev/null
+++ b/databases/catdat/data/categories/CompHaus.yaml
@@ -0,0 +1,126 @@
+id: CompHaus
+name: category of compact Hausdorff spaces
+notation: $\CompHaus$
+objects: compact Hausdorff spaces
+morphisms: continuous functions
+description: This is the full subcategory of $\Top$ consisting of those spaces that are compact and Hausdorff.
+nlab_link: https://ncatlab.org/nlab/show/compact+Hausdorff+space
+
+tags:
+ - topology
+
+related_categories:
+ - Haus
+ - Top
+
+satisfied_properties:
+ - property_id: locally small
+ reason: It is a full subcategory of $\Top$, which is locally small.
+
+ - property_id: semi-strongly connected
+ reason: This is already true for $\Top$.
+
+ - property_id: products
+ reason: By the Tychonoff product theorem, a product in $\Top$ of compact Hausdorff spaces is compact; it is also clearly Hausdorff. Since the forgetful functor from $\CompHaus$ to $\Top$ is fully faithful, this limit is reflected in $\CompHaus$ as well.
+ check_redundancy: false
+
+ - property_id: equalizers
+ reason: 'The equalizer in $\Top$ of two continuous functions $f, g : X \rightrightarrows Y$ between compact Hausdorff spaces is a closed subspace of $X$, and therefore it is also compact Hausdorff. Since the forgetful functor from $\CompHaus$ to $\Top$ is fully faithful, this limit is reflected in $\CompHaus$ as well.'
+ check_redundancy: false
+
+ - property_id: cocomplete
+ reason: $\CompHaus$ is a reflective subcategory of $\Top$, with the reflector being the Stone-Čech compactification functor. See nLab for example. Therefore, as usual, we can form colimits in $\CompHaus$ by forming colimits in $\Top$ and then applying Stone-Čech compactification.
+ check_redundancy: false
+
+ - property_id: generator
+ reason: The one-point space is a generator because it represents the forgetful functor to $\Set$, which is faithful.
+
+ - property_id: cogenerator
+ reason: 'The unit interval $[0, 1]$ is a cogenerator: Suppose we have $f, g : X \rightrightarrows Y$ with $f \ne g$. Choose $x\in X$ such that $f(x) \ne g(x)$. Then by Urysohn''s lemma, there is a continuous function $h : Y \to [0, 1]$ such that $h(f(x)) = 0$ and $h(g(x)) = 1$. Therefore, $h\circ f \ne h\circ g$.'
+
+ - property_id: effective congruences
+ # TODO: rework this when Barr-exact is added
+ reason: The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example nLab. Therefore, by this result, $\CompHaus$ is Barr-exact, and in particular it has effective congruences.
+
+ - property_id: regular
+ # TODO: rework this when Barr-exact is added
+ reason: The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example nLab. Therefore, by this result, $\CompHaus$ is Barr-exact and in particular is regular.
+
+ - property_id: coregular
+ reason:
+ 'It suffices to show that pushouts preserve (regular) monomorphisms in $\CompHaus$. Thus, suppose we have a pushout square
+ $$\begin{CD}
+ A @> i >> B \\
+ @V f VV @VV g V \\
+ C @>> j > D,
+ \end{CD}$$
+ with $i : A \hookrightarrow B$ a monomorphism. Then for any pair of distinct elements $c, c'' \in C$, by Urysohn''s lemma there exists $\gamma : C \to [0, 1]$ with $\gamma(c) = 0$ and $\gamma(c'') = 1$. Also, by Tietze''s extension theorem, there exists $\beta : B \to [0, 1]$ such that $\beta \circ i = \gamma \circ f$. By the pushout property, there is a unique $\delta : D \to [0, 1]$ such that $\delta \circ g = \beta$ and $\delta \circ j = \gamma$. Since $\delta(j(c)) \ne \delta(j(c''))$, we conclude that $j(c) \ne j(c'')$. This shows that $j$ is injective, so it is a regular monomorphism.'
+
+ - property_id: extensive
+ reason: This follows as for $\Top$ or $\Haus$ since finite coproducts in $\CompHaus$ are formed as disjoint union spaces with the disjoint union topology.
+
+ - property_id: epi-regular
+ reason: |-
+ First, any epimorphism $f : X \to Y$ is surjective: if not, its image would be a proper subset of $Y$, which is compact and hence closed. Then by Urysohn's lemma, there would be a non-zero continuous function $g : Y \to [0, 1]$ which is $0$ on the image; but then $g \circ f = 0 \circ f$, giving a contradiction.
+ Now the identity morphism from $Y$, with the quotient topology of $f$, to $Y$ with its given topology is a bijective continuous function between compact Hausdorff spaces, so it is a homeomorphism. In other words, $f$ is a quotient map. Therefore, we see that if $g, h : E \rightrightarrows X$ is the kernel pair of $f$, and $U : \CompHaus \to \Top$ is the forgetful functor, then $U(f)$ is the coequalizer of $U(g)$ and $U(h)$. Since $U$ is fully faithful, that implies $f$ is the coequalizer of $g$ and $h$.
+
+ - property_id: cofiltered-limit-stable epimorphisms
+ reason: 'Suppose we have a cofiltered diagram of epimorphisms $(f_i : X_i \to Y_i)$, and $y = (y_i) \in \lim_i Y_i$. Then by lemma 1 here, the limit of $f_i^{-1}(\{ y_i \})$ is non-empty. If $x$ is in this limit, that implies that $(\lim_i f_i)(x) = y$.'
+
+ - property_id: locally copresentable
+ reason: A proof can be found here.
+
+unsatisfied_properties:
+ - property_id: skeletal
+ reason: This is trivial.
+
+ - property_id: Malcev
+ reason: This is clear since $\FinSet$ is not Malcev and can be interpreted as the subcategory of finite discrete spaces.
+
+ - property_id: regular subobject classifier
+ reason: The proof is almost identical to the one for $\Haus$.
+
+ - property_id: natural numbers object
+ reason: >-
+ Let $I := [0, 1]$. If a natural numbers object $(N, z : 1 \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition
+ $$\begin{align*}
+ I & \overset{y \times \id}\longrightarrow N\times I \to I\times I \overset{p_2}\longrightarrow I, \\
+ x & \mapsto (y, x) \mapsto (x, \delta_{x,1}) \mapsto \delta_{x,1},
+ \end{align*}$$
+ would have to be continuous.
+
+ - property_id: filtered-colimit-stable monomorphisms
+ reason: 'The proof is similar to $\Haus$. For $n \geq 1$ let $X_n$ be the pushout of $[1/n, 1] \hookrightarrow [0, 1]$ with itself. That is, $X_n$ is the union of two unit intervals $[0, 1] \times \{ 1 \}$ and $[0, 1] \times \{ 2 \}$ where we identify $(x,1) \equiv (x,2)$ when $x \geq 1/n$. As in the construction for $\Haus$, we see that the colimit in $\Haus$ is $[0, 1]$ where all corresponding points of both unit intervals are identified. Since this is compact Hausdorff, it also provides the colimit in $\CompHaus$. Again, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to [0,1]$ in the colimit, which is not a monomorphism.'
+
+ - property_id: exact cofiltered limits
+ reason: |-
+ Consider the $\IN$-codirected systems $X_n := [0, 1] \times [0, 1/n]$ with the maps $X_{n+1} \to X_n$ being inclusion maps, and $Y_n := [0, 1+1/n]$ with the maps $Y_{n+1} \to Y_n$ also being inclusion maps. We define $f_n : X_n \to Y_n$, $(x, y) \mapsto x$ and $g_n : X_n \to Y_n$, $(x, y) \mapsto x+y$. It is straightforward to check these give morphisms of $\IN$-codirected systems in $\CompHaus$.
+ Now for each $n$, we claim the coequalizer of $f_n$ and $g_n$ is a singleton space. To see this, we prove the more general result that for $r, s > 0$ the coequalizer of $f, g : [0, r] \times [0, s] \rightrightarrows [0, r+s]$, $f(x,y) = x$, $g(x,y) = x+y$ is a singleton. We must show that for any $h : [0, r+s] \to T$ with $h\circ f = h\circ g$, then $h$ is constant. To this end, we show by induction on $n$ that whenever $x \in [0, r+s]$ and $x \le ns$, we have $h(x) = h(0)$. The base case $n=0$ is trivial. For the inductive step, if $x \le s$, then $f(0,x) = 0$ and $g(0,x) = x$, so $h(0) = h(x)$. Otherwise, we have $x-s \in [0,r]$ and $x-s \le (n-1)s$, so by inductive hypothesis $h(x-s) = h(0)$. Also, $f(x-s, s) = x-s$ and $g(x-s, s) = x$, so $h(x-s) = h(x)$, completing the induction. With this established, the desired result follows from the case $n := \lceil r/s \rceil + 1$.
+ On the other hand, $\lim X_n \simeq [0, 1] \times \{ 0 \}$; $\lim Y_n \simeq [0, 1]$; and $\lim f_n = \lim g_n$, $(x, 0) \mapsto x$. Thus, the coequalizer of $\lim f_n$ and $\lim g_n$ is $[0, 1]$, showing that the limit does not preserve this coequalizer.
+
+special_objects:
+ initial object:
+ description: empty space
+ terminal object:
+ description: singleton space
+ coproducts:
+ description: Stone-Čech compactification of the disjoint union with the disjoint union topology (in the finite case, the disjoint union is already compact Hausdorff so Stone-Čech compactification is not necessary)
+ products:
+ description: direct product with the product topology (which is compact by the Tychonoff product theorem)
+
+special_morphisms:
+ isomorphisms:
+ description: homeomorphisms
+ reason: This is easy.
+ monomorphisms:
+ description: injective continuous maps (which are automatically closed embeddings)
+ reason: 'For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. To prove the parenthetical remark, given an injective continuous function $f : X \to Y$ between compact Hausdorff spaces, the image of $f$ is a closed subset. Also, the induced map from $X$ to $\im(f)$ with the subspace topology is a bijective continuous map between compact Hausdorff spaces, so it is a homeomorphism.'
+ epimorphisms:
+ description: surjective continuous maps (which are automatically quotient maps)
+ reason: For the non-trivial direction, and for a proof of the parenthetical remark, see the proof above that $\CompHaus$ is epi-regular.
+ regular monomorphisms:
+ description: same as monomorphisms
+ reason: This is because the category is mono-regular.
+ regular epimorphisms:
+ description: same as epimorphisms
+ reason: This is because the category is epi-regular.
diff --git a/databases/catdat/data/categories/Haus.yaml b/databases/catdat/data/categories/Haus.yaml
index b92dffc74..931c4a85a 100644
--- a/databases/catdat/data/categories/Haus.yaml
+++ b/databases/catdat/data/categories/Haus.yaml
@@ -12,6 +12,7 @@ tags:
related_categories:
- Met_c
- Top
+ - CompHaus
satisfied_properties:
- property_id: locally small
@@ -68,7 +69,10 @@ unsatisfied_properties:
reason: 'Recall the counterexample for sets: The unique maps $\IN_{\geq n} \to 1$ are surjective, but their limit $0 = \bigcap_{n \geq 0} \IN_{\geq n} \to 1$ is not. This also works in $\Haus$ by using discrete topologies. We could also apply a variant of (the dual of) this lemma to the discrete topology functor $\Set \to \Haus$, which does not preserve all cofiltered limits, but does preserve intersections.'
- property_id: filtered-colimit-stable monomorphisms
- reason: 'The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the pushout of $[-1/n,+1/n] \hookrightarrow \IR$ with itself. That is, $X_n$ is the union of two lines $\IR \times \{1\}$ and $\IR \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \leq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\Top$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \leq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\IR$ where all points of both lines are identified, and it provides the colimit in $\Haus$. Now, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to \IR$ in the colimit, which is no monomorphism.'
+ reason: |-
+ The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the pushout of
+ $$(-\infty, -1/n] \cup [1/n, \infty) \hookrightarrow \IR$$
+ with itself. That is, $X_n$ is the union of two lines $\IR \times \{1\}$ and $\IR \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\Top$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\IR$ where all points of both lines are identified, and it provides the colimit in $\Haus$. Now, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to \IR$ in the colimit, which is not a monomorphism.
special_objects:
initial object:
diff --git a/databases/catdat/data/category-implications/congruences.yaml b/databases/catdat/data/category-implications/congruences.yaml
index a6f0b3ea0..def9ee3aa 100644
--- a/databases/catdat/data/category-implications/congruences.yaml
+++ b/databases/catdat/data/category-implications/congruences.yaml
@@ -8,6 +8,16 @@
reason: This holds by definition of a regular category.
is_equivalence: false
+- id: regular_well-powered_well-copowered
+ assumptions:
+ - regular
+ - epi-regular
+ - well-powered
+ conclusions:
+ - well-copowered
+ reason: The regularity condition gives a bijection between the collection of quotients of $X$ and the collection of effective congruences on $X$, where the latter is a subcollection of the collection of subobjects of $X\times X$.
+ is_equivalence: false
+
- id: congruence_quotients_are_reflexive_coequalizers
assumptions:
- reflexive coequalizers
diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml
index 149a871f7..d33feabd3 100644
--- a/databases/catdat/data/macros.yaml
+++ b/databases/catdat/data/macros.yaml
@@ -80,6 +80,7 @@
\PMet: \mathbf{PMet}
\Top: \mathbf{Top}
\Haus: \mathbf{Haus}
+\CompHaus: \mathbf{CompHaus}
\sSet: \mathbf{sSet}
\Man: \mathbf{Man}
\LRS: \mathbf{LRS}
diff --git a/static/pdf/.gitignore b/static/pdf/.gitignore
index 372e1325b..662623f71 100644
--- a/static/pdf/.gitignore
+++ b/static/pdf/.gitignore
@@ -1,5 +1,7 @@
# Files from Latex Workshop
*.aux
+*.bbl
+*.blg
*.fdb_latexmk
*.fls
*.log
diff --git a/static/pdf/comphaus_copresentable.bib b/static/pdf/comphaus_copresentable.bib
new file mode 100644
index 000000000..c94f74256
--- /dev/null
+++ b/static/pdf/comphaus_copresentable.bib
@@ -0,0 +1,78 @@
+@misc{marra2020characterisationcategorycompacthausdorff,
+ title={A characterisation of the category of compact {H}ausdorff spaces},
+ author={Vincenzo Marra and Luca Reggio},
+ year={2020},
+ eprint={1808.09738},
+ archivePrefix={arXiv},
+ primaryClass={math.CT},
+ url={https://arxiv.org/abs/1808.09738},
+}
+@article{HUSEK2019251,
+ title = {Factorization and local presentability in topological and uniform spaces},
+ journal = {Topology and its Applications},
+ volume = {259},
+ pages = {251-266},
+ year = {2019},
+ note = {William Wistar Comfort (1933-2016): In Memoriam},
+ issn = {0166-8641},
+ doi = {https://doi.org/10.1016/j.topol.2019.02.033},
+ url = {https://www.sciencedirect.com/science/article/pii/S0166864119300513},
+ author = {M. Hušek and J. Rosický},
+ keywords = {Realcompact space, Factorization, Locally presentable category},
+ abstract = {Investigating dual local presentability of some topological and uniform classes, a new procedure is developed for factorization of maps defined on subspaces of products and a new characterization of local presentability is produced. The factorization is related to large cardinals and deals, mainly, with realcompact spaces. Instead of factorization of maps on colimits, local presentability is characterized by means of factorization on products.}
+}
+@article{Marra_2017,
+ title={Stone duality above dimension zero: Axiomatising the algebraic theory of {C(X)}},
+ volume={307},
+ ISSN={0001-8708},
+ url={http://dx.doi.org/10.1016/j.aim.2016.11.012},
+ DOI={10.1016/j.aim.2016.11.012},
+ journal={Advances in Mathematics},
+ publisher={Elsevier BV},
+ author={Marra, Vincenzo and Reggio, Luca},
+ year={2017},
+ month=Feb, pages={253–287} }
+@article{Isb82,
+ title = {Generating the algebraic theory of {C(X)}},
+ journal = {Algebra Universalis},
+ volume = {15 (2)},
+ pages = {153-155},
+ year = {1982},
+ author = {Isbell, J.R.}
+}
+@inproceedings{Dus69,
+ title = {Variations on {B}eck's tripleability criterion},
+ series = {Reports of the Midwest Category Seminar III},
+ editor = {MacLane, S.},
+ author = {Duskin, J.},
+ pages = {74-129},
+ year = {1969},
+ publisher = {Springer Berlin Heidelberg}
+}
+@article{Hoff18,
+ title = {Generating the algebraic theory of {C(X)}: The case of partially ordered compact spaces},
+ journal = {Theory and Applications of Categories},
+ author = {Hoffman, Dirk and Neves, Renato and Nora, Pedro},
+ pages = {276-295},
+ year = {2018},
+ volume = {33},
+ number = {12},
+ url = {http://www.tac.mta.ca/tac/volumes/33/12/33-12.pdf}}
+@article{GU71,
+ title = {Lokal pr\"asentierbare {K}ategorien},
+ author = {P. Gabriel and F. Ulmer},
+ journal = {Lecture Notes in Mathematics},
+ publisher = {Springer-Verlag, Berlin},
+ volume = {221},
+ year = {1971}
+}
+@book{SGL,
+ title={Sheaves in Geometry and Logic: A First Introduction to Topos Theory},
+ author={Mac Lane, Saunders and Moerdijk, Ieke},
+ year={1992},
+ publisher={Springer-Verlag New York, Inc.},
+ series={Universitext},
+ isbn={978-0-387-97710-2},
+ doi={10.1007/978-1-4612-0927-0},
+ url={https://link.springer.com/book/10.1007/978-1-4612-0927-0}
+}
diff --git a/static/pdf/comphaus_copresentable.pdf b/static/pdf/comphaus_copresentable.pdf
new file mode 100644
index 000000000..96c164894
Binary files /dev/null and b/static/pdf/comphaus_copresentable.pdf differ
diff --git a/static/pdf/comphaus_copresentable.tex b/static/pdf/comphaus_copresentable.tex
new file mode 100644
index 000000000..ed589d725
--- /dev/null
+++ b/static/pdf/comphaus_copresentable.tex
@@ -0,0 +1,118 @@
+\documentclass[a4paper,12pt,reqno]{amsart}
+\usepackage[utf8]{inputenc}
+\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry}
+
+\usepackage{amsmath, amssymb, amsfonts, amscd, amsthm, mathtools, hyperref, doi}
+\usepackage[numbers]{natbib}
+\newtheorem{proposition}{Proposition}
+\newtheorem{lemma}[proposition]{Lemma}
+\newtheorem{corollary}[proposition]{Corollary}
+
+\newcommand{\Hom}{\operatorname{Hom}}
+\newcommand{\Mor}{\operatorname{Mor}}
+\newcommand{\op}{\operatorname{op}}
+\newcommand{\CompHaus}{\mathbf{CompHaus}}
+\newcommand{\Set}{\mathbf{Set}}
+\newcommand{\im}{\operatorname{im}}
+\newcommand{\id}{\operatorname{id}}
+\newcommand{\I}{\mathcal{I}}
+\newcommand{\calT}{\mathcal{T}}
+\newcommand{\INnz}{\mathbb{N}_{>0}}
+\newcommand{\colim}{\operatorname{colim}}
+
+\title{Local $\aleph_1$-copresentability of the category of compact Hausdorff spaces}
+\author{Daniel Schepler}
+\date{\today}
+
+\begin{document}
+\maketitle
+
+Our purpose here is to gather several relevant results about the category $\CompHaus$ of compact Hausdorff spaces, and provide accessible (sic) proofs of these facts leading up to a proof that it is locally $\aleph_1$-copresentable.
+
+A good overview of some of these results is contained in the introduction of \cite{Hoff18}.
+
+We first prove a couple preliminary results.
+
+\begin{lemma}
+ Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltered diagram in which $X_i$ is non-empty for each $i\in \I$. Then $\lim_i X_i$ is also non-empty.
+
+ \begin{proof}
+ Consider the product space $\prod_{i\in \I} X_i$. Now for each morphism $f : i \to j$ in $\I$, define the subset
+ $$\textstyle E_f := \bigl\{ x \in \prod_{i \in \I} X_i \mid X_f(x_i) = x_j \bigr\}.$$
+ Then each $E_f$ is a closed subset.
+
+ Next, we prove that the collection $\{ E_f : f \in \Mor(\I) \}$ has the finite intersection property, i.e. that $\bigcap_{f\in F} E_f$ is non-empty for every finite set $F \subseteq \Mor(\I)$. For $f\in F$ we write $f : i_f \to j_f$. Then the diagram with objects $J := \{ i_f \mid f \in F \} \cup \{ j_f \mid f \in F \}$ and morphisms $\{ f \mid f \in F \}$ has a cone with vertex $k \in \I$ and morphisms $g_i : k \to i$ for each $i \in J$. Now choose $y \in X_k$, and define $x \in \prod_{i \in \I} X_i$ such that $x_i = X_{g_i}(y)$ if $i \in J$, with arbitrary choices of $x_i \in X_i$ for all other $i$. We then see that $x \in \bigcap_{f\in F} E_f$, which finishes the proof of the claim.
+
+ Since $\prod_{i \in \I} X_i$ is compact, that implies that the intersection of all $E_f$ is non-empty. But that intersection is precisely $\lim_{i \in \I} X_i$.
+ \end{proof}
+\end{lemma}
+
+\begin{lemma}
+ Suppose we have a cofiltered limit $X = \lim_{i\in \I} X_i$ in $\mathbf{Top}$. Note the topology on $X$ is the weak topology for the projections $p_i : X \to X_i$. Then the canonical subbasis of this topology on $X$ is closed under finite intersections. Thus, it agrees with the canonical basis of the topology on $X$.
+
+ \begin{proof}
+ Suppose we have a finite collection of subbasic open sets of the form $U_n = p_{i_n}^{-1}(V_n)$, $n \in \{ 1, \ldots, N \}$, where each $V_n$ is an open subset of $X_{i_n}$. Take a cone $(j, f_n : j \to i_n)$ of the objects $i_1, \ldots, i_N$. We then have
+ $$\bigcap_{n=1}^N U_n = p_j^{-1} \left( \bigcap_{n=1}^N X_{f_n}^{-1}(V_n) \right),$$
+ where the right hand side is again in the canonical subbasis.
+ \end{proof}
+\end{lemma}
+
+\begin{proposition}
+ The functor $\Hom({-}, [0, 1]) : \CompHaus^{\op} \to \Set$ is monadic. (Originally proved in \cite{Dus69})
+
+ \begin{proof}
+ We use the crude monadicity theorem (see e.g.~\cite{SGL}, Thm.~IV.4.2). First, the functor has a left adjoint $S \mapsto [0, 1]^S$ with the evident isomorphism
+ $$\Hom_{\CompHaus}(X, [0, 1]^S) \simeq \Hom_{\Set}(S, \Hom_{\CompHaus}(X, [0, 1])). $$
+
+ To see the functor is conservative, suppose we have a continuous function $f : X \to Y$ such that $f^* : \Hom(Y, [0, 1]) \to \Hom(X, [0, 1])$ is a bijection. Then for any $x_1, x_2 \in X$ with $x_1 \ne x_2$, there exists $\varphi : X \to [0, 1]$ with $\varphi(x_1) = 0$ and $\varphi(x_2) = 1$ by Urysohn's lemma. Since $f^*$ is surjective, there exists $\psi : Y \to [0, 1]$ with $\varphi = \psi \circ f$; thus, we must have $f(x_1) \ne f(x_2)$. Likewise, we know the image of $f$ is closed. If this image is not all of $Y$, then by Urysohn's lemma there exists nonzero $\varphi : Y \to [0, 1]$ which is zero on the image. But then $\varphi \circ f = 0 \circ f$, contradicting the injectivity of $f^*$. Thus, $f$ is a bijective continuous function, and therefore a homeomorphism.
+
+ Finally, suppose we have a coreflexive equalizer pair
+ $$E \xhookrightarrow{i} A \overset{f}{\underset{g}{\rightrightarrows}} B$$
+ with $r : B \to A$. We may assume that $i$ is a subspace inclusion map. We may use $r$ to think of $B$ as a bundle of compact spaces over $A$, with two sections $f, g$. We then need to show that
+ $$\Hom(B, [0,1])) \overset{f^*}{\underset{g^*}{\rightrightarrows}} \Hom(A, [0, 1]) \xrightarrow{i^*} \Hom(E, [0, 1])$$
+ is a coequalizer diagram. We first define $s : \Hom(E,[0,1]) \to \Hom(A,[0,1])$ by choosing a Tietze extension of each continuous function $E \to [0,1]$. Now, for each $\varphi \in \Hom(A,[0,1])$, we can define a continuous function on $\im(f) \cup \im(g) \subseteq B$ to be $\varphi \circ r$ on $\im(f)$, and $s(i^*(\varphi))\circ r$ on $\im(g)$. Note that on the overlap $\im(f)\cap \im(g) = f(E) = g(E)$, the first expression gives $f(e) \mapsto \varphi(e)$, and the second expression gives $g(e) \mapsto s(i^*(\varphi))(e) = \varphi(e)$, so we have indeed given a well-defined function on $\im(f)\cup\im(g)$. Choosing a Tietze extension of this function to a function $B\to [0,1]$ for each $\varphi$, we get a map $t : \Hom(A,[0,1]) \to \Hom(B,[0,1])$. By construction, we have $i^* s = \id$, $f^* t = \id$, and $g^* t = s i^*$, so we have shown that the diagram above is a split coequalizer.
+ \end{proof}
+\end{proposition}
+
+This shows that $\CompHaus^{\op}$ is equivalent to the category of algebras over the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$. We may view such algebras as being models of the infinitary algebraic theory of all continuous functions $[0,1]^S \to [0,1]$. In fact, we can show that any such function only depends on countably many coordinates in the domain, so that operations of this theory will be generated by the continuous functions $[0,1]^\omega \to [0,1]$. Indeed, we get the following somewhat stronger result:
+
+\begin{proposition}
+ The object $[0,1]$ of $\CompHaus$ is $\aleph_1$-copresentable. (Originally proved in \cite{GU71}, 6.5(c))
+
+ \begin{proof}
+ Suppose we have an $\aleph_1$-cofiltered limit $X = \lim_{i\in \I} X_i$ with projections $p_i : X \to X_i$, and a continuous function $\varphi : X \to [0,1]$. For the time being, fix $n\in \INnz$. Then for any $x\in X$, there exists an interval neighborhood $N_x$ of $\varphi(x)$ of diameter at most $1/n$ --- for example, we can take $N_x := (\varphi(x) - 1/(2n), \varphi(x) + 1/(2n)) \cap [0,1]$. We can also take a basic open neighborhood whose image is contained in $N_x$; by lemma 2, we can write that basic open neighborhood in the form $p_i^{-1}(V)$ where $V$ is an open subset of $X_i$.
+
+ By compactness of $X$, we may take finitely many such basic open neighborhoods of the form $p_i^{-1}(V)$ which cover $X$. Again using the assumption that $\I$ is cofiltered, we may assume that $i$ is the same for each neighborhood. In particular, we see that whenever we have $x, y\in X$ with $p_i(x) = p_i(y)$, then $|\varphi(x) - \varphi(y)| < 1/n$.
+
+ To summarize, we have shown that for each $n \in \INnz$, there exists $i \in \I$ and a finite cover $\{ V_\lambda \mid \lambda \in \Lambda \}$ of $\im(p_i)$ such that whenever $p_i(x), p_i(y) \in V_\lambda$ for some $\lambda$, we have $|\varphi(x) - \varphi(y)| < 1/n$. Now choose such a $i_n$ and associated finite cover of $\im(p_{i_n})$ for each $n$. Then use the fact that $\I$ is $\aleph_1$-cofiltered to take a cone $(j, f_n : j \to i_n)$ of the objects $i_n$. We then see that whenever we have $x, y\in X$ with $p_j(x) = p_j(y)$, then $\varphi(x) = \varphi(y)$. Thus, $\varphi$ induces a well-defined function on the image of $p_j$. This function is continuous, since by construction for any $n\in \INnz$ and $x \in X$, there is a neighborhood $V$ of $p_j(x)$ such that whenever $p_j(y)\in V$ as well, $|\varphi(y) - \varphi(x)| < 1/n$. By the Tietze extension theorem, this induced function can then be extended to a continuous function $\psi : X_j \to [0,1]$. Then $\varphi = \psi \circ p_j$.
+
+ This shows the canonical map
+ $$\colim_{i\in \I^{\op}} \Hom(X_i, [0,1]) \to \Hom(\lim_{i\in \I} X_i, [0,1])$$
+ is surjective.
+
+ Likewise, suppose we have $\alpha, \beta : X_i \rightrightarrows [0,1]$ such that $\alpha \circ p_i = \beta \circ p_i$. For each $n\in \INnz$, consider the set $D_n := \{ x \in X_i \mid |\alpha(x) - \beta(x)| \ge 1/n \}$. Note that $D_n$ is a closed subset of $X_i$, so it is compact. For any $x \in D_n$, we must have $x \notin \im(p_i)$. Using the contrapositive of lemma 1, we can conclude that there exists $f : j \to i$ such that $x \not\in \im(X_f)$. Indeed, suppose not: then the slice category $\I / i$ is cofiltered, with the limit over this slice category being the same as the limit over $\I$. Also, by the contrary assumption, we have that $x \in \im(X_f)$ for any $f : j \to i$, so $X_f^{-1}(\{ x \})$ is non-empty. Therefore, by lemma 1, the limit $p_i^{-1}(\{ x \})$ would be non-empty, contradicting the assumption.
+
+ Now each $D_n \setminus \im(X_f)$ is open and we have just shown such sets cover $D_n$; taking a finite subcover and then using the cofiltering assumption again, we conclude that there is a single $f_n : j_n \to i$ such that $\im(X_{f_n})$ is disjoint from $D_n$. Using the $\aleph_1$-cofiltering assumption to take a cone of the $f_n$, we get that there is $f : k \to i$ such that $\im(X_f)$ is disjoint from all $D_n$. This implies that $\alpha \circ X_f = \beta \circ X_f$.
+
+ This shows the canonical map
+ $$\colim_{i\in \I^{\op}} \Hom(X_i, [0,1])) \to \Hom(\lim_{i\in I} X_i, [0,1])$$
+ is injective.
+ \end{proof}
+\end{proposition}
+
+\begin{corollary}
+ The category $\CompHaus$ is locally $\aleph_1$-copresentable.
+
+ \begin{proof}
+ It suffices to show that the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$ is $\aleph_1$-accessible. This monad is the composition of $[0, 1]^{-} : \Set \to \CompHaus^{\op}$ followed by $\Hom_{\CompHaus}({-}, [0,1]) : \CompHaus^{\op} \to \Set$. The first automatically preserves $\aleph_1$-filtered colimits (and in fact all colimits) since it has a right adjoint. The second one preserves $\aleph_1$-filtered colimits by the previous lemma.
+
+ Alternately, applying the general framework of Lawvere theories shows that $\CompHaus^{\op}$ is equivalent to the category of functors $\calT \to \Set$ preserving countable products, where $\calT$ is the full subcategory of $\CompHaus$ of all spaces $[0,1]^A$ where $A$ is countable. Note that $\calT$ is essentially small. We thus reproduce a result from \cite{Isb82} which also provides a nice description of a small set of generators of the operations of the $\aleph_0$-ary algebraic theory. A more recent treatment in \cite{Marra_2017} refines this by providing a nice axiomatization of the relations of that theory.
+ \end{proof}
+\end{corollary}
+
+\nocite{marra2020characterisationcategorycompacthausdorff}
+\nocite{HUSEK2019251}
+\bibliographystyle{plainnat}
+\bibliography{comphaus_copresentable}
+
+\end{document}