An Agda Formalisation of a Graded Modal Type Theory with First-Class Universe Levels and Erasure

This code is related to the paper “Normalisation for First-Class Universe Levels”, Nils Anders Danielsson, Naïm Camille Favier and Ondřej Kubánek, Proceedings of the ACM on Programming Languages, Volume 10, Issue POPL, 2026 (doi:10.1145/3776645). It builds on an existing formalisation, see “Project history” below.

Dependencies and licences

The code depends on some libraries:

• Agda’s standard library, version 2.3 (licence).
• The builtin modules that are shipped with Agda 2.8.0 (licence).

When HTML code is generated from this file code is also generated for the two libraries above, so links (which are up-to-date at the time of writing) to their licences are included above.

The licence for this project can be found in the file LICENSE.

Type-checking

To type-check everything in the formalisation, including this file, you can run the following command (assuming that agda refers to a suitable version of Agda set up with a suitable version of its standard library):

agda Everything.agda

The file graded-type-theory.agda-lib includes the flag --safe, which disallows things like postulates, turning off the termination checker, and so on.

Project history

This formalisation originated as a fork of logrel-mltt. That work consisted of the following contributions:

• “A Logical Relation for Martin-Löf Type Theory in Agda”, code mostly written by Joakim Öhman in 2016 as part of a master’s thesis supervised by Andrea Vezzosi and Andreas Abel.

  That development is described in the article “Decidability of Conversion for Type Theory in Type Theory”, Andreas Abel, Joakim Öhman and Andrea Vezzosi, Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL, 2017 (doi:10.1145/3158111).

• The empty type was added by Gaëtan Gilbert (2018).

• A unit type and Σ-types were added by Wojciech Nawrocki (2021).

• The code was refactored to use well-scoped syntax by Oskar Eriksson (2021).

The formalisation was lifted to graded modal type theory: this is the basis of the paper “A Graded Modal Type Theory with a Universe and Erasure, Formalized”, Andreas Abel, Nils Anders Danielsson and Oskar Eriksson, Proceedings of the ACM on Programming Languages, Volume 7, Issue ICFP, 2023 (doi:10.1145/3607862).

Later other additions were made:

• Identity types were added by Nils Anders Danielsson (2023).

• A weak unit type was added by Oskar Eriksson (2023).

• A universe hierarchy with first-class universe levels was added by Nils Anders Danielsson, Naïm Camille Favier and Ondřej Kubánek (2024-2025): this is the focus of the discussion below.

Note also that some changes to the code were made after feedback from anonymous reviewers.

Pointers to code for specific definitions, theorems etc. in the paper

module README where

Below pointers to code are included for all the main definitions, theorems, etc. in the paper, along with some discussion of differences between the paper and the code.

Note that if HTML has been generated from this file in a suitable way using agda --html, then names in import statements below should be linked to the corresponding definitions.

2: A Type Theory with First-Class Universe Levels

2.1: Syntax

import Graded.Modality.Instances.Unit
  using (UnitModality)

import Definition.Untyped
  using (Term; sucᵘᵏ; ↓ᵘ_)

import Definition.Untyped
  using (Con)

import Definition.Untyped
  using (_[_])

import Definition.Untyped
  using (wk; step; id; wk1)
import Definition.Typed.Weakening
  using (_∷ʷ_⊇_; wk₁; wkTerm₁)

2.2: Typing Rules

import Definition.Typed.Restrictions
  using (Type-restrictions)

It is also possible to restrict the Level type so that it is not an element of a universe, or not allowed at all. There is a parameter level-support that can take one of the following three values:

• only-literals: The Level type is disallowed, and only level literals are allowed.

• level-type small: The Level type is allowed and has type U zeroᵘ. If this setting is used, then the type Level-is-small is inhabited.

• level-type not-small: The Level type is allowed, but does not belong to the first (or any) universe. If this setting is used, then the type Level-is-not-small is inhabited.

open Definition.Typed.Restrictions.Type-restrictions
  using
    (level-support; Level-is-small; Level-is-not-small; Level-allowed)

import Definition.Typed.Properties.Admissible.Level
  using (⊢Id-Level; ¬Level-is-small→¬Level∷U)

import Definition.Typed
  using
    (⊢_; _⊢_; _⊢_≡_; _⊢_∷_; _⊢_≡_∷_; _∷_∈_; _⊢_≤_∷Level;
     _⊢_∷Level; _⊢_≡_∷Level)

