Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Higher inductive types in $(\infty,1)$-categories

Taichi Uemura

Abstract

We propose a definition of higher inductive types in $(\infty,1)$-categories with finite limits. We show that the $(\infty,1)$-category of $(\infty,1)$-categories with higher inductive types is finitarily presentable. In particular, the initial $(\infty,1)$-category with higher inductive types exists. We prove a form of canonicity: the global section functor for the initial $(\infty,1)$-category with higher inductive types preserves higher inductive types.

Higher inductive types in $(\infty,1)$-categories

Abstract

We propose a definition of higher inductive types in -categories with finite limits. We show that the -category of -categories with higher inductive types is finitarily presentable. In particular, the initial -category with higher inductive types exists. We prove a form of canonicity: the global section functor for the initial -category with higher inductive types preserves higher inductive types.

Paper Structure

This paper contains 11 sections, 51 theorems, 12 equations, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Presentable categories
  4. Presentable $2$-categories
  5. Lex universes
  6. Marked categories
  7. Cartesian fibrations
  8. Higher inductive types in $\mathbf{S}$
  9. Categories with higher inductive types
  10. Examples of higher inductive types
  11. Canonicity for higher inductive types

Key Result

Theorem 1

The global section functor for the initial $(\infty,1)$-category with higher inductive types preserves higher inductive types.

Theorems & Definitions (109)

  • Theorem : \ref{['prop-inductive-type-canonicity']}
  • Theorem : \ref{['prop-homotopy-group-canonicity']}
  • Proposition 2.1
  • proof
  • Proposition 2.2
  • proof
  • Proposition 2.3: adamek1994locally
  • proof
  • Proposition 2.4: adamek1994locally
  • proof
  • ...and 99 more