nLab simplicial type theory

Contents

Contents

Idea

Simplicial type theory (Riehl & Shulman 2017, Β§3) is a homotopy type theory which introduces additional non-fibrant layers on top of Martin-LΓΆf type theory to provide a logical calculus for a directed interval type and with it for geometric shapes, consisting of Segal space-types, Rezk complete-types, and covariant fibrations.

Formal presentations

There are many different ways to formalize the directed interval primitive in simplicial type theory:

With axioms

The directed interval primitive 𝟚\mathbb{2} in simplicial type theory is a non-trivial bounded total order. Bounded total orders have many definitions in mathematics, such as a bounded partial order satisfying totality, or a lattice satisfying totality. As such, there are multiple possible sets of inference rules one could use to present the directed interval in the formalization.

The axiomx for the directed interval primitive (𝟚,≀)(\mathbb{2}, \leq) as a partial order in the formalization are as follows:

Ξ“ctxΞ“βŠ’πŸštypeΞ“ctxΞ“βŠ’0:πŸšΞ“ctxΞ“βŠ’1:πŸšΞ“ctxΞ“,x:𝟚,y:𝟚⊒x≀ytypeΞ“ctxΞ“,x:𝟚,y:πŸšβŠ’Ο„ ≀(x,y):isProp(x≀y)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{2} \; \mathrm{type}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash x \leq y \; \mathrm{type}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \tau_\leq(x, y):\mathrm{isProp}(x \leq y)}
Ξ“ctxΞ“,x:𝟚⊒refl ≀(x):x≀xΞ“ctxΞ“,x:𝟚,y:𝟚,z:𝟚,p:x≀y,q:y≀z⊒trans ≀(x,y,z,p,q):(x≀z)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{refl}_\leq(x):x \leq x} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2}, z:\mathbb{2}, p:x \leq y, q:y \leq z \vdash \mathrm{trans}_\leq(x, y, z, p, q):(x \leq z)}
Ξ“ctxΞ“,x:𝟚,y:𝟚⊒antisym ≀(x,y):isEquiv(idtoleqgeq(x,y))whereidtoleqgeq(x,y):(x= 𝟚y)β†’(x≀y)Γ—(y≀x) idtoleqgeq(x,x)(id 𝟚(x))≔(refl ≀(x),refl ≀(x))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{antisym}_\leq(x, y):\mathrm{isEquiv}(idtoleqgeq(x, y))} \quad \mathrm{where} \quad \begin{array}{l} idtoleqgeq(x, y):(x =_\mathbb{2} y) \to (x \leq y) \times (y \leq x) \\ idtoleqgeq(x, x)(\mathrm{id}_\mathbb{2}(x)) \coloneqq (\mathrm{refl}_\leq(x), \mathrm{refl}_\leq(x)) \end{array}
Ξ“ctxΞ“,x:𝟚,y:𝟚⊒totl ≀(x,y):[(x≀y)+(y≀x)]Ξ“ctxΞ“,x:𝟚⊒bot ≀(x):0≀xΞ“ctxΞ“,x:𝟚⊒top ≀(x):x≀1\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{totl}_\leq(x, y):[(x \leq y) + (y \leq x)]} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{bot}_\leq(x):0 \leq x} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{top}_\leq(x):x \leq 1}
Ξ“ctxΞ“βŠ’nontriv ≀:(0= 𝟚1)β†’πŸ˜\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{nontriv}_\leq:(0 =_\mathbb{2} 1) \to \mathbb{0}}

The axioms for the directed interval primitive 𝟚\mathbb{2} as a lattice in the formalization are as follows:

Ξ“ctxΞ“βŠ’πŸštypeΞ“ctxΞ“βŠ’Ο„ 0:isSet(𝟚)Ξ“ctxΞ“βŠ’0:πŸšΞ“ctxΞ“βŠ’1:πŸšΞ“ctxΞ“,x:𝟚,y:𝟚⊒x∧y:πŸšΞ“ctxΞ“,x:𝟚,y:𝟚⊒x∨y:𝟚\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{2} \; \mathrm{type}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \tau_0:\mathrm{isSet}(\mathbb{2})} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash x \wedge y:\mathbb{2}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash x \vee y:\mathbb{2}}
Ξ“ctxΞ“,x:𝟚⊒idem ∧(x):x∧x= 𝟚xΞ“ctxΞ“,x:𝟚,y:𝟚⊒comm ∧(x,y):x∧y= 𝟚y∧x\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{idem}_\wedge(x):x \wedge x =_{\mathbb{2}} x} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{comm}_\wedge(x, y):x \wedge y =_{\mathbb{2}} y \wedge x}
Ξ“ctxΞ“,x:𝟚,y:𝟚,z:𝟚⊒assoc ∧(x,y,z):(x∧y)∧z= 𝟚x∧(y∧z)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2}, z:\mathbb{2} \vdash \mathrm{assoc}_\wedge(x, y, z):(x \wedge y) \wedge z =_{\mathbb{2}} x \wedge (y \wedge z)}
Ξ“ctxΞ“,x:𝟚⊒lunit ∧(x):1∧x= 𝟚xΞ“ctxΞ“,x:𝟚⊒runit ∧(x):x∧1= 𝟚x\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{lunit}_\wedge(x):1 \wedge x =_{\mathbb{2}} x} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{runit}_\wedge(x):x \wedge 1 =_{\mathbb{2}} x}
Ξ“ctxΞ“,x:𝟚⊒idem ∨(x):x∨x= 𝟚xΞ“ctxΞ“,x:𝟚,y:𝟚⊒comm ∨(x,y):x∨y= 𝟚y∨x\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{idem}_\vee(x):x \vee x =_{\mathbb{2}} x} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{comm}_\vee(x, y):x \vee y =_{\mathbb{2}} y \vee x}
Ξ“ctxΞ“,x:𝟚,y:𝟚,z:𝟚⊒assoc ∨(x,y,z):(x∨y)∨z= 𝟚x∨(y∨z)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2}, z:\mathbb{2} \vdash \mathrm{assoc}_\vee(x, y, z):(x \vee y) \vee z =_{\mathbb{2}} x \vee (y \vee z)}
Ξ“ctxΞ“,x:𝟚⊒lunit ∨(x):0∨x= 𝟚xΞ“ctxΞ“,x:𝟚⊒runit ∨(x):x∨0= 𝟚x\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{lunit}_\vee(x):0 \vee x =_{\mathbb{2}} x} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2} \vdash \mathrm{runit}_\vee(x):x \vee 0 =_{\mathbb{2}} x}
Ξ“ctxΞ“,x:𝟚,y:𝟚⊒asorp ∧(x,y):x∧(x∨y)= 𝟚xΞ“ctxΞ“,x:𝟚,y:𝟚⊒asorp ∨(x,y):x∨(x∧y)= 𝟚x\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{asorp}_\wedge(x, y):x \wedge (x \vee y) =_{\mathbb{2}} x} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{asorp}_\vee(x, y):x \vee (x \wedge y) =_{\mathbb{2}} x}
Ξ“ctxΞ“,x:𝟚,y:𝟚⊒totl(x,y):[(x∧y= 𝟚x)+(x∧y= 𝟚y)]Ξ“ctxΞ“βŠ’nontriv ≀:(0= 𝟚1)β†’πŸ˜\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{totl}(x, y):[(x \wedge y =_{\mathbb{2}} x) + (x \wedge y =_{\mathbb{2}} y)]} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{nontriv}_\leq:(0 =_\mathbb{2} 1) \to \mathbb{0}}

We inductively define the nn-simplices as the following family of types:

  • The 00-simplex is the unit type

    Ξ” 0≔1\Delta^0 \coloneqq \mathbf{1}
  • Let Fin(n)β‰”βˆ‘ i:β„•i<n\mathrm{Fin}(n) \coloneqq \sum_{i:\mathbb{N}} i \lt n be the canonical finite type with nn elements. The n+1n+1-simplex is defined as the type

    n:β„•βŠ’Ξ” n+1β‰”βˆ‘ t:Fin(n+1)β†’πŸšβˆ i:Fin(n)t(Ο€ 1(i+1))≀t(Ο€ 1(i))n:\mathbb{N} \vdash \Delta^{n + 1} \coloneqq \sum_{t:\mathrm{Fin}(n + 1) \to \mathbb{2}} \prod_{i:\mathrm{Fin}(n)} t(\pi_1(i + 1)) \leq t(\pi_1(i))

The first few simplicies can be explicitly written as

Ξ” 1β‰”πŸš\Delta^1 \coloneqq \mathbb{2}
Ξ” 2β‰”βˆ‘ t:Fin(2)β†’πŸšt(1)≀t(0)\Delta^2 \coloneqq \sum_{t:\mathrm{Fin}(2) \to \mathbb{2}} t(1) \leq t(0)
Ξ” 3β‰”βˆ‘ t:Fin(3)β†’πŸš(t(2)≀t(1))Γ—(t(1)≀t(0))\Delta^3 \coloneqq \sum_{t:\mathrm{Fin}(3) \to \mathbb{2}} (t(2) \leq t(1)) \times (t(1) \leq t(0))

Subshapes of the simplicies could also be defined.

  • The boundary of the 11-simplex is defined as

    βˆ‚Ξ” 1β‰”βˆ‘ t:Ξ” 1[(t= Ξ” 10)+(t= 𝟚1)]\partial \Delta^1 \coloneqq \sum_{t:\Delta^1} [(t =_{\Delta^1} 0) + (t =_{\mathbb{2}} 1)]
  • The boundary of the 22-simplex is defined as

    βˆ‚Ξ” 2β‰”βˆ‘ t:Fin(2)β†’πŸš[(t(0)= 𝟚0)Γ—(t(0)≀t(1))+(t(0)= 𝟚t(1))+(t(0)≀t(1))Γ—(t(1)= 𝟚1)]\partial \Delta^2 \coloneqq \sum_{t:\mathrm{Fin}(2) \to \mathbb{2}} [(t(0) =_{\mathbb{2}} 0) \times (t(0) \leq t(1)) + (t(0) =_{\mathbb{2}} t(1)) + (t(0) \leq t(1)) \times (t(1) =_{\mathbb{2}} 1)]

See also

References

A talk on synthetic (infinity,1)-category theory in simplicial type theory and infinity-cosmos theory:

A proof assistant implementing simplicial type theory:

Formalization of the ( ∞ , 1 ) (\infty,1) -Yoneda lemma via simplicial homotopy type theory (in Rzk):

Last revised on August 9, 2024 at 15:40:15. See the history of this page for a list of all contributions to it.