Simplicial Sets & Complete Segal Spaces: A Visual and Interactive Library

Section 2.1 · Notes: Def. 2.1 – Lemma 2.5The simplex category ∆, chain notation, and unique decomposition

Idea: the s's first "compress" the chain (repeats are collapsed — the surjective part), then the d's "skip" the elements missing from the image (the injective part). The d exponents are the elements of [n] not in the image (largest first); the s exponents are the positions j with a_j = a_j+1 (smallest first).

Section 2.1 (cont.) · Notes: Def. 2.7 – Rem. 2.11Simplicial sets and the maps dᵢ, sᵢ

Notation 2.9: For δ : [m] → [n], the corresponding map X(δ) : X_n → X_m is denoted δ^∗. In particular, for dⁱ and sⁱ the corresponding maps are written dᵢ = (dⁱ)^∗ and sᵢ = (sⁱ)^∗. Note: the generators of ∆ carry upper indices (dⁱ, sⁱ), the maps in a simplicial set carry lower indices (dᵢ, sᵢ), and all arrows are reversed: dᵢ : X_n+1 → X_n, sᵢ : X_n−1 → X_n.

Intuition 2.13 (geometric intuition): We imagine X as a recipe for constructing a topological space with a notion of "direction": X₀ is the set of vertices; the non-degenerate elements of X₁ are the edges; the non-degenerate elements of X₂ are the triangles, and so on. The maps d₀, d₁ : X₁ → X₀ specify the source and target of each edge, while d₀, d₁, d₂ : X₂ → X₁ specify the edges forming the boundary of each triangle. Degenerate simplices do not manifest geometrically, but they play an important role (see Section 6, Remark 2.46).

Section 2.2 · Notes: Def. 2.16 – Cor. 2.27The standard simplex Dⁿ: how face and degeneracy maps behave

D⁰, D¹, D² geometrically (Ex. 2.19, 2.22, 2.24 and Intuition 2.21, 2.23, 2.25)

The levels (Example 2.24): D²₀ = {0, 1, 2}, D²₁ = {00, 01, 11, 12, 22, 02}, D²₂ = {000, 001, 011, 111, 112, 122, 222, 002, 022, 012}, ...

Notes: Def. 2.12, Rem. 2.18Degenerate and non-degenerate simplices

Visual explanation: In Dⁿ, if a chain contains a repeat, its geometric carrier collapses onto a lower-dimensional simplex. For example, 001 ∈ D²₂ is a "2-simplex", but since it equals s₀(01) it actually lives flattened on the edge 01; it carries no new geometry. In contrast, 012 is injective — it is the genuine triangle face.

Section 2.3 · Notes: Def. 2.30 – Ex. 2.44Sub-simplicial sets: boundary ∂Dⁿ, horn Lⁿᵢ, spine Spⁿ

Example 2.34: ∂D⁰ = ∅. Example 2.35: ∂D¹ consists of the two vertices {0, 1} and their degenerate simplices (there is no edge 01). Example 2.36: ∂D² is the vertices and the three edges of the triangle; the interior face 012 is absent.

Example 2.38: L¹₀ ≅ L¹₁ ≅ D⁰ (a single vertex). Example 2.39: L²₀ = {edges 01, 02}, L²₁ = {edges 01, 12}, L²₂ = {edges 12, 02} (together with the vertices).

Lemma 2.41: Spⁿ₀ = Dⁿ₀ (all vertices). Lemma 2.42: for k ≥ 2, every element of Spⁿ_k is degenerate (the spine is 1-dimensional). Example 2.43: Sp² ≅ L²₁. Example 2.44: Sp³₁ = {00, 01, 11, 12, 22, 23, 33}.

How Sp³ sits inside D³ (Example 2.44)

Section 2.4 · Notes: Ex. 2.45 – Prop. 2.50How the square is obtained: product and coproduct constructions

Limits and colimits in sSet are computed level-wise: for example (X × Y)_n = X_n × Y_n and (X ⨿ Y)_n = X_n ⨿ Y_n, with face and degeneracy maps acting componentwise.

Coproduct: ∂D¹ ≅ D⁰ ⨿ D⁰ (Lemma 2.47)

