Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-27T11:28:45.822Z Has data issue: false hasContentIssue false

The long exact sequence of homotopy n-groups

Published online by Cambridge University Press:  07 September 2023

Ulrik Buchholtz*
Affiliation:
Technische Universität Darmstadt, Fachbereich Mathematik, Schlossgartenstrasse 7, 64289 Darmstadt, Germany School of Computer Science, University of Nottingham, Jubilee Campus, Wollaton Road, Nottingham NG8 1BB, UK
Egbert Rijke
Affiliation:
University of Ljubljana, Fakulteta za matematiko in fiziko, Jadranska 19, 1000 Ljubljana, Slovenia
*
Corresponding author: Ulrik Buchholtz; Email: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Working in homotopy type theory, we introduce the notion of n-exactness for a short sequence $F\to E\to B$ of pointed types and show that any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ of arbitrary types induces a short sequence

that is n-exact at $\| E\|_{n-1}$. We explain how the indexing makes sense when interpreted in terms of n-groups, and we compare our definition to the existing definitions of an exact sequence of n-groups for $n=1,2$. As the main application, we obtain the long n-exact sequence of homotopy n-groups of a fiber sequence.

Type
Special Issue: Homotopy Type Theory 2019
Copyright
© The Author(s), 2023. Published by Cambridge University Press

1. Introduction

Homotopy type theory (Univalent Foundations Program 2013) is not only a foundational system (univalent foundations); but it also allows us to reason synthetically about $\infty$ -groupoids (synthetic homotopy theory). By viewing higher groups in terms of certain pointed $\infty$ -groupoids as laid out by Buchholtz et al. (Reference Buchholtz, van Doorn and Rijke2018), it also allows us to do synthetic higher group theory.

From this point of view, a 1-group G is (represented by) a pointed connected 1-type BG (its classifying type). Loosely speaking, these are types that only have an interesting fundamental group and no nontrivial higher homotopy groups. Of course, it is not quite as simple if there are noncontractible $\infty$ -connected types around, as can happen if Whitehead’s principle fails. Recall that homotopy type theory has models in $(\infty,1)$ -toposes (Shulman Reference Shulman2019, Thm. 11.2), Footnote 1 and there are plenty such where Whitehead’s principle fails. Footnote 2 The underlying type of a 1-group is therefore a set equipped with the usual structure of a group, so a group in the traditional sense of the word is a 1-group.

Likewise, an n-group G is represented by a connected n-type BG. The principal example of an n-group is the fundamental n-group of a pointed type X, represented by the n-truncation of the connected component at the base point.

Many n-groups G have further structure because they come with further deloopings of BG. The higher homotopy n-groups, $\pi^{(n)}_k(X)$ , of a pointed type X are examples of such n-groups with additional symmetries. These capture the structure of X in dimensions k to $n+k-1$ , inclusive, just like the usual higher homotopy 1-groups, $\pi_k(X)$ , capture the structure of X at dimension k. So, whereas the usual homotopy groups discard any interactions between different dimensions, the homotopy n-groups for $n>1$ retain some of that information, while still being more algebraically tractable than X itself.

Our main result in this paper is Theorem 5.5, where we show that any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ induces a long exact sequence of homotopy n-groups. The basic observation that enables this result is Proposition 5.4, in which we establish that the n-truncation operation – although it is not left exact – preserves k-cartesian squares for any $k<n$ . A square

is called k-cartesian if the gap map $C\to A\times_X B$ is k-connected. In particular, any pullback square is $(n-1)$ -cartesian, so the n-truncation of a pullback square is an $(n-1)$ -cartesian square.

We work in homotopy type theory with a predicative hierarchy of univalent universes closed under n-truncations. Although we recall the basic definitions, we refer to Univalent Foundations Program (2013, Sec. 7) for some results about n-types and the n-truncation modality, and we also assume some familiarity with the basic theory of k-symmetric n-groups as developed in Buchholtz et al. (Reference Buchholtz, van Doorn and Rijke2018).Footnote 3

1.1 Outline

We start by establishing some basic definitions and notation in Section 2. In Section 3, we define the notion of $\infty$ -exactness and show that any fiber sequence induces a long $\infty$ -exact sequence of homotopy $\infty$ -groups. In Section 4, we turn to n-exactness of k-symmetric n-groups and show that it is equivalent to n-exactness of the map on underlying $(n-1)$ -types. Our main results are in Section 5, and in Section 6, we point to some related work in the classical setting.