import Definition.Typed.Properties.Admissible.Level
  using (⊢≤-refl; ⊢≤-trans; ⊢≤-antisymmetric; supᵘ-zeroʳⱼ)

import Definition.Typed.Properties.Admissible.Lift
  using (Liftⱼ≤)

import Definition.Typed.Consequences.Universe
  using (the-type-of-id-does-not-have-a-type; type-without-type)

import Definition.Typed.Properties.Admissible.Pi-Sigma
  using (⊢ΠΣʰ; ΠΣʰ-cong-⊢; ⊢ΠΣʰ∷; ΠΣʰ-cong-⊢∷)
import Definition.Typed.Properties.Admissible.Pi
  using (⊢lamʰ; ⊢∘ʰ; app-congʰ; β-redʰ; η-eqʰ)
import Definition.Typed.Properties.Admissible.Sigma
  using
    (⊢prodʰ; prodʰ-cong;
     ⊢fstʰ; ⊢sndʰ; fstʰ-cong; sndʰ-cong; Σʰ-β₁; Σʰ-β₂; Σʰ-η;
     ⊢prodrecʰ⟨⟩; prodrecʰ⟨⟩-cong; prodrecʰ⟨⟩-β)

import Definition.Typed.Consequences.Inequality
  using (¬ℕ∷U-sucᵘ)

2.3: Reduction Rules

import Definition.Typed
  using (_⊢_⇒_∷_; _⊢_⇒*_∷_; _⊢_⇒_; _⊢_⇒*_)

import Definition.Untyped.Neutral
  using (Neutral; Neutralˡ; Whnf)

import Definition.Typed.Properties
  using (wf; wfEq; wfTerm; wfEqTerm)
import Definition.Typed.Well-formed
  using (wf-⊢≡; wf-⊢∷; wf-⊢≡∷)
import Definition.Typed.Syntactic
  using (syntacticRed; syntacticRedTerm)

3: A Logical Relation

import Definition.Untyped.NotParametrised
  using (Universe-level)

open import Definition.Typed.EqualityRelation
  using (EqRelSet)
open EqRelSet
  using (Neutrals-included)

import Definition.Typed.EqRelInstance
  using (eqRelInstance)

3.1: Reducible Levels and Neutrals

import Definition.LogicalRelation.Unary
  using (_⊩neNf_∷_; ⊩neNf∷⇔⊩neNf≡∷)
import Definition.LogicalRelation
  using
    (_⊩neNf_≡_∷_;
     _⊩Level_∷Level; _⊩Level_≡_∷Level;
     Level-prop; [Level]-prop;
     neLevel-prop; [neLevel]-prop)

import Definition.LogicalRelation.Properties.Whnf
  using (level; nelevel; lsplit; nelsplit)

import Definition.LogicalRelation
  using (↑ⁿ_; ↑ᵘ_)

import Definition.LogicalRelation.Properties.Primitive
  using (↑ⁿ-respects-⇒*; ↑ⁿ-zeroᵘ; ↑ⁿ-sucᵘ; ↑ⁿ-supᵘ′; ↑ⁿ-ne; ↑ⁿ-unique)

import Definition.LogicalRelation.Properties.Primitive
  using
    (↑ⁿ-irrelevance; ↑ᵘ-irrelevance;
     ↑ⁿ-cong; ↑ᵘ-cong;
     ↑ⁿ-cong-≤; ↑ᵘ-cong-≤)

import Definition.LogicalRelation.Properties.Primitive
  using (⊩supᵘ-congˡ)

import Definition.LogicalRelation.Properties.Primitive
  using (⊩supᵘ)

import Definition.LogicalRelation.Properties.Primitive
  using (⊩supᵘ-idem)

import Definition.LogicalRelation.Properties.Primitive
  using (⊩Level-⇒*; redLevel′)

3.2: Reducibility

import Definition.LogicalRelation
  using (_⊩⟨_⟩_; _⊩⟨_⟩_≡_/_; _⊩⟨_⟩_≡_∷_/_; _⊩⟨_⟩_∷_/_)

import Definition.LogicalRelation.Properties.Embedding
  using (emb-≤-⊩; emb-≤-⊩≡; emb-≤-⊩≡∷; emb-≤-⊩∷)