A map D⁰ ⨿ D⁰ → ∂D¹ amounts, by Yoneda, to picking two elements of ∂D¹₀ = {0, 1}; the map 0 ⨿ 1 is at every level the bijection {00...0} ⨿ {00...0} → {00...0, 11...1}. So two disjoint points = the boundary of the edge.

Pushout: horns are two edges glued together (Lemma 2.48)

Lemma 2.49: By the same idea, Spⁿ ≅ D¹ ⨿_D⁰ ⋯ ⨿_D⁰ D¹ (n edges glued end to end; Exercise 2.11 by induction).

Product: the square D¹ × D¹ (Example 2.45, Remark 2.46)

The product is also level-wise: (D¹ × D¹)_n = D¹_n × D¹_n; an n-simplex is a pair of chains (α, β). The first three levels:

• (D¹ × D¹)₀ = {(0,0), (0,1), (1,0), (1,1)} — 4 vertices
• (D¹ × D¹)₁ — 9 elements; the non-degenerate ones: (00,01), (11,01), (01,00), (01,11), (01,01) — 4 sides + the diagonal
• (D¹ × D¹)₂ — 16 elements; the non-degenerate ones: (011,001) and (001,011) — two triangles

sHoTT library · 02-simplicial-type-theory.rzk · RS17 §3Rzk counterparts: shapes as topes

In simplicial type theory (RS17), shapes are defined as topes (logical conditions) on cube variables: a point in the cube 2 is a variable t : 2, and a shape is a formula saying which points (t, s, ...) belong to it. The sHoTT-library counterparts of the sSet objects Dⁿ, ∂Dⁿ, L²₁:

Coordinate dictionary: the vertices of Δ² are 0 = (0₂,0₂), 1 = (1₂,0₂), 2 = (1₂,1₂). Edges: s ≡ 0₂ is edge 01, t ≡ 1₂ is edge 12, s ≡ t is the diagonal edge 02. Hence Λ = (edge 01) ∨ (edge 12), which is exactly the inner horn L²₁.

The definitions in the library (02-simplicial-type-theory.rzk.md)

-- Simplices
#def Δ¹ : 2 → TOPE
  := \ t → TOP

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

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

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

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

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

-- Products: the product of topes defines the product of shapes
#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 Δ¹ Δ¹

-- The total boundary of the square
#def ∂□ : ( 2 × 2) → TOPE
  := \ (t , s) → ((∂Δ¹ t) ∧ (Δ¹ s)) ∨ ((Δ¹ t) ∧ (∂Δ¹ s))

-- Vertical / horizontal boundary
#def ∂Δ¹×Δ¹ : ( 2 × 2) → TOPE
  := shape-prod 2 2 ∂Δ¹ Δ¹

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

Face and degeneracy operations in Rzk / RS17 language

In RS17 §3, face and degeneracy operations are λ-terms on extension types: a face is obtained by fixing one coordinate on the boundary; a degeneracy by ignoring a variable. For example, the two degenerate 2-simplices associated to a 1-simplex:

-- degenerate 2-simplices from a 1-simplex (one variable is ignored)
λf. λ⟨t1, t2⟩. f(t1) : (Δ¹ → A) → (Δ² → A)
λf. λ⟨t1, t2⟩. f(t2) : (Δ¹ → A) → (Δ² → A)

-- the four 2-simplex faces of a 3-simplex (0 ≡ t3, t3 ≡ t2, t2 ≡ t1, t1 ≡ 1)
λf. λ⟨t1, t2⟩. f⟨t1, t2, 0⟩  : (Δ³ → A) → (Δ² → A)
λf. λ⟨t1, t2⟩. f⟨t1, t2, t2⟩ : (Δ³ → A) → (Δ² → A)
λf. λ⟨t1, t2⟩. f⟨t1, t1, t2⟩ : (Δ³ → A) → (Δ² → A)
λf. λ⟨t1, t2⟩. f⟨1, t1, t2⟩  : (Δ³ → A) → (Δ² → A)

Compare: on the sSet side, sᵢ repeats an element of the chain; on the Rzk side, the corresponding degeneracy ignores the relevant cube variable (it stays constant). On the sSet side, dⁱ skips an element; on the Rzk side, a face adds a coordinate constraint.