2. Basic Definitions and Notation

Just as in Univalent Foundations Program (2013), we write $x=y$ for the type of identifications of x and y, provided that both x and y have a common type X. Sometimes we call identifications paths. We write

\begin{equation*} \mathrm{ap}_f:(x=y)\to (f(x)=f(y))\end{equation*}

for the action of a function f on paths. Path concatenation is written in diagrammatic order, i.e., we write $p \centerdot q$ for the concatenation of $p:x=y$ and $q:y=z$ . The fiber of a map $f:A\to B$ at $b:B$ is defined to be the type

\begin{equation*} \mathrm{fib}_f(b):\equiv \sum\nolimits_{(x:A)}f(x)=b.\end{equation*}

If B is a pointed type with base point $y_0$ , we define the kernel of f as the fiber of f at $y_0$ , $\ker(f) :\equiv \mathrm{fib}_f(y_0)$ .

Definition 2.1. A map $f:X\to Y$ is said to be an n-truncation if Y is n-truncated, and for any family P of n-truncated types over Y, the precomposition map

\begin{equation*} \mathord{\hspace{1pt}\text{--}\hspace{1pt}}\circ f:\Big(\prod\nolimits_{(y:Y)}P(y)\Big)\to\Big(\prod\nolimits_{(x:X)}P(f(x))\Big) \end{equation*}

is an equivalence. We assume that every type X has an n-truncation

\begin{equation*} \eta:X\to\| X\|_{n}.\end{equation*}

Definition 2.2. Consider a pointed type B with base point $x_0$ and a family $E:B\to\mathcal{U}$ equipped with a base point $y_0:E(x_0)$ in the fiber over $x_0$ . The type of pointed sections $\prod\nolimits^\ast_{(x:B)}E(x)$ is the type of pairs (f,p) consisting of a section $f:\prod\nolimits_{(x:B)}E(x)$ and an identification $p:f(x_0)=y_0$ .

Given two pointed sections $(f,p),(g,q):\prod\nolimits^\ast_{(x:B)}E(x)$ , we define the type of pointed homotopies as

\begin{equation*} f\sim_\ast g :\equiv \prod\nolimits^\ast_{(x:B)}f(x)=g(x), \end{equation*}

where we equip the family of identifications given by $x\mapsto (f(x)=g(x))$ with the base point

\begin{equation*} p \centerdot q^{-1} : f(x_0)=g(x_0) \end{equation*}

in the fiber over $x_0$ .

In the case of a nondependent type family, we recover the notions of pointed maps and pointed homotopies between these.

Definition 2.3. A k-symmetric n-group G is a pointed $(k-1)$ -connected $(n+k-1)$ -type $B^kG$ . Its underlying type is the k-fold loop space $\Omega^kB^kG$ . A homomorphism $f : G \to H$ of k-symmetric n-groups is represented by a pointed map $B^kf : B^kG \to_* B^kH$ .

We call $B^kG$ the classifying type of G.

Definition 2.4. The m-connected cover $X\langle m\rangle$ of a pointed type X is the kernel of $\eta : X \to \| X\|_{m}$ , equivalently,

\begin{equation*} X\langle m\rangle :\equiv \sum\nolimits_{(x:X)}\| x_0=x\|_{m-1}. \end{equation*}

Recall that $\eta:X\to\| X\|_{m}$ is an m-connected map, so that $X\langle m\rangle$ is indeed an m-connected type.

Definition 2.5. The k’th homotopy n-group of a pointed type X is represented by the $(n+k-1)$ -truncation of the $(k-1)$ -connected cover of X at the base point, i.e., it is defined via the type

\begin{equation*} B^k\pi^{(n)}_k(X) :\equiv \| X\langle k-1\rangle\|_{n+k-1}. \end{equation*}

The underlying type of $\pi^{(n)}_k(X)$ is equivalent to $\| \Omega^k X\|_{n-1}$ .

Thus, we see that $B^k\pi^{(n)}_k(X)$ fits in the fiber sequence

Note also that in the case $k=0$ , we just recover the $(n-1)$ -truncation of X. The observation that $B^k\pi^{(n)}_k(X)$ is the kernel of $\| X\|_{n+k-1}\to\| X\|_{k-1}$ is a generalization of the well-known fiber sequence