import Definition.LogicalRelation
  using (_⊩ne_; _⊩ne_≡_/_; _⊩ne_≡_∷_/_)

import Definition.LogicalRelation
  using (_⊩Level_; _⊩Level_≡_; _⊩Level_≡_∷Level)

import Definition.LogicalRelation.Properties.Primitive
  using (reflLevel; wf-Level-eq)

open import Definition.LogicalRelation
  using (module LogRel)
open LogRel
  using (_⊩₁U_; _⊩₁U≡_/_; _⊩₁U_≡_∷U/_)

import Definition.Untyped.Neutral
  using (Type)

open LogRel
  using (_⊩ₗLift_; _⊩ₗLift_≡_/_; _⊩ₗLift_≡_∷_/_)

open LogRel
  using (_⊩ₗB⟨_⟩_; _⊩ₗB⟨_⟩_≡_/_; _⊩ₗΠ_≡_∷_/_)

import Definition.LogicalRelation.Weakening.Restricted
  using (_∷ʷʳ_⊇_; ∷ʷ⊇→∷ʷʳ⊇; ∷ʷʳ⊇→∷ʷ⊇)

import Definition.Untyped.NotParametrised
  using (lift)
import Definition.Typed.Weakening
  using (liftʷ)

import Definition.LogicalRelation.Irrelevance
  using (irrelevanceEq; irrelevanceEqTerm; irrelevanceTerm)

import Definition.LogicalRelation.Hidden
  using (_⊩⟨_⟩_∷_; _⊩⟨_⟩_≡_∷_; _⊩⟨_⟩_≡_)

3.3 Validity and the Fundamental Lemma

import Definition.LogicalRelation.Properties.Escape
  using (escape; escapeEq; escapeTerm; escapeTermEq)

import Definition.LogicalRelation.Substitution
  using
    (⊩ᵛ_; _⊩ᵛ⟨_⟩_; _⊩ᵛ⟨_⟩_≡_; _⊩ˢ_∷_; _⊩ˢ_≡_∷_; _⊩ᵛ⟨_⟩_∷_; _⊩ᵛ⟨_⟩_≡_∷_;
     _⊩ᵛ⟨_⟩_∷Level; _⊩ᵛ⟨_⟩_≡_∷Level; ⊩ᵛ∷L⇔; ⊩ᵛ≡∷L⇔)

import Definition.LogicalRelation.Fundamental
  using
    (valid;
     fundamental-⊩ᵛ; fundamental-⊩ᵛ≡; fundamental-⊩ᵛ∷; fundamental-⊩ᵛ≡∷)

import Definition.LogicalRelation.Substitution.Introductions.Universe
  using (⊩ᵛU∷U)

import Definition.LogicalRelation.Substitution.Introductions.Universe
  using (⊩ᵛ∷U→⊩ᵛ)

import Definition.LogicalRelation.Substitution.Introductions.Lift
  using (Liftᵗᵛ)

import Definition.LogicalRelation.Substitution.Introductions.Pi-Sigma
  using (ΠΣᵗᵛ)

import Definition.LogicalRelation.Weakening
  using (wk-↑ⁿ; wk-↑ᵘ)

import Definition.LogicalRelation.Fundamental.Reducibility
  using (reducible-⊩; reducible-⊩≡; reducible-⊩∷; reducible-⊩≡∷)

import Definition.LogicalRelation.Substitution
  using (⊩ˢ∷-idSubst)

import Definition.LogicalRelation.Properties.Neutral

import Definition.Typed.Consequences.Canonicity
  using (¬Empty)

import Definition.Typed.Consequences.Canonicity
  using (canonicity)

import Definition.Typed.Consequences.Reduction
  using (whNorm; whNormTerm)

import Definition.Typed.Consequences.Injectivity
  using
    (U-injectivity; Lift-injectivity;
     ΠΣ-injectivity-no-equality-reflection)
import Definition.Typed.Consequences.Inequality
  using (Level≢ℕ; U≢ℕ)

import Definition.Typed.Consequences.Canonicity
  using (canonicity-Only-Level-or-U)

4: Decidability of Equality

Algorithmic equality. The conversion relations are denoted as follows:

• Γ ⊢ A [conv↑] B and Γ ⊢ A [conv↓] B for arbitrary types and types in WHNF, respectively,