-- RS17, Proposition 3.6
#def Δ²-is-retract-Δ¹×Δ¹
  ( A : U)
  : is-retract-of (Δ² → A) (Δ¹×Δ¹ → A)
  :=
    ( ( \ f → \ (t , s) →
        recOR
          ( t ≤ s ↦ f (t , t)
          , s ≤ t ↦ f (t , s)))
    , ( ( \ f → \ ts → f ts) , \ _ → refl))

Sources: N. Rasekh, ICERM School Notes: Complete Segal Spaces (v0.3), Section 2 · E. Riehl, M. Shulman, A type theory for synthetic ∞-categories (RS17), §3 · the sHoTT library, src/simplicial-hott/02-simplicial-type-theory.rzk.md. All definitions and numbering on this page are taken from these sources.

Section 3.1 · Notes: Def. 3.1 – Prop. 3.4The nerve construction

Visual reading of an n-simplex of NC: a string of n composable morphisms is exactly the data of the spine of an n-simplex whose vertices are the objects x₀, ..., x_n. The rest of the simplex — the edges a₀a₁ with a₁ − a₀ ≥ 2 and the higher faces — is filled in by composites. For n = 2 this is a commuting triangle:

Section 3.1 (cont.) · Notes: Def. 3.5 – Cor. 3.18The Segal condition and Theorem 3.15

Three equivalent readings (Lemma 3.6, Prop. 3.7, Prop. 3.8): by Lemma 3.6 and Yoneda, maps out of the spine are tuples, so the Segal condition says the map X_n → X₁ ×_X₀ ⋯ ×_X₀ X₁ (restricting an n-simplex to its spine edges 01^∗, 12^∗, ..., (n−1)n^∗) is a bijection; equivalently, every map Spⁿ → X extends uniquely along i_n to Dⁿ → X. In words: an n-simplex is exactly a string of n composable edges, with all composites determined.

Proposition 3.9 / Remark 3.11: the infinitely many conditions can be packaged into a single one — i^∗₂ : Map(D², X) → Map(Sp², X) being an isomorphism of simplicial sets (and Sp² ≅ L²₁, so this is a statement about the inner horn). Proposition 3.13: every nerve NC satisfies the Segal condition. Proposition 3.14: N(C × D) ≅ NC × ND.

The proof of Theorem 3.15, visually

Given X Segal, write µ₂ : X₁ ×_X₀ X₁ → X₂ and µ₃ : X₁ ×_X₀ X₁ ×_X₀ X₁ → X₃ for the inverse Segal maps, and build a category C: objects Obj_C = X₀; morphisms Hom_C(x, y) = the fiber of (0^∗, 1^∗) : X₁ → X₀ × X₀ over (x, y); identity id_x = 00^∗(x); composition g ∘ f = 02^∗µ₂(f, g). The category axioms are then read off from well-chosen simplices:

Unitality via degenerate triangles

For f : x → y, the degenerate 2-simplex 001^∗(f) = s₀(f) has faces 01 = id_x, 12 = f, 02 = f; reading off its 02 edge gives f ∘ id_x = 02^∗µ₂(00^∗(x), f) = f. Similarly 011^∗(f) = s₁(f) gives id_y ∘ f = f. (In the notes' proof: f ∘ id_x = 02^∗µ₂(00^∗(x), f) = f and id_y ∘ f = 02^∗µ₂(f, 00^∗(y)) = f.)

Finally, NC ≅ X: NC₀ = X₀ and NC₁ = X₁ by construction, and for n ≥ 2 both NC_n and X_n are identified with the same iterated pullback X₁ ×_X₀ ⋯ ×_X₀ X₁ — NC because nerves are Segal (Prop. 3.13), X by assumption. Remark 3.16: Hom_C(x, y) is recovered from NC as the fiber of (0^∗, 1^∗). Corollary 3.18: N : Cat → sSet_Seg is an equivalence of categories — category theory is the study of Segal simplicial sets.

-- restriction of a 2-simplex to its underlying horn
#def horn-restriction (A : U)
  : ( Δ² → A) → (Λ → A)
  := \ f t → f t

-- Segal types as types local for Λ ⊂ Δ²
#def is-local-horn-inclusion : U → U
  := is-local-type (2 × 2) Δ² (\ t → Λ t)

-- unitality, RS17 Prop 5.8; in ∘ notation this says id_y ∘ f ≃ f
-- (comp-is-segal is written in diagrammatic order: comp ... f g means g ∘ f,
--  so the library calls this the "right unit law"; the mirror case
--  f ∘ id_x ≃ f is id-comp-is-segal)
#def comp-id-is-segal (A : U) (is-segal-A : is-segal A) (x y : A) (f : hom A x y)
  : ( comp-is-segal A is-segal-A x y y f (id-hom A y)) = f

-- associativity, RS17 Prop 5.9
#def associative-is-segal (A : U) (is-segal-A : is-segal A) (w x y z : A)
  ( f : hom A w x) (g : hom A x y) (h : hom A y z)
  : ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
  = ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h))