in which the fiber is the k’th Eilenberg-Mac Lane space of the k’th homotopy group of X (Licata and Finster Reference Licata and Finster2014).

We can also set $n\equiv\infty$ in these definitions:

Definition 2.6. A k-symmetric $\infty$ -group G is a pointed $(k-1)$ -connected type $B^kG$ . Its underlying type is the k-fold loop space $\Omega^kB^kG$ . The k’th homotopy $\infty$ -group of a pointed type X is represented by $(k-1)$ -connected cover of X at the base point

\begin{equation*} B^k\pi^{(\infty)}_k(X) :\equiv X\langle k-1\rangle, \end{equation*}

so the underlying type is equivalent to $\Omega^k X$ .

3. The Long $\infty$ -Exact Sequence of a Fiber Sequence

Definition 3.1. A short sequence (or complex) consists of pointed types B, E, and F with base points $x_0:B$ , $z_0:E$ and $y_0:F$ , respectively, equipped with pointed maps

and a pointed homotopy $H:p\circ_\ast i \sim_\ast \mathrm{const}_{x_0}$ . This homotopy witnesses that the square

commutes. A short sequence is said to be a fiber sequence if the above square is a pullback square.

Definition 3.2. A short sequence

is said to be $\infty$ -exact if the family of maps

\begin{equation*} \alpha : \prod\nolimits_{(z:E)} \mathrm{fib}_i(z)\to (p(z)=x_0) \end{equation*}

given by $\alpha(z,(y,q))= \mathrm{ap}_p(q)^{-1} \centerdot H(y)$ is a family of equivalences.

Proposition 3.3. A short sequence is $\infty$ -exact if and only if it is a fiber sequence.

Proof. First we note that we have a commuting square

where the gap map at the top sends $y:F$ to the triple $(*,i(y),H(y))$ . The two vertical maps in this square are equivalences. Thus, we see that the gap map is an equivalence if and only if $\mathrm{total}(\alpha)$ is an equivalence, which is the case if and only if each $\alpha_z:\mathrm{fib}_i(z)\to (p(z)=x_0)$ is an equivalence.

The following corollary is of course a well-known fact.Footnote 4

Corollary 3.4. For any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ , we obtain a long $\infty$ -exact sequence

We can reinterpret this as the sequence

where the maps into a k-symmetric $\infty$ -group are homomorphisms of k-symmetric $\infty$ -groups (i.e., pointed maps of the classifying types). This motivates the following definitions and subsequent observation.

Definition 3.5. A short sequence (or complex) of k-symmetric $\infty$ -groups consists of three k-symmetric $\infty$ -groups K,G,H, and homomorphisms

with an identification of $\varphi\circ\psi$ with the trivial homomorphism from K to H as homomorphisms. By definition, this means we have a short sequence

of classifying types.

Definition 3.6. Given a homomorphism of k-symmetric $\infty$ -groups $\varphi : G \to H$ , we define its kernel, $\ker(\varphi)$ , via the classifying type $B^k\ker(\varphi) :\equiv \ker(B^k\varphi)\langle k-1 \rangle$ , that is, the $(k-1)$ -connected cover of the pointed kernel at the level of classifying types, $\ker(B^k\varphi)$ .

