Synthetic Lecture 2: First steps with Segal types¶

With the basics in HoTT from Lecture 1, we are now ready to introduce the simplicial extension due to Riehl--Shulman. We want to do higher category theory synthetically. We have seen how in homotopy type theory every type is an $\infty$-groupoid. But how do we get a working theory of $\infty$-categories? In simplicial HoTT, the approach is to introduce an axiomatic directed interval, defining the shape of a morphism that need not necessarily be invertible. We describe the setup in sHoTT and Rzk to achieve this.

§2.1. Shapes in simplicial HoTT¶

Recall that in ordinary dependent type theory types depend on contexts:

\[ \Gamma \vdash A \]

In sHoTT, we want our types to not only depend on other types but geometric shapes. This is done by adding new layers to the type theory with their corresponding notion of context.

Concretely, a general family depends on a multi-part context

\[ \Xi \; | \; \Phi \; | \; \Gamma \vdash A\]

where:

$\Xi$ is a cube context
$\Phi$ is a tope context
$\Gamma$ is a type context
The cube layer is a non-dependent type theory, generated by the following:
the terminal cube $\mathbf{1}$ aka the $0$-cube with a unique term $1_1 \in \mathbf{1}$.
a directed interval $\mathbf{2}$ aka the $1$-cube with two terms $0_2, 1_2 : \mathbf{2}$
for every pair of cubes $I, J$ the cartesian product $I \times J$ is again a cube
A tope is a formula over a cube generated from:
equality topes of the form $s \equiv t$ for $s,t : I$, for a cube $I$
inequality topes of the form $s \leq t$ for $s,t : \mathbf{2}$
the minimal and maximal topes $\bot, \top$
finite conjunction $\land$ and finite disjunction $\lor$

Tope formulas live over a cube context:

\[ \Xi \; |\; \varphi \; \; \text{tope}\]

Moreover, a tope formula can be entailed by a tope context (over a common cube):

\[ \Xi \; |\; \Phi \vdash \psi \; \; \text{tope}\]

A cube $I$ together with a tope formula $\varphi$ is called a shape, written $\{ t : I \; | \; \varphi(t)\}$.

If $I \; | \; \varphi \vdash \psi$, we say that the shape defined by $\varphi$ is a subshape of $\psi$, and we write:

\[ \{ t : I \; | \; \varphi(t)\} \subseteq \{ t : I \; | \; \psi(t)\}, $$ or, for short: $$ \varphi \subseteq \psi.\]

We show below the following important shapes together with their definitions in Rzk.

The representation of (sub-)topes/shapes in Rzk is analogous to the presentation of ordinary dependent types, i.e., as a family into an appropriate universe:

sHoTT	Rzk
type $\; \vdash A$	`A:U`
dependent type $x : A \vdash B(x)$	`B:A -> U`
cube $I$	`I : CUBE`
tope/shape $t : I \vdash \varphi(t)$	`Φ : I → TOPE`
subtope/subshape $t : I \; \\| \; \varphi(t) \vdash \psi(t)$	`ϕ : ψ → TOPE`

$1$-simplex $\Delta^2$:

#lang rzk-1
#def Δ¹
  : 2 → TOPE
  := \ t → TOP

#def ∂Δ¹
  : Δ¹ → TOPE
  := \ t → (t ≡ 0₂ ∨ t ≡ 1₂)

$2$-simplex $\Delta^2$: $2$-simplex">

#def Δ²
  : ( 2 × 2) → TOPE
  := \ (t , s) → s ≤ t

$3$-simplex $\Delta^3$: $3$-simplex">

#def Δ³
  : ( 2 × 2 × 2) → TOPE
  := \ ((t1 , t2) , t3) → t3 ≤ t2 ∧ t2 ≤ t1

$(2,1)$-horn $\Lambda_1^2$: <span class=

$3$-simplex">

#def Λ
  : ( 2 × 2) → TOPE
  := \ (t , s) → (s ≡ 0₂ ∨ t ≡ 1₂)