• Γ ⊢ t [conv↑] u ∷ A and Γ ⊢ t [conv↓] u ∷ B for arbitrary terms with arbitrary types, and terms in WHNF with types in WHNF, respectively, and

• Γ ⊢ t ~ u ↑ A and Γ ⊢ t ~ u ↓ A for atomic neutral terms and atomic neutral terms with types in WHNF, respectively.

import Definition.Conversion
  using
    (_⊢_[conv↑]_; _⊢_[conv↓]_; _⊢_[conv↑]_∷_; _⊢_[conv↓]_∷_;
     _⊢_~_↑_; _⊢_~_↓_)

import Definition.Conversion
  using (LevelAtom; Level⁺; Levelᵛ)

import Definition.Conversion
  using (_≡ᵛ_; ≤ᵛ; ≤⁺ᵛ; ≤⁺; ≤ᵃ)

import Definition.Conversion
  using (sucᵛ; supᵛ)

import Definition.Conversion
  using (_⊢_↑ᵛ_; _⊢_↓ᵛ_; _⊢_~ᵛ_)

import Definition.Conversion.Soundness
  using
    (soundnessConv↑; soundnessConv↓;
     soundnessConv↑Term; soundnessConv↓Term;
     soundness~↑; soundness~↓)

import Definition.Conversion.Weakening
  using (wkConv↑; wkConv↓; wkConv↑Term; wkConv↓Term; wk~↑; wk~↓)

import Definition.Conversion.Decidable
  using (decConv↑; decConv↓; decConv↑Term; decConv↓Term; dec~↑; dec~↓)

import Definition.Conversion.Level
  using (deterministic-↑ᵛ)

open import Definition.Conversion.EqRelInstance
  using (module Lemmas)
open Lemmas
  using (supᵘ-↑ᵛ)

import Definition.Conversion.EqRelInstance
  using (eqRelInstance)

import Definition.Conversion.Consequences.Completeness
  using (completeEq; completeEqTerm)

import Definition.Typed.Decidable.Equality
  using (decEq; decEqTerm)

import Definition.Conversion.FullReduction
  using (fullRed; fullRedTerm)

import Definition.Typechecking
  using (Checkable-type; Checkable; Inferable; Checkable-level)

import Definition.Typechecking
  using (Checkable-type׬Checkable; ⊢→Checkable-type→Inferable)

import Definition.Typed.Decidable
  using (decWfCon; decConTypeᶜ; decConTermTypeᶜ; decConTermᵢ)

5: Erasing Levels Is Safe

import Graded.Usage
  using (_▸[_]_)
import Graded.Usage.Restrictions
  using (Usage-restrictions)

import Graded.Context
  using (Conₘ)

import Graded.Mode
  using (Mode)

import Graded.Modality.Instances.Erasure
  using (𝟘; ω)
import Graded.Modality.Instances.Erasure.Modality
  using (ErasureModality)

import Graded.Erasure.Target
  using (Term; Strictness; Value; Value⟨_⟩; _⇒_; suc⟨_⟩; sucᵏ)
import Definition.Untyped
  using (sucᵏ)
import Graded.Erasure.Target.Non-terminating
  using (loop)
import Graded.Erasure.Extraction
  using (loop?)
import Graded.Erasure.SucRed
  using (_⇒ˢ_; _⊢_⇒ˢ_∷ℕ; _⊢_⇒ˢ*_∷ℕ; _⇒ˢ⟨_⟩*_)

import Graded.Erasure.Extraction
  using (erase)

import Graded.Erasure.Extraction.Non-terminating
  using (loops-reduces-forever; ⊢loops; ▸loops)

open import Graded.Erasure.Consequences.Soundness
open Soundness
  using (soundness-ℕ)

open Soundness₀
  using (soundness-ℕ)

import Graded.Erasure.Consequences.Soundness using
  (soundness-ℕ-only-source-counterexample₁; soundness-ℕ-counterexample₆)

6: Discussion and Future Work

open import Definition.Conversion
  using (module _⊢_[conv↓]_∷_)
open _⊢_[conv↓]_∷_
  using (Lift-η)
import Definition.Conversion.Conversion
  using (convConv↑Term; convConv↓Term)
import Definition.Conversion.Lift
  using (lift~toConv↓)

More pointers to code

import Graded.Erasure.Examples
  using (⊢id; ⊢Vec; ⊢head)