At the level of underlying types, we then have $\Omega^kB^k\ker(\varphi) \simeq \Omega^k\ker(B^k\varphi) \simeq \ker(\Omega^kB^k\varphi)$ , where the first equivalence is an instance of the equivalence $\Omega^k(X\langle k-1\rangle \simeq \Omega^k X$ and the second follows by iterated application of the equivalence $\Omega(\ker(f)) \simeq \ker(\Omega(f))$ for any pointed map f. That is, the underlying type of the kernel is the kernel of the map of underlying types.

Definition 3.7. A short sequence of k-symmetric $\infty$ -groups $K \xrightarrow{\psi}{} G \xrightarrow{\varphi}{} H$ is $\infty$ -exact if the induced homomorphism $K \to \ker(\varphi)$ , obtained as the unique lift in the commutative square

where the left map is $(k-2)$ -connected and the right map is $(k-2)$ -truncated is an equivalence.

The following proposition is the higher analog of the fact that a group homomorphism is an isomorphism if and only if its underlying map is a bijection.

Proposition 3.8. A homomorphism of k-symmetric $\infty$ -groups is an equivalence if and only if the map of underlying types is an equivalence.

Proof. This follows by induction, based on the fact that a pointed map of connected types $f : X \to Y$ is an equivalence if and only if $\Omega f : \Omega X \to \Omega Y$ is Univalent Foundations Program (2013, Cor. 8.8.2).

Corollary 3.9. A short sequence of k-symmetric $\infty$ -groups is $\infty$ -exact if and only if the short sequence of underlying types is $\infty$ -exact.

4. Exactness of Complexes of k-Symmetric n-Groups

Now we have laid the groundwork to consider the case of n-groups of finite n.

Definition 4.1. A short sequence (or complex) of k-symmetric n-groups is a short sequence of three k-symmetric $\infty$ -groups that happen to be n-groups.

But beware that we have a different notion of exactness in this case, cf. Definition 4.3 below.

Proposition 4.2. Given a homomorphism of k-symmetric n-groups $\varphi : G \to H$ , the kernel $\ker(\varphi)$ is again an n-group.

Proof. This follows since $\ker(B^k\varphi)$ is an $(n+k-1)$ -type, and taking the $(k-1)$ -connected cover preserves $(n+k-1)$ -types.

Definition 4.3. A short sequence of k-symmetric n-groups $K \xrightarrow{\psi}{} G \xrightarrow{\varphi}{} H$ is n-exact if and only if the induced map of underlying $(n-1)$ -types $K \to \ker(\varphi)$ is $(n-2)$ -connected.

In contrast to the $\infty$ -case, we also have a useful notion of image for finite n:

Definition 4.4. Given a homomorphism of k-symmetric n-groups $\varphi : G \to H$ , we define the n-image $\mathrm{im}^n(\varphi)$ via the classifying type $B^k\mathrm{im}^n(\varphi)$ as it appears in the $(n+k-2)$ -image factorization of $B^k\varphi$ (Univalent Foundations Program 2013, Def. 7.6.3):

(1)

viz., $B^k\mathrm{im}^n(\varphi):\equiv \sum\nolimits_{(t:B^kH)}\| \mathrm{fib}_{B^k\varphi}(t)\|_{n+k-2}$ .

When n is fixed and clear from the context, we shall leave it out from the notation and just write $\mathrm{im}(\varphi)$ for the (n-)image. We do not mention k in the notation, thanks to the following.

Proposition 4.5. Given a homomorphism of k-symmetric n-groups $\varphi : G \to H$ with $k>0$ , we can regard $\varphi$ as a homomorphism of underlying $(k-1)$ -symmetric n-groups. Then the universal property of the $(n+k-3)$ -image factorization induces an equivalence $\Omega B^k\mathrm{im}^n(\varphi) \simeq B^{k-1}\mathrm{im}^n(\varphi)$ .

Proof. If we apply the loop space functor to (1), we get a factorization of $\Omega B^k\varphi = B^{k-1}\varphi$ as an $(n+k-3)$ -connected map followed by an $(n+k-3)$ -truncated map. Thus, we get the desired induced equivalence (Univalent Foundations Program 2013, Thm. 7.6.6).

In particular, at the level of underlying $(n-1)$ -types, the n-image $\mathrm{im}^n(\varphi)$ is the usual $(n-2)$ -image. In the special case $n=1$ of 1-groups, we recover the usual image (i.e., $(-1)$ -image) at the level of underlying sets. Footnote 5

Proposition 4.6. A short sequence of k-symmetric n-groups $K \xrightarrow{\psi}{} G \xrightarrow{\varphi}{} H$ is n-exact if and only if the unique homomorphism $\mathrm{im}^n(\psi) \to \ker(\varphi)$ is an equivalence.

Proof. The map of underlying types $K \to \ker(\varphi)$ is $(n-2)$ -connected if and only if the map $B^kK \to B^k\ker(\varphi)$ is $(n+k-2)$ -connected, and this happens if and only if the right map in the $(n+k-2)$ -image factorization is an equivalence.

5. The Long n-Exact Sequence of Fiber Sequences

Our deliberations in the previous section motivate the following definition.

Definition 5.1. A short sequence $F\xrightarrow i{} E\xrightarrow p{} B$ of pointed types is n-exact if for each $z:E$ , the map

\begin{equation*} \alpha_z : \mathrm{fib}_i(z)\to (p(z)=x_0) \end{equation*}

as in Definition 3.2 is $(n-2)$ -connected.

Definition 5.2. A commuting square

is k-cartesian if its gap map $C \to A \times_X B$ is k-connected.

Lemma 5.3. Consider a short sequence $F\xrightarrow i{} E\xrightarrow p{} B$ . The following are equivalent:

  1. (1) The short sequence is n-exact.

  2. (2) The square

    is $(n-2)$ -cartesian.

Proof. Recall that the fiber of $\alpha_z$ at $q:p(z)=x_0$ is equivalent to the fiber of $\mathrm{total}(\alpha)$ at $(z,q):\mathrm{fib}_p(x_0)$ (Univalent Foundations Program 2013, Thm. 4.7.6). Therefore, it follows immediately that each $\alpha_z$ is $(n-2)$ -connected if and only if $\mathrm{total}(\alpha)$ is $(n-2)$ -connected.

We now come to the key observation:

Proposition 5.4. The n-truncation modality preserves k-cartesian squares for any $k<n$ .

Proof. Consider a k-cartesian square

for some $k<n$ . Our goal is to show that the square

is again k-cartesian. To see this, consider the commuting square

In this square, the top map is assumed to be k-connected. The left map is n-connected, so it is also k-connected. Recall that if, in a commuting triangle

the top map is k-connected, then the left map is k-connected if and only if the right map is Rijke et al. (Reference Rijke, Shulman and Spitters2020, Lem. 1.33). Therefore, it suffices to show that the right map in the above square is k-connected. This is indeed the case, since it is the induced map on total spaces of the two n-connected maps $\eta:A\to\| A\|_{n}$ and $\eta:B\to\| B\|_{n}$ , and the $(n-1)$ -connected map $\mathrm{ap}_\eta: (f(a)=g(b))\to (\eta(f(a))=\eta(g(b)))$ , all of which are also k-connected.

Our main theorem is now a simple consequence of the above results.

Theorem 5.5. Any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ induces an n-exact short sequence $\| F\|_{n-1}\to\| E\|_{n-1}\to\| B\|_{n-1}$ .

Proof. Consider a fiber sequence $F\hookrightarrow E\twoheadrightarrow B$ . Since any pullback square is in particular $(n-2)$ -cartesian, it follows from Proposition 5.4 that the square

is $(n-2)$ -cartesian. By Lemma 5.3, it now follows that the short sequence $\| F\|_{n}\hookrightarrow\| E\|_{n}\twoheadrightarrow\| B\|_{n}$ is n-exact.

As a corollary, we obtain the long n-exact sequence of homotopy n-groups, obtained from a fiber sequence $F\hookrightarrow E\twoheadrightarrow B$ .

Corollary 5.6. For any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ , we obtain a long n-exact sequence

of homotopy n-groups, where the morphisms are homomorphisms of k-symmetric n-groups whenever the codomain is a k-symmetric n-group.

As a further application we note:

Corollary 5.7. Given a short n-exact sequence of k-symmetric n-groups $K \xrightarrow{\psi}{} G \xrightarrow{\varphi}{} H$ , the resulting looped sequence $\Omega K \to \Omega G \to \Omega H$ is a short $(n-1)$ -exact sequence of $(k+1)$ -symmetric $(n-1)$ -groups, and the resulting decategorified sequence $\mathrm{Decat}(K) \to \mathrm{Decat}(G) \to \mathrm{Decat}(H)$ is a short $(n-1)$ -exact sequence of k-symmetric $(n-1)$ -groups.

Here, Decat maps a k-symmetric n-group G, represented by the pointed $(k-1)$ -connected $(n+k-1)$ -type $B^kG$ , to the k-symmetric $(n-1)$ -group $\mathrm{Decat}(G)$ , represented by $\| B^kG\|_{n+k-2}$ (Buchholtz et al. Reference Buchholtz, van Doorn and Rijke2018, Sec. 6).

6. Discussion and Related Work

The notion of 2-exactness of a complex of 2-groups is by now standard when described in terms of crossed complexes or gr-stacks (Aldrovandi and Noohi Reference Aldrovandi and Noohi2009; Vitale Reference Vitale2002). Our Corollary 5.7 is reminiscent of the results of Kasangian et al. (Reference Kasangian, Metere and Vitale2011) in the setting of strict groupoids.

The benefits of our synthetic development are that we automatically get the results in the case of stacks over a Grothendieck site as well by interpretation in the corresponding $(\infty,1)$ -topos, and that our approach covers all higher groups, not just the case of 2-groups as presented by crossed modules.

Acknowledgements

The authors acknowledge the support of the Centre for Advanced Study (CAS) at the Norwegian Academy of Science and Letters in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19. The authors are also grateful to the anonymous referees for constructive and helpful comments.

Footnotes

1 More precisely, the quoted theorem includes the interpretation of many higher inductive types, including the truncations we use here, but not yet the closure of univalent universes under these.

2 An $(\infty,1)$ -topos satisfying Whitehead’s principle is also called hypercomplete. Examples of non-hypercomplete $(\infty,1)$ -toposes (in a classical metatheory) include the $(\infty,1)$ -topos of parametrized spectra (an object is hypercomplete if and only if the spectrum part is trivial) and the $(\infty,1)$ -topos of continuous $\mathbb{Z}_p$ -equivariant spaces, where we view the group $\mathbb{Z}_p$ of p-adic integers as a profinite group (Lurie Reference Lurie2009, Warning 7.2.2.31). The latter example is even boolean, hence satisfies the law of excluded middle internally.

3 The terminology is a bit in flux: In loc.cit. the term was “k-tuply groupal $(n-1)$ -types, which is more in line with the classical notion of group-like $\mathbb{E}_k$ -algebra in $(n-1)$ -types, where $\mathbb{E}_k$ is the little k-cubes $\infty$ -operad. Another proposed term is “ $(k-1)$ -commutative n-group”.

4 It was formalized already in Voevodsky’s first UniMath formalization, Part A, ca. 2010–11 (Voevodsky et al. n.d.).

5 This is the reason we write a superscript n for the higher group-theoretical n-image: We have to subtract 2 when we describe this as an $(n-2)$ -image in the sense of the truncation modality orthogonal factorization system at the level of underlying $(n-1)$ -types: $\mathrm{im}^n(\varphi) = \mathrm{im}_{n-2}(\varphi)$ .

References

Aldrovandi, E. and Noohi, B. (2009). Butterflies. I. Morphisms of 2-group stacks. Advances in Mathematics 221 (3) 687773. http:10.1016/j.aim.2008.12.014.CrossRefGoogle Scholar
Buchholtz, U., van Doorn, F. and Rijke, E. (2018). Higher groups in homotopy type theory. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’18, New York, NY, USA, ACM, 205–214. doi: 10.1145/3209108.3209150.CrossRefGoogle Scholar
Kasangian, S., Metere, G. and Vitale, E. M. (2011). The ziqqurath of exact sequences of n-groupoids. Cahiers de Topologie et Géométrie Différentielle Catégoriques 52 (1) 244. http://www.numdam.org/item/CTGDC_2011__52_1_2_0.Google Scholar
Licata, D. R. and Finster, E. (2014). Eilenberg-MacLane spaces in homotopy type theory. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), New York, ACM, Article No. 66, 10.Google Scholar
Lumsdaine, P. L. and Shulman, M. (2020). Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society 169 (1) 159208. doi: 10.1017/S030500411900015X.CrossRefGoogle Scholar
Lurie, J. (2009). Higher Topos Theory , Annals of Mathematics Studies, vol 170, Princeton, NJ: Princeton University Press, xviii+925. doi: 10.1515/9781400830558.Google Scholar
Rijke, E., Shulman, M. and Spitters, B. (2020). Modalities in homotopy type theory. Logical Methods in Computer Science 16 (1). doi: 10.23638/LMCS- 16(1:2)2020.Google Scholar
Shulman, M. (2019) All $(\infty,1)$ -toposes have strict univalent universes. arXiv:1904.07004.Google Scholar
Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book/.Google Scholar
Vitale, E. M. (2002). A Picard-Brauer exact sequence of categorical groups. In: 1–3 Special volume celebrating the 70th birthday of Professor Max Kelly, vol. 175, 383–408. doi: 10.1016/S0022-4049(02)00142-1.CrossRefGoogle Scholar
Voevodsky, V., Ahrens, B., Grayson, D. et al. (n.d). UniMath — a computer-checked library of univalent mathematics. http://UniMath.org.Google Scholar