Section 3.2 · Notes: Def. 3.19 – Prop. 3.36From algebraic topology: homotopy, CW-complexes, the topological simplex, Sing

Section 3.2 (cont.) · Notes: Def. 3.37 – Rem. 3.46Kan complexes, π₀, and the homotopy theorem

Proposition 3.38: For every topological space X, Sing(X) is a Kan complex — |Lⁿ_k| is a retract of |Dⁿ|, so continuous horns always fill. This gives a functor Sing : Top → Kan (Def. 3.39), which is not an equivalence of categories, but becomes one after passing to homotopy.

Lemma 3.42: π₀(Sing(X)) ≅ π₀(X) — vertices of Sing(X) are points, edges are paths, so the simplicial π₀ recovers path-components. Combined with Def. 3.43 (Ho(Top_CW)) and Def. 3.44 (Ho(Kan)):

Remark 3.46: one consequence is the 2-out-of-3 property for homotopy equivalences of Kan complexes: if two of f, g, g ∘ f are homotopy equivalences, so is the third.

Section 4 · Notes: Def. 4.2 – Lemma 4.14Two directions: simplicial spaces and the bisimplicial grid

Section 6 · Notes: Def. 6.1 – Ex. 6.11Reedy fibrancy: making the vertical direction spatial

The spatial direction of a simplicial space should behave like spaces, i.e. Kan complexes. But a naive level-wise Kan condition is not enough: the Segal condition will be a statement about pullbacks like X₁ ×_X₀ X₁, and, as Section 5 shows (Lemma 5.12), such pullbacks behave homotopy-invariantly when the maps 0^∗, 1^∗ : X₁ → X₀ are Kan fibrations. Reedy fibrancy packages exactly this dependency.

What Reedy fibrancy buys, on the grid (Examples 6.3 – 6.5): every column X_n is a Kan complex; the map (0^∗, 1^∗) : X₁ → X₀ × X₀ is a Kan fibration (so its fibers — the future mapping spaces — are Kan complexes, and pullbacks over X₀ are homotopy invariant); more generally (0^∗, ..., n^∗) : X_n → (X₀)ⁿ⁺¹ is a Kan fibration.

disc always works, const usually fails. Proposition 6.8: disc(A) is Reedy fibrant for every simplicial set A — the mapping spaces Map(∆ⁿ, disc A) and Map(∂∆ⁿ, disc A) are constant simplicial sets (Lemmas 6.6, 6.7), and any map between constant simplicial sets is a Kan fibration (Lemma 5.26). In particular ∆ⁿ, ∂∆ⁿ, Sp_n are Reedy fibrant (Example 6.9). On the const side, even a Kan complex can fail:

Section 5 · Notes: Def. 5.6 – Ex. 5.28Kan fibrations: dependent spaces

Why fibrations? Pullbacks of Kan complexes are not homotopy invariant. Example 5.5 is the smallest possible failure: replace N(I(1)) by the equivalent D⁰ and the pullback jumps from ∅ to a point.

Section 7 · Notes: Def. 7.1 – Rem. 7.16Uniqueness vs. contractibility

Local vs. global, and why fibrancy is needed. For sets, a map is a bijection iff every pre-image is a singleton (Lemma 7.7): global uniqueness = local uniqueness at every point (Intuition 7.8). The naive homotopical analogue is false — Example 7.9: 0 : D⁰ → N(I(1)) is a homotopy equivalence, but the pre-image of the vertex 1 is ∅, which is not contractible (Exercise 7.9). Global equivalence does not see the fibers unless the map is a fibration:

Horn filling vs. boundary filling

The two lifting conditions of this module, side by side, at n = 2: a Kan fibration fills horns (one boundary face missing — existence of composites, inverses, ...); a trivial fibration fills boundaries (only the interior missing — any already-given candidate boundary is realized, which is where uniqueness-up-to-homotopy comes from).

Section 8 · Notes: Def. 8.2 – Lemma 8.26Segal spaces: composition as a contractible choice

Reedy fibrancy (section 13) makes a simplicial space behave like a space vertically; now we make it behave like a category horizontally. The key property was the Segal condition (Theorem 3.15) — here is its homotopical analogue.

Section 8 (cont.) · Notes: Def. 8.31 – Prop. 8.45Identities, the homotopy category, and the Rzk dictionary

The associativity picture is the homotopical upgrade of the tetrahedron from section 9: lift the triple (f, g, h) along the equivalence to a 3-cell σ in map_T(x, y, z, w); restricting along 013 computes (h∘g)∘f, restricting along 023 computes h∘(g∘f), and both land on the same 03-edge of the same σ.

-- identity = degenerate arrow             (Def 8.31: id_x = 00*(x))
id-hom

-- unit law, RS17 Prop 5.8                 (Prop 8.33: id_y ∘ f ≃ f)
--   comp-is-segal is diagrammatic: comp ... f g = g ∘ f
--   the mirror case f ∘ id_x ≃ f is id-comp-is-segal
comp-id-is-segal

-- associativity, RS17 Prop 5.9            (Prop 8.33: (h∘g)∘f ≃ h∘(g∘f))
associative-is-segal

Section 9 · Notes: Def. 9.2 – Lemma 9.10Homotopy equivalences in Segal spaces

The hidden data (Intuition 9.4): the definition looks like "three maps exist", but in a Segal space each homotopy to an identity is carried by a witnessing 2-cell. What the definition really provides is two filled triangles:

Exercise 9.1 records where these witnesses live: the right-inverse triangle is a point of a pullback of map_T(y, x, y), the left-inverse triangle of map_T(x, y, x).

Lemma 9.5: any left inverse h and any right inverse g of f agree up to homotopy — the classical chain g ≃ id_x ∘ g ≃ (h ∘ f) ∘ g ≃ h ∘ (f ∘ g) ≃ h ∘ id_y ≃ h, run entirely with Prop. 8.33 (in sHoTT this is RS17 Prop. 10.1).

Section 9 (cont.) · Notes: Def. 9.31 – Lemma 9.46Property vs. structure: the space of equivalences

Theorem 9.43: the forgetful map P_forgchoice : T_hoeqchoice → T_hoequiv is a homotopy equivalence — forgetting the chosen inverses loses nothing; the choice is homotopically unique.

-- one two-sided inverse iff separate left and right inverses  (RS17 Prop 10.1 = Lemma 9.5)
#def inverse-iff-iso-arrow
  : iff (has-inverse-arrow A is-segal-A x y f) (is-iso-arrow A is-segal-A x y f)

-- being an isomorphism is a proposition  (RS17 Prop 10.2 = Thm 9.43 + Prop 9.40)
#def is-prop-is-iso-arrow
  : is-prop (is-iso-arrow A is-segal-A x y f)

Section 10 · Notes: Ex. 10.1 – Ex. 10.14Why Segal spaces are not enough: E(1)

The problem, in one example. Let E(1) := disc(N(I(1))) (Notation 10.3). The functor 0 : [0] → I(1) is an equivalence of categories — yet ∆⁰ → E(1) is not an equivalence of Segal spaces: by Lemma 8.41 it would make {0} → E(1)₀ = {0, 1} a homotopy equivalence of spaces, which it is not (Example 10.4). The two directions of E(1) disagree:

Section 10 (cont.) · Notes: Def. 10.15 – Thm. 10.44Completeness: gluing the two directions together