Skip to content

Modalities (experimental)

#lang rzk-1

Rzk’s modal extension supports reasoning in the style of Triangulated Type Theory (TTT), introduced by Gratzer, Weinberger, and Buchholtz1 as an enrichment of simplicial type theory with modalities \(\flat\), \(\sharp\), and \(op\). The extension is implemented on branch lishy2-modal by Islam Talipov, using a parameterized mode theory (composition and coercion of modes) layered on top of Rzk’s existing cube, tope, and type layers.

Formalizations that use this syntax include the sHoTT diruniv branch, in particular modal API examples and a development of directed univalence (17-diruniv.rzk).

Experimental

Modalities are not yet on the main develop branch or in published Rzk releases. Build Rzk from lishy2-modal to typecheck examples on this page.

Modalities in Rzk

Currently Rzk supports 3 modalities:

Description ASCII syntax Unicode syntax
Discretization _b ♭
Codiscretization _# ♯
Reverses orientation of arrows _op ᵒᵖ
Identity _id —

Modalities compose according to a fixed mode theory (for example, _op/_op reduces to _id). Not every pair of modalities coerces into one another; the typechecker tracks which variables are accessible under the current modal context.

graph TB
  flat["♭  flat"]
  id["𝑖𝑑  identity"]
  sharp["♯  sharp"]
  op["ᵒᵖ  opposite"]

  flat -->|"coe"| id
  id  -->|"coe"| sharp
  id ~~~ op

♭ is idempotent and absorbing

\({\flat} \cdot {\flat} = {\flat}\)   \({\flat} \cdot {\sharp} = {\flat}\)

\({op} \cdot {\flat} = {\flat}\)   \({\flat} \cdot {op} = {\flat}\)

♯ is idempotent and absorbing

\({\sharp} \cdot {\sharp} = {\sharp}\)   \({\sharp} \cdot {\flat} = {\sharp}\)

\({\sharp} \cdot {op} = {\sharp}\)   \({op} \cdot {\sharp} = {\sharp}\)

op is involutive

\({op} \cdot {op} = {id}\)

A type in modality µ is written <| µ | A |>, where A is checked under µ. A term of that type is introduced with mod µ t, where t is checked in a context “under” modality µ:

#def sharp-pure₁ (A : U) (x : A)
  : <| ♯ | A |>
  := mod ♯ x

This works for _# because there is a coercion id → _#, so any variable accessible under id (i.e. any ordinary variable) is also accessible under _#. For _b there is no such coercion, so the analogous definition is ill-typed:

-- ill-typed
#def bad-flat-pure (A : U) (x : A)
  : <| _b | A |>
  := mod _b x

Modal let mod is the elimination principle for modal types. Modal bindings use let mod ext/inn x := value in body, where:

  • value is checked against <| inn | T |> under an ext-lock
  • body is checked with x \(:^{ext \cdot inn}\) T in context

If ext is omitted, let mod m x := value in body is sugar for let mod _id/m x := value in body.

It can be seen as a pattern-match on mod in the binder. For example, flat-extract is the opposite of sharp-pure — it is definable precisely because there is a coercion \(\flat \Rightarrow id\):

#def flat-extract (A : <| ♭ | U |>) (x : let mod ♭ Ab := A in <| ♭ | Ab |>)
  : let mod ♭ Ab := A in Ab
  := let mod ♭ xb := x in xb

Using let mod you can define the modal сomposition \(\langle \mu | \langle \nu | A \rangle \rangle \to \langle \mu \cdot \nu | A \rangle\). A concrete example is double-op:

#def double-op (A : U) (x : <| ᵒᵖ | <| ᵒᵖ | A |> |>)
  : A
  :=
  let mod ᵒᵖ x_1 := x in
  let mod ᵒᵖ / ᵒᵖ x_2 := x_1 in
  x_2

Modal parameter annotations (x : m A) are syntactic sugar that makes definitions look less verbose than the raw let mod form. A parameter (x : _b A) -> ... desugars to (_a : <| _b | A |>) → let mod _b x := _a in …. This sugar is available in λ-abstractions, Π- and Σ-types, and definition argument lists.

For example, b-extract and b-map written with modal bindings are much cleaner than the explicit let mod version shown above:

#def b-extract₁ (A : ♭ U) (x : ♭ A)
  : A
  := x

#def b-map₁ (A B : ♭ U) (f : ♭ A → B)
  : <| ♭ | A |> → <| ♭ | B |>
  :=
  \ (x : ♭ A) → mod ♭ (f x)

S4-like combinators

Below is a small self-contained example of modal syntax. The combinators follow the S4-style structure: each modality comes with extract/map/join operations where the mode theory allows it. Note that ♭ carries a comonadic structure (b-extract, b-map, b-dup), while ♯ carries a monadic structure (sharp-pure, sharp-map, sharp-join).

#def b-extract (A : ♭ U) (x : ♭ A)
  : A
  := x

#def b-map (A B : ♭ U) (f : ♭ A → B)
  : <| ♭ | A |> → <| ♭ | B |>
  := \ (x : ♭ A) → mod ♭ (f x)

#def b-dup (A : ♭ U) (x : ♭ A)
  : <| ♭ | <| ♭ | A |> |>
  := mod ♭ (mod ♭ x)

#def op-map (A B : ᵒᵖ U) (f : ᵒᵖ A → B)
  : <| ᵒᵖ | A |> → <| ᵒᵖ | B |>
  := \ (x : ᵒᵖ A) → mod ᵒᵖ (f x)

#def sharp-pure (A : U) (x : A)
  : <| ♯ | A |>
  := mod ♯ x

#def sharp-map (A B : U) (f : A → B)
  : <| ♯ | A |> → <| ♯ | B |>
  := \ (x : ♯ A) → mod ♯ (f x)

#def sharp-join (A : U) (a : <| ♯ | <| ♯ | A |> |>)
  : <| ♯ | A |>
  :=
  let mod ♯ x_1 := a in
  let mod ♯ / ♯ x_2 := x_1 in
  mod ♯ x_2

How the typechecker uses modalities

Modalities not only introduce modal types but also impose constraints on how variables can be introduced and used.

  • Every mod m … or <| m | … |> expression places an m-lock (a lock annotated with modality \(m\)) on the current context.
  • let mod ext/inn x := value in body introduces x as a modality-parametrized binding with modality \(ext \cdot inn\).
  • A variable bound under modality \(\mu\) can only be used when the accumulated lock \(\hat{m}\) — the composition of all m-locks placed between the binding site and the use site — is \(\mu\)-coercible, i.e. there exists a coercion from \(\mu\) to \(\hat{m}\).

If a variable's modality cannot be coerced into the current lock accumulator, the typechecker reports:

unaccessible var with modality … under locks …

Modalities at tope level

Inversion of arrows with op

Modalities are also available at the cube and tope layers. Their mechanics are the same as for modal types at the dependent type layer. Additionally, there are operators for inverting cubes and topes.

The equivalence between 2 and <| _op | 2 |> is witnessed by flipᵒᵖ and unflipᵒᵖ. In particular, flipᵒᵖ 0₂ reduces to mod _op 1₂ and vice versa.

The equivalence between TOPE and <| _op | TOPE |> is witnessed by invᵒᵖ and uninvᵒᵖ, which reverse the direction of inequalities.

Here is an example of a function that reverses the direction of a morphism using the _op modality:

#def op-hom-to-hom
  ( B : _op U)
  ( x : _op B)
  ( y : _op B)
  ( h : _op (t : 2) → B [ t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y ])
  : ( ( t : 2) → <| _op | B |> [ t ≡ 0₂ ↦ mod _op y , t ≡ 1₂ ↦ mod _op x ])
  := \ t → let mod _op s := flipᵒᵖ t in mod _op (h s)

Discrete interval elimination

The discrete interval <| _b | 2 |> can be treated as a Boolean type. A crisp point of 2 is either 0₂ or 1₂, so we can eliminate by cases:

#def discrete-2-elim (i : _b 2) (A : U) (x y : A) : A :=
  recOR(
    (i === 0_2) |-> x,
    (i === 1_2) |-> y)

Axioms and larger formalizations

Many principles of TTT are not built into Rzk as primitive rules; they are introduced as #postulate in libraries. On the sHoTT diruniv branch, examples include crisp induction for _b and axioms for the directed interval modality. The directed-univalence development in 17-diruniv.rzk is the reference corpus for how modal syntax is used at scale; this page does not reproduce that proof.

  1. Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz. Directed univalence in simplicial homotopy type theory. arXiv:2407.09146, 2024 (revised 2026). https://arxiv.org/abs/2407.09146 ↩