#def Λ²₁
  : Δ² → TOPE
  := \ (t , s) → Λ (t , s)

#def shape-prod
  ( I J : CUBE)
  ( ψ : I → TOPE)
  ( χ : J → TOPE)
  : ( I × J) → TOPE
  := \ (t , s) → ψ t ∧ χ s

#def Δ¹×Δ¹
  : ( 2 × 2) → TOPE
  := shape-prod 2 2 Δ¹ Δ¹

§2.2. Extension types in simplicial HoTT¶

If we assumed a directed interval type $\mathbb I$ we could define the type of arrows in a type $A$ as follows:

\[ \sum_{f : \mathbb I \to A} (f(0) =_A x) \times (f(1) =_A y)\]

Terms in this type are morphisms up to homotopy, i.e. triples $\langle f, p, q \rangle$ where $p,q$ are paths $p : f(0) = x$ and $q : f(1) = y$. Given the intensional character of our identity types, we cannot necessarily conclude that $f(0) \equiv x$ and $f(1) \equiv y$, so we have to keep track about the homotopical data. This becomes difficult to work with quite quickly.

In this version of simplicial HoTT, we will work with extension types instead:

Let $\phi \subseteq \psi$ be a shape inclusion.
Let $t : \phi \vdash a(t) : A$.

We now want to consider all the terms $t : \psi \vdash b(t) : A$ that extend $a$, and strictly so:

\[ t : \phi \vdash a(t) \equiv b(t) \]

This cannot be defined in our type theory, so we add as a primitive the extension type associated to the data $(A, \phi \subseteq \psi, a)$:

\[ \langle \psi \to A |^\phi_a \rangle \]

The syntax looks like a function type, only with some imposed side conditions---and that's exactly right. The terms $b : \langle \psi \to A |^\phi_a \rangle$ are dependent terms

\[ t : \psi \vdash b(t) : A \]

that also satisfy:

\[ t : \phi \vdash b(t) \equiv a(t) \]

sHoTT	Rzk
type $\; \vdash A$	`A:U`
dependent type $x : A \vdash B(x)$	`B:A -> U`
cube $I$	`I : CUBE`
tope/shape $t : I \vdash \varphi(t)$	`Φ : I → TOPE`
subtope/subshape $t : I \; \\| \; \varphi(t) \vdash \psi(t)$	`ϕ : ψ → TOPE`
term over shape $t : \varphi(t) \vdash b(t) : A$	`b : ϕ → A`
extension type $\langle \psi \to A \rangle$	`(t : ψ) → A [ϕ t ↦ a t]`

§2.3. Morphisms in a type¶

Let $A$ be a type and $x,y:A$. We will use the extension types to define types of arrows or morphisms in $A$. The idea is that an arrow $x \to y$ should have the shape of the interval $\Delta^1$ with the initial vertex labeled $x$ and the terminal vertex labeled $y$.

In sHoTT we define this as:

\[\hom_A(x,y) := \left \langle \Delta^1 \to A |^{\partial \Delta^1}_{[x,y]}\right\rangle\]

In Rzk, the notation is:

#def hom
  ( A : U)
  ( x y : A)
  : U
  :=
  (t : Δ¹)
  → A [ t ≡ 0₂ ↦ x , -- the left endpoint is exactly `x`
        t ≡ 1₂ ↦ y ] -- the right endpoint is exactly `y`

For every term $x : A$ we can define the identity morphism as the morphism that is constant at $x$:

\[ \mathrm{id}_x :\equiv \lambda t.x : \hom_A(x,x)\]

Can you write this in Rzk?

#def id-hom (A : U) (x : A)
  : hom A x x
  := \ t → x

To talk about composition, we need to reason about triangles. Let $x,y,z : A$, $f : \hom_A(x,y)$, $g : \hom_A(y,z)$, and $h : \hom_A(x,z)$. We define the type of triangles with boundary consisting of those morphisms as:

\[ \hom_{A,x,y,z}^2(f,g,h) :\equiv \left \langle \Delta^2 \to A |^{\partial \Delta^2}_{[f,g,h]}\right\rangle\]

In Rzk, this can be implemented as follows using case-splits on the dimension variables on the simplex:

#def hom2
  ( A : U)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  ( h : hom A x z)
  : U
  :=
  ( ( t₁ , t₂) : Δ²)
  → A [ t₂ ≡ 0₂ ↦ f t₁ , -- the top edge is exactly `f`,
        t₁ ≡ 1₂ ↦ g t₂ , -- the right edge is exactly `g`, and
        t₂ ≡ t₁ ↦ h t₂]  -- the diagonal is exactly `h`

There are some canonical triangles in every type, regardless if it's a category or not:

Triangle witnesses

E.g., the leftmost one is given by:

#def const-triangle (A : U) (x : A)
  : hom2 A x x x
    ( id-hom A x) (id-hom A x) (id-hom A x)
  := \ (t , s) → x

Of course, these should witness unitality of the identity morphism, part of the axiomatics of a category. But we don't have a notion of composition yet!

2.3 Segal types¶

We want to express the property of a type having composition of arrows (as witnessed by a $2$-simplex) uniquely up to homotopy. Namely, we call a type $A$ Segal if and only if the following proposition is satisfied:

\[ \text{is-Segal}(A) :\equiv \prod_{x,y,z:A} \prod_{f : \hom_A(x,y)}\prod_{g : \hom_A(y,z)} \text{is-contr}\left( \sum_{h : \hom_A(x,z)}\hom_A^2(f,g,h) \right) \]

In Rzk, this translates into:

#def is-segal
  ( A : U)
  : U
  :=
  ( x : A) → (y : A) → (z : A)
  → ( f : hom A x y) → (g : hom A y z)
  → is-contr (Σ (h : hom A x z) , (hom2 A x y z f g h))

It will be handy to extract the pieces of the "canonical" composition data through the following helper functions. The data is comprised out of: 1. a composite morphism ($1$-simplex) $\mathrm{comp}_A(f,g)$ 2. a triangle ($2$-simplex) bounded $f$, $g$, and $\mathrm{comp}(f,g)$:

#def comp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  : hom A x z
  := first (first (is-segal-A x y z f g))

#def witness-comp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  : hom2 A x y z f g (comp-is-segal A is-segal-A x y z f g)
  := second (first (is-segal-A x y z f g))

Indeed, we can now prove that the Segal condition implies the unique existence of composite morphisms. Whenever there exists a candidate composite edge $h : \hom_A(x,z)$, fitting into a $2$-simplex $\alpha : \hom_A^2(f,g,h)$, then we can construct a path from the canonical composite as constructed above.

For this, we need some prerequisites about paths in sHoTT:

#def ap
  ( A B : U)
  ( x y : A)
  ( f : A → B)
  ( p : x = y)
  : f x = f y
  := ?

#def first-path-Σ
  ( A : U)
  ( B : A → U)
  ( s t : Σ (a : A) , B a)
  ( e : s = t)
  : first s = first t
  := ?

#def uniqueness-comp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  ( h : hom A x z)
  ( alpha : hom2 A x y z f g h)
  : ( comp-is-segal A is-segal-A x y z f g) = h
  :=
  first-path-Σ
  ( hom A x z)
  ( hom2 A x y z f g)
  ( comp-is-segal A is-segal-A x y z f g
    , witness-comp-is-segal A is-segal-A x y z f g)
  ( h , alpha)
  ( homotopy-contraction
    ( Σ ( k : hom A x z) , (hom2 A x y z f g k))
    ( is-segal-A x y z f g)
    ( h , alpha))

sHoTT	Rzk
type \(\; \vdash A\)	`A:U`
dependent type \(x : A \vdash B(x)\)	`B:A -> U`
cube \(I\)	`I : CUBE`
tope/shape \(t : I \vdash \varphi(t)\)	`Φ : I → TOPE`
subtope/subshape \(t : I \; \\| \; \varphi(t) \vdash \psi(t)\)	`ϕ : ψ → TOPE`