topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
vector bundle, 2-vector bundle, (∞,1)-vector bundle
real, complex/holomorphic, quaternionic
A covering space (or wrapping space) is a bundle $p: E \to B$ in which is locally trivial and with discrete fiber.
A continuous function $p: E \to B$ is a covering space over $B$ if for each point $x \in B$, there exists an open neighborhood $U$ of $x$ which is evenly covered by $p$ in that the pullback of $p$ over $U$ is isomorphic to a product bundle with discrete fiber $E_x = p^{-1}(x)$:
(the square is a pullback and the isomorphism maps $(x, e \in E_x) \mapsto e$).
Covering spaces over $B$ form an evident full subcategory $Cov/B \hookrightarrow Top/B$ of the slice category of Top over $B$, the category of covering spaces. These may be put together to form a replete, wide subcategory $Cov$ of $Top$, so that $Cov/B$ is an over category, just as the notation suggests.
Different points in $B$ may have non-isomorphic fibers. However, if open sets $U$ and $V$ are evenly covered by $p: E \to B$ and have nonempty intersection, then there are canonical identifications
between typical fibers over $x \in U$, $y \in V$, and $z \in U \cap V$. If $B$ is path-connected, then all the fibers match up to isomorphism (by the unique path-lifting lemma (lemma below)).
Fibers of a covering space may be empty. Some authors choose to forbid that, adding the condition that $p$ be a surjection, but the resulting category of covering projections over a space $B$ is not as nice as it would be without that condition.
The terms “covering space” and “covering projection”, while traditional, are certainly not optimal: they mislead by being too close to (open) “coverings”. James Dolan has suggested “wrapping space” as an alternative (as in the image of thread wrapping around a spool, to evoke the archetypal example of a covering projection, $p: \mathbb{R} \to S^1: x \mapsto \exp(i x)$).
There is a generalization to “semi-coverings” (Brazas12). Semicoverings satisfy the “2 out of 3 rule”. I.e,, if $f=g h$ and two of $f,g,h$ are semicoverings , then so is the third. This is not true for covering maps.
(covering projections are open maps)
If $p \colon E \to X$ is a covering space projection, then $p$ is an open map.
By definition of covering space there exists an open cover $\{U_i \subset X\}_{i \in I}$ and homeomorphisms $p^{-1}(U_i) \simeq U_i \times Disc(F_i)$ for all $i \in I$. Since the projections out of a product topological space are open maps (this prop.), it follows that $p$ is an open map when restricted to any of the $p^{-1}(U_i)$. But a general open subset $W \subset E$ is the union of its restrictions to these subspaces:
Since images preserve unions (this prop.) it follows that
is a union of open sets, and hence itself open.
(fiber-wise diagonal of covering space is open and closed)
Let $E \overset{p}{\to} X$ be a covering space. Consider the fiber product
hence (by the discussion at Top - Univeral constructions) the topological subspace of the product space $E \times E$, as shown on the right. By the universal property of the fiber product, there is the diagonal continuous function
Then the image of $E$ under this function is an open subset and a closed subset:
First to see that it is an open subset. It is sufficient to show that for any $e \in E$ there exists an open neighbourhood of $(e,e) \in E \times_X E$.
Now by definition of covering spaces, there exists an open neighbourhood $U_{p(e)} \subset X$ of $p(e) \in X$ such that
It follows that $U_{p(e)} \times \{e\} \subset E$ is an open neighbourhood. Hence by the nature of the product topology, $U_{p(e)} \times U_{p(e)} \subset E \times E$ is an open neighbourhood of $(e,e)$ in $E \times E$ and hence by the nature of the subspace topology the restriction
is an open neighbourhood of $(e,e)$ in $E \times_X E$.
Now to see that the diagonal is closed, hence that the complement $(E \times_X E) \setminus \Delta(E)$ is an open subset, it is sufficient to show that every point $(e_1, e_2)$ with $e_1 \neq e_2$ but $p(e_1) = p(e_2)$ has an open neighbourhood in this complement.
As before, there is an open neighbourhood $U \subset X$ of $p(e_1) = p(e_2)$ over which the cover trivializes, and hence $U \times \{e_1\}, U \times \{e_2\} \subset E$ are open neighbourhoods of $e_1$ and $e_2$, respectively. These are disjoint by the assumption that $e_1 \neq e_2$. As above, this means that the intersection
is an open subset of the complement of the diagonal in the fiber product.
Every covering space (even in the more general sense not requiring any connectedness axiom) is an etale space, but not vice versa:
for a covering space the inverse image of some open set in the base $B$ needs to be, by the definition, a disjoint union of homeomorphic open sets in $E$; however the ‘size’ of the neighborhoods over various $e$ in the same stalk required in the definition of étalé space may differ, hence the intersection of their projections does not need to be an open set, if there are infinitely many points in the stalk.
even if the stalks of the etale space are finite, it need not be locally trivial. For instance the disjoint union $\coprod_i Ui$ of a collection of open subsets of a space $X$ with the obvious projection $(\coprod_i U_i) \to X$ is etale, but does not have a typical fiber: the fiber over a given point has cardinality the number of open sets $U_i$ that contain this particular point.
We discuss left lifting properties satisfied by covering spaces.
(lifts out of connected space into covering spaces are unique relative to any point)
Let
$E \overset{p}{\to} X$ be a covering space,
$f \;\colon\; Y \longrightarrow X$ a continuous function.
$\hat f_1, \hat f_2 \;\colon\; Y \longrightarrow E$ two lifts of $f$, in that the following diagram commutes:
for $i \in \{1,2\}$.
If there exists $y \in Y$ such that $\hat f_1(y) = \hat f_2(y)$ then the two lifts already agree everywhere: $\hat f_1 = \hat f_2$.
By the universal property of the fiber product
the two lifts determine a single continuous function of the form
Write
for the diagonal on $E$ in the fiber product. By lemma this is an open subset and a closed subset of the fiber product space. Hence by continuity of $(\hat f_1, \hat f_2)$ also its pre-image
is both closed and open, hence also its complement is open in $Y$.
Moreover, the assumption that the functions $\hat f_1$ and $\hat f_2$ agree in at least one point means that the above pre-image is non-empty. Therefore the assumption that $Y$ is connected implies that this pre-image coincides with all of $Y$. This is the statement to be proven.
(path lifting property)
Let $p \colon E \to X$ be any covering space. Given
$\gamma \colon [0,1] \to X$ a path in $X$,
$\hat x_0 \in E$ be a lift of its starting point, hence such that $p(\hat x_0) = \gamma(0)$
then there exists a unique path $\hat \gamma \colon [0,1] \to E$ such that
it is a lift of the original path: $p \circ \hat \gamma = \gamma$;
it starts at the given lifted point: $\hat \gamma(0) = \hat x_0$.
In other words, every commuting diagram in Top of the form
has a unique lift:
First consider the case that the covering space is trival, hence of the Cartesian product form
By the universal property of the product topological spaces in this case a lift $\hat \gamma \colon [0,1] \to X \times Disc(S)$ is equivalently a pair of continuous functions
Now the lifting condition explicitly fixes $pr_1(\hat \gamma) = \gamma$. Moreover, a continuous function into a discrete topological space $Disc(S)$ is locally constant, and since $[0,1]$ is a connected topological space this means that $pr_2(\hat \gamma)$ is in fact a constant function (this example), hence uniquely fixed to be $pr_2(\hat \gamma) = \hat x_0$.
This shows the statement for the case of trivial covering spaces.
Now consider any covering space $p \colon E \to X$. By definition of covering spaces, there exists for every point $x \in X$ a open neighbourhood $U_x \subset X$ such that the restriction of $E$ to $U_x$ becomes a trivial covering space:
Consider such a choice
This is an open cover of $X$. Accordingly, the pre-images
constitute an open cover of the topological interval $[0,1]$.
Now the closed interval is a compact topological space, so that this cover has a finite open subcover. By the Euclidean metric topology, each element in this finite subcover is a disjoint union of open intervals. The collection of all these open intervals is an open refinement of the original cover, and by compactness it once more has a finite subcover, now such that each element of the subcover is guaranteed to be a single open interval.
This means that we find a finite number of points
with $t_0 = 0$ and $t_{n+1} = 1$ such that for all $0 \lt j \leq n$ there is $x_j \in X$ such that the corresponding path segment
is contained in $U_{x_j}$ from above.
Now assume that $\hat \gamma\vert_{[0,t_j]}$ has been found. Then by the triviality of the covering space over $U_{x_j}$ and the first argument above, there is a unique lift of $\gamma\vert_{[t_j, t_{j+1}]}$ to a continuous function $\hat \gamma|_{[t_j,t_{j+1}]}$ with starting point $\hat \gamma(t_j)$. Since $[0,t_{j+1}]$ is the pushout $[0,t_j] \underset{\{t_j\}}{\sqcup} [t_j,t_{j+1}]$ (this example), it follows that $\hat \gamma|_{[0,t_j]}$ and $\hat \gamma\vert_{[t_j,t_{j+1}]}$ uniquely glue to a continuous function $\hat \gamma\vert_{[0,t_{j+1}]}$ which lifts $\gamma\vert_{[0,t_{j+1}]}$.
By induction over $j$, this yields the required lift $\hat \gamma$.
Conversely, given any lift, $\hat \gamma$, then its restrictions $\hat \gamma\vert_{[t_j, t_{j+1}]}$ are uniquely fixed by the above inductive argument. Therefore also the total lift is unique. Altrnatively, uniqueness of the lifts is a special case of lemma .
(homotopy lifting property of covering spaces against locally connected spaces)
Let
$E \overset{p}{\to} X$ be a covering space;
$Y$ a topological space.
Then every lifting problem of the form
has a unique lift
Let $\{U_i \subset X\}_{i \in I}$ be an open cover over which the covering space trivializes. Then the pre-images $\{\eta^{-1}(U_i) \subset Y \times [0,1]\}_{i \in I}$ is an open cover of the product space. By nature of the product space topology and the Euclidean topology on $[0,1]$, each of the $\eta^{-1}(U_i)$ is a union of Cartesian products $V_j \times I_j$ with $V_i \subset Y$ an open subset of $Y$ and $I_i \subset [0,1]$ an interval. Hence there is an open cover of the form
with the property that for each $j$ there exists $i \in I$ with $\eta(V_j \times I_j) \subset U_i$.
Now by the fact that $[0,1]$ is a compact topological space, for each $y \in Y$ there exists a finite set $K_y \subset J$ such that
still restricts to a cover of $\{y\} \times [I]$. Since $K$ is finite, the intersection
is still open, and so also
still restricts to a cover of $\{y\} \times [0,1]$.
This means that the same argument as for the path lifting in lemma provides a unique lift $\widehat{\eta\vert_{V_y \times [0,1]}}$ for each $y \in Y$.
Moreover, for $y_1, y_2 \in Y$ two points, these lifts clearly have to agree on $V_{y_1} \cap V_{y_2}$.
Since $\{V_y \times [0,1] \subset Y \times [0,1]\}_{y \in Y}$ is an open cover, means that there is a unique function $\hat \eta$ that restricts to all these local lifts (this prop). This is the required lift.
(covering spaces are Hurewicz fibrations)
Continuous functions with the right lifting property against functions of the form $Y \overset{(id,const_0)}{\longrightarrow} Y \times [0,1]$ are called Hurewicz fibrations.
Hence prop. says that covering projections are in particular Hurewicz fibrations.
(lift homotopy of paths for given lifts of paths)
Let $p \colon E \to X$ be a covering space. Then given a homotopy relative the starting point between two paths in $X$,
there is for every lift $\hat \gamma_1, \hat \gamma_2$ of these two paths to paths in $E$ with the same starting point a unique homotopy
between the lifted paths that lifts the given homotopy:
For commuting squares of the form
there is a unique diagonal lift in the lower diagram, as shown.
Moreover if the homotopy $\eta$ also fixes the endpoint, then so does the lifted homotopy $\hat \eta$.
There are horizontal homeomorphisms such that the following diagram commutes
Let $(E,e) \overset{p}{\longrightarrow} (X,x)$ be a pointed covering space and let $f \colon (Y,y) \longrightarrow (X,x)$ be a point-preserving continuous function such that the image of the fundamental group of $(Y,y)$ is contained within the image of the fundamental group of $(E,e)$ in that of $(X,x)$:
Then for $\ell_Y$ a path in $(Y,y)$ that happens to be a loop, every lift of its image path $f \circ \ell$ in $(X,x)$ to a path $\widehat{f\circ \ell_Y}$ in $(E,e)$ is also a loop there.
By assumption, there is a loop $\ell_E$ in $(E,e)$ and a homotopy fixing the endpoints of the form
Then by the homotopy lifting property as in example , there is a homotopy in $(E,e)$ fixing the starting point, of the form
and lifting the homotopy $\eta_X$. Since $\eta_X$ in addition fixes the endpoint, the uniqueness of the path lifting (lemma ) implies that also $\eta_{E}$ fixes the endpoint. Therefore $\eta_E$ is in fact a homotopy between loops, and so $\widehat{f \circ \ell_Y}$ is indeed a loop.
(lifting theorem)
Let
$p \colon E \to X$ be a covering space;
$e \in E$ a point, with $x \coloneqq p(e)$ denoting its image,
$Y$ be a connected and locally path-connected topological space;
$y \in Y$ a point
$f \colon (Y,y) \longrightarrow (X,x)$ a continuous function such that $f(y) = x$.
Then the following are equivalent:
There exists a unique lift $\hat f$ in the diagram
The image of the fundamental group of $Y$ under $f$ in that of $X$ is contained in the image of the fundamental group of $E$ under $p$:
Moreover, if $Y$ is path-connected, then the lift in the first item is unique.
The implication $1) \Rightarrow 2)$ is immediate. We need to show that the second statement already implies the first.
Since $Y$ is connected and locally path-connected, it is also a path-connected topological space (this prop.). Hence for every point $y' \in Y$ there exists a path $\gamma$ connecting $y$ with $y'$ and hence a path $f \circ \gamma$ connecting $x$ with $f(y')$. By the path-lifting property (lemma ) this has a unique lift
Therefore
is a lift of $f(y')$.
We claim now that this pointwise construction is independent of the choice $\gamma$, and that as a function of $y'$ it is indeed continuous. This will prove the claim.
Now by the path lifting lemma the lift $\widehat{\f \circ \gamma}$ is unique given $f \circ \gamma$, and hence $\hat f(y')$ depends at most on the choice of $\gamma$.
Hence let $\gamma' \colon [0,1] \to Y$ be another path in $Y$ that connects $y$ with $y'$. We need to show that then $\widehat{f \circ \gamma'} = \widehat{f \circ \gamma}$.
First observe that if $\gamma'$ is related to $\gamma$ by a homotopy, so that then also $f \circ \gamma'$ is related to $f \circ \gamma$ by a homotopy, then this is the statement of the homotopy lifting property as in example .
Next write $\bar\gamma'\cdot \gamma$ for the path concatenation of the path $\gamma$ with the reverse path of the path $\gamma'$, hence a loop in $Y$, so that $f \circ (\bar\gamma'\cdot \gamma)$ is a loop in $X$. The assumption that $f_\ast(\pi_1(Y,y)) \subset p_\ast(\pi_1(E,e))$ implies (example ) that the path $\widehat{f \circ (\bar \gamma' \cdot \gamma)}$ which lifts this loop to $E$ is itself a loop in $E$.
By uniqueness of path lifting, this means that the lift of
coincides at $1 \in [0,1]$ with that of $f \circ \gamma'$ at 1. But $\gamma' \cdot (\bar \gamma' \cdot \gamma)$ is homotopic (via reparameterization) to just $\gamma$. Hence it follows now with the first statement that the lift of $f \circ \gamma'$ indeed coincides with that of $f \circ \gamma$.
This shows that the above prescription for $\hat f$ is well defined.
It only remains to show that the function $\hat f$ obtained this way is continuous.
Let $y' \in Y$ be a point and $W_{\hat f(y')} \subset E$ an open neighbourhood of its image in $E$. It is sufficient to see that there is an open neighbourhood $V_{y'} \subset Y$ such that $\hat f(V_y) \subset W_{\hat f(y')}$.
Let $U_{f(y')} \subset X$ be an open neighbourhood over which $p$ trivializes. Then the restriction
is an open subset of the product space. Consider its further restriction
to the leaf
which is itself an open subset. Since $p$ is an open map (this prop.), the subset
is open, hence so is its pre-image
Since $Y$ is assumed to be locally path-connected, there exists a path-connected open neighbourhood
By the uniqueness of pah lifting, the image of that under $\hat f$ is
This shows that the lifted function is continuous. Finally that this continuous lift is unique is the statement of lemma .
(monodromy of a covering space)
Let $X$ be a topological space and $E \overset{p}{\to} X$ a covering space. Write $\Pi_1(X)$ for the fundamental groupoid of $X$.
Define a functor
to the category Set of sets as follows:
to a point $x \in X$ assign the fiber $p^{-1}(\{x\}) \in Set$;
to the homotopy class of a path $\gamma$ connecting $x \coloneqq \gamma(0)$ with $y \coloneqq \gamma(1)$ in $X$ assign the function $p^{-1}(\{x\}) \longrightarrow p^{-1}(\{y\})$ which takes $\hat x \in p^{-1}(\{x\})$ to the endpoint of a path $\hat \gamma$ in $E$ which lifts $\gamma$ through $p$ with starting point $\hat \gamma(0) = \hat x$
This construction is well defined for a given representative $\gamma$ due to the unique path-lifting property of covering spaces (this lemma) and it is independent of the choice of $\gamma$ in the given homotopy class of paths due to the homotopy-lifting property (this lemma). Similarly, these two lifting properties give that this construction respects composition in $\Pi_1(X)$ and hence is indeed a functor.
Given a homomorphism between two covering spaces $E_i \overset{p_i}{\to} X$, hence a continuous function $f \colon E_1 \to E_2$ which respects fibers in that the diagram
commutes, then the component functions
are compatible with the monodromy $Fib_{E}$ (def. ) along any path $\gamma$ between points $x$ and $y$ from def. in that the following diagrams of sets commute
This means that $f$ induces a natural transformation between the monodromy functors of $E_1$ and $E_2$, respectively, and hence that constructing monodromy is itself a functor from the category of covering spaces of $X$ to that of permutation representations of the fundamental groupoid of $X$:
(fundamental groupoid of covering space)
Let $E \overset{p}{\longrightarrow} X$ be a covering space.
Then the fundamental groupoid $\Pi_1(E)$ of the total space $E$ is equivalently the Grothendieck construction of the monodromy functor $Fib_E \;\colon\; \Pi_1(X) \to Set$
whose
By the uniqueness of the path-lifting, lemma and the very definition of the monodromy functor.
Let $X$ be a path-connected topological space and let $E \overset{p}{\to} X$ be a covering space. Then the total space $E$ is
path-connected precisely if the monodromy $Fib_E$ is a transitive action;
simply connected precisely if the monodromy $Fib_E$ is a transitive and free action.
Given a permutation representation of the fundamental groupoid of a locally path-connected and semi-locally simply connected space, there is a construction of reconstructing covering spaces from monodromy, which is a functor of the form
(fundamental theorem of covering spaces)
Let $X$ be a locally path-connected and semi-locally simply-connected topological space. Then the operations on
extracting the monodromy $Fib_{E}$ of a covering space $E$ over $X$
constitute an adjoint equivalence of categories
between the category of covering spaces and the permutation groupoid representations of the fundamental groupoid of $X$.
(trivial covering space)
For $X$ a topological space and $S$ a set with $Disc(S)$ the discrete topological space on that set, then the projection out of the product topological space
is a covering space, called the trivial covering space over $X$ with fiber $Disc(S)$.
If $E \overset{p}{\longrightarrow} X$ is any covering space, then an isomorphism of covering spaces of the form
is called a trivialization of $E \overset{p}{\to} X$.
It is in this sense that evry coverin space $E$ is, by definition, locally trvializable.
(n-sphere covering over real projective space)
For $n \in \mathbb{N}$ the canonical projection
from the n-sphere to the real projective space of dimension $n$ is a covering space projection. See this prop..
We want to describe here how the universal covering space of $X$ is the homotopy fiber of the canonical morphism $X \to \Pi_1(X)$, hence the $\Pi_1(X)$-principal bundle classified by this cocycle.
We place ourselves in the context of topological ∞-groupoids and regard both the space $X$ as well as its path ∞-groupoid $\Pi(X)$ and its truncation to the fundamental groupoid $\Pi_1(X)$ as objects in there.
The canonical morphism $X \to \Pi(X)$ hence $X \to \Pi_1(X)$ given by the inclusion of contant paths may be regarded as a cocycle for a $\Pi(X)$-principal ∞-bundle, respectively for a $\Pi_1(X)$-principal bundle.
Let $\pi_0(X)$ be the set of connected components of $X$, regarded as a topological $\infty$-groupoid, and choose any section $\pi_0(X) \to \Pi(X)$ of the projection $\Pi(X) \to \pi_0(X)$.
Then the $\Pi(X)$-principal $\infty$-bundle classified by the cocycle $X \to \Pi(X)$ is its homotopy fiber, i.e. the homotopy pullback
We think of this topological $\infty$-groupoid $UCov(X)$ as the universal covering $\infty$-groupoid of $X$. To break this down, we check that its decategorification gives the ordinary universal covering space:
for this we compute the homotopy pullback
where we assume $X$ to be connected with chosen baspoint $x$ just to shorten the exposition a little. By the laws of homotopy pullbacks in general and homotopy fibers in particular, we may compute this as the ordinary pullback of a weakly equivalent diagram, where the point $*$ is resolved to the universal $\Pi_1(X)$-principal bundle
(More in detail, what we do behind the scenes is this: we regard the diagram as a diagram in the global model structure on simplicial presheaves on Top. In there all our topological groupoids are fibrant, hence all we have to ensure is that one of the morphisms of the diagram becomes a fibration, which is what the passage to $\mathbf{E}_x \Pi_1(X)$ achieves. Then the ordinary pullback in the category of simplicial presheaves is the homotopy pullback in $\infty$-prestacks. Then by left exactness of $\infty$-stackification, the image of that in $\infty$-stacks is still a homotopy pullback. )
The topological groupoid $\mathbf{E}_x \Pi_1(X)$ has as objects homotopy classes rel endpoints of paths in $X$ starting at $x$ and as morphisms $\kappa : \gamma \to \gamma'$ it has commuting triangles
in $\Pi_1(X)$. The topology on this can be deduced from thinking of this as the pullback
in simplicial presheaves on Top. Unwinding what this means we find that the open sets in $Mor(\mathbf{E}_x \Pi_1(X))$ are those where the endpoint evaluation produces an open set in $X$.
Now it is immediate to read off the homotopy pullback as the ordinary pullback
Since $X$ is categorically discrete, this simply produces the space of objects of $\mathbf{E}_x \Pi_1(X)$ over the points of $X$, which is just the space of all paths in $X$ starting at $x$ with the projection $UCov_1(X) \to X$ being endpoint evaluation.
This indeed is then the usual construction of the universal covering space in terms of paths, as described for instance in (Dahlke)
A detailed treatment is available in
Textbook accounts:
William S. Massey, Chapter 5 of: Algebraic Topology: An Introduction, Harcourt Brace & World 1967, reprinted in: Graduate Texts in Mathematics, Springer 1977 (ISBN:978-0-387-90271-5)
Tammo tom Dieck, sections 2 an 3 of Algebraic Topology, EMS 2006 (pdf)
Review
Jesper Møller, The fundamental group and covering spaces (2011) (pdf)
Ronnie Brown, chapter 11 of Topology and Groupoids
Karl Dahlke, Covering spaces, Building a universal cover , Math Reference Project
Some of the problems of generalising covering spaces to deal with wild spaces are dealt with in:
Discussion of (homotopy types of) covering spaces via homotopy type theory:
Kuen-Bang Hou, Covering Spaces in Homotopy Type Theory, extended abstract Type Theory, Homotopy Theory and Univalent Foundations (2013) $[$doi:10.1007/978-3-319-21284-5_15$]$
Kuen-Bang Hou, Robert Harper, Covering Spaces in Homotopy Type Theory, Leibniz International Proceedings in Informatics (LIPIcs) 97 (2018) $[$doi:10.4230/LIPIcs.TYPES.2016.11, pdf$]$
and with emphasis on the $n$-truncation-modal homotopy type theory involved:
Last revised on November 17, 2023 at 21:47:05. See the history of this page for a list of all contributions to it.