Modalities (experimental)¶

#lang rzk-1

Rzk's modal extension supports reasoning in the style of Triangulated Type Theory (TTT), introduced by Gratzer, Weinberger, and Buchholtz¹ as an enrichment of simplicial type theory with modalities \(\flat\), \(\sharp\), and \(op\). The extension was implemented 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. It ships with Rzk v0.8 and remains experimental.

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 an experimental extension shipped in Rzk v0.8. The surface syntax and the mode theory may still change in future releases.

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

  flat -->|"coe"| op
  op  -->|"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`¶

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, double-op uses let mod to define the modal composition \(\langle \text{op} | \langle \text{op} | A \rangle \rangle \to A\), since \(\text{op} \cdot \text{op} = id\):

#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 :µ A) bind the variable x directly under modality µ with type A. This is a first-class modal binding — the variable x is accessible according to the coercion rules of µ. Modal bindings are 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) → let mod ♭ bx := x in mod ♭ (f bx)

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) → let mod ♭ bx := x in mod ♭ (f bx)

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

#def op-map (A B :ᵒᵖ U) (f :ᵒᵖ A → B)
  : ᵒᵖ A → ᵒᵖ B
  := \ (x : ᵒᵖ A) → let mod ᵒᵖ opx := x in mod ᵒᵖ (f opx)

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

#def sharp-map (A B : U) (f : A → B)
  : ♯ A → ♯ B
  := \ (x : ♯ A) → let mod ♯ sx := x in mod ♯ (f sx)

#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 A 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)

Known unsoundness footgun: don't postulate `√` on `2`¶

Do not postulate √ ("2 is tiny") on the cube 2

When formalizing Triangulated Type Theory¹, the natural-looking next step after introducing modalities is to postulate the amazing right adjoint √ to the path-space functor (2 → −) — equivalently, the assertion that the directed interval 2 is tiny. This is unsound on the standard RS17 model.

The reason is structural. In the standard simplicial-set model PSh(∆), the directed interval is realized by the representable y([1]), and (−)^I has no right adjoint — concretely, exponentiation by y([1]) does not preserve pushouts (see Gratzer–Weinberger–Buchholtz §1.3 and §3, footnote 7). Rzk's cube 2 inherits exactly that totally-ordered structure, so postulating √ on 2 — or any is-tiny(2) formulation — contradicts the model.

The planned 𝕀 primitive — a bounded distributive lattice cube, per GWB §1.3 — is the sound place to postulate √. Until 𝕀 ships, TT⊲ formalizations with √-on-2 can potentially be unsound (if the underlying tope solver ever relies on the total order).

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.

Gratzer, Weinberger & Buchholtz — Directed univalence in simplicial homotopy type theory (TTT)
Talipov & Kudasov — Towards Formalization of Directed Univalence in Rzk proof assistant — HoTT/UF 2026 contributed talk on this extension
sHoTT diruniv — formalizations using Rzk modalities
Introduction — cube, tope, and type layers
Dependent types — functions, sums, and identity types without modalities

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 ↩↩
Islam Talipov and Nikolai Kudasov. Towards Formalization of Directed Univalence in Rzk proof assistant. Contributed talk, HoTT/UF 2026. https://hott-uf.github.io/2026/abstracts/HoTTUF_2026_paper_22.pdf ↩

Modalities (experimental)¶

Modalities in Rzk¶

Modal types and introduction¶

Modal let mod¶

Modal bindings¶