Introduction to simplicial HoTT and synthetic ∞-categories¶

#lang rzk-1

Simplicial types with Rzk¶

Following Riehl–Shulman's paper¹, Rzk has cube and tope layers². These provide the ability to specify (higher) diagram schemas.

For the purposes of his demo, we will only care about the directed interval cube 2, 2-dimensional directed cube (2 × 2), and 3-dimensional directed cube (2 × 2 × 2).

A cube may have points in it, and the directed interval 2 has two known points 0₂ : 2 and 1₂ : 2.

Tope layer¶

Tope layer adds logical constraints on the points in a cube, "carving out" a shape inside a space. There is a handful of ways to specify topes:

TOP selects all points (provides no constraints)
BOT selects no points (producing an empty shape)
(φ ∧ ψ) selects all points that satisfy both φ and ψ
(φ ∨ ψ) selects all points that satisfy φ or ψ (or both)
(t ≡ s) selects all points such that t is equal to s
(t ≤ s) selects all points such that t ≤ s (only when both t and s are in 2)

Mostly for technical reasons, we define shapes as mappings from cubes into the TOPE universe. For example, here is a shape that carves a (directed) triangle out of a (directed) square:

#define Δ¹
  : 2 → TOPE
  := \ _ → TOP

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

For another example, here is a 3-dimensional simplex:

#define Δ³
  : (2 × 2 × 2) → TOPE
  := \ ((t₁, t₂), t₃) → (t₃ ≤ t₂) ∧ (t₂ ≤ t₁)

Yet another example would be the horn shape that only takes two edges of a square:

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

We could refine this definition by specifying that it is a subshape of Δ²:

#define Λ'
  : ( (t, s) : 2 × 2 | Δ² (t, s) ) → TOPE
  := \ (t, s) → (s ≡ 0₂) ∨ (t ≡ 1₂)

Since shapes have the information about the cube in their types, Rzk provides an implicit coercion, allowing shorter definitions:

#define Λ''
  : Δ² → TOPE
  := \ (t, s) → (s ≡ 0₂) ∨ (t ≡ 1₂)

Note

This more precise type expresses a restriction on the definition of Λ'', but, perhaps counterintuitively, not on the input points! With this type, Rzk additionally checks that (s ≡ 0) ∨ (t ≡ 1) implies Δ² (t, s) for all t, s. However, we can still apply Λ'' to all points in the cube (2 × 2).

Mapping from a shape into a type, effectively selects a concrete diagram in it. We can select a subdiagram, simply by restricting to a subshape:

#define horn-restriction
  (A : U)
  : (f : Δ² → A) → (Λ → A)
  := \ f t → f t

To construct diagrams from parts, we can use recOR by specifying values for several shapes. Rzk will be checking that provided values agree (definitionally) on the intersections of these shapes.

For example, given a triangle, we can construct a square:

#define unfolding-square
  (A : U)
  (triangle : Δ² → A)
  : (2 × 2) → A
  :=
    \ (t, s) →
    recOR
      ( t ≤ s ↦ triangle (s , t) ,
        s ≤ t ↦ triangle (t , s))

Extension types with Rzk¶

Mapping from a shape into a type, we get a diagram. To fix some parts of the diagram, we can specify refinements — for each subshape we want to fix, we provide an explicit term of the proper type.

For example, taking a diagram in A correspoding to the directed interval 2 and fixing the endpoints, we get the type of all arrows between two given points in A:

#define hom
  (A : U)
  (x y : A)
  : U
  := (t : 2) →
    A [ t ≡ 0₂ ↦ x
      , t ≡ 1₂ ↦ y ]

Note that this is different from the following type, since in hom endpoints are x and y definitionally, where as pseudo-hom carries proofs of equality and requires extra bookkeeping:

#define pseudo-hom
  (A : U)
  (x y : A)
  : U
  := Σ (f : 2 → A), product (f 0₂ = x) (f 1₂ = y)

Another common example of an extension type would be the hom2 type of composites of arrows:

#define hom2
  (A : U)
  (x y z : A)
  (f : hom A x y)
  (g : hom A y z)
  : U
  := ((t, s) : Δ²) →
    A [ s ≡ 0₂ ↦ f t
      , t ≡ 1₂ ↦ g s ]

Cofibration composition¶

A useful theorem about extension types says that any extension type is equivalent to an extension of its restriction.

RS17, Theorem 4.4

#def cofibration-composition
  ( I : CUBE)
  ( χ : I → TOPE)
  ( ψ : χ → TOPE)
  ( ϕ : ψ → TOPE)
  ( X : χ → U)
  ( a : (t : ϕ) → X t)
  : Equiv
    ( (t : χ) → X t [ϕ t ↦ a t])
    ( Σ ( f : (t : ψ) → X t [ϕ t ↦ a t]) ,
        ( (t : χ) → X t [ψ t ↦ f t]))
  :=
    ( \ h → (\ t → h t , \ t → h t) ,
      ( ( \ (_f , g) t → g t , \ h → refl) ,
        ( ( \ (_f , g) t → g t , \ h → refl))))

Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442 ↩
Instead of builtin layers, Rzk uses CUBE and TOPE universes to separate them from the types. ↩