Anders is a reincarnation of cubicaltt type checker in another basis.
$ opam install anders$ anders preeval check library/book.anders help repl
...
File “KGn.anders” checked.
File “book.anders” checked.
Anders Proof Assistant version 5.5.0
Copyright © 2016–2026 Groupoid Infinity.
Home: https://homotopy.dev/
Use:
exec := anders | anders list
list := [] | comm list
comm := check <filename> | silent
| parse <filename> | trace
| lex <filename> | girard
| preeval | irrelevance
| repl | help
Anders Proof Assistant version 5.5.0
Copyright © 2016–2026 Groupoid Infinity.
For help type ‘:h’.
> :h
Available commands:
<statement> infer type and normalize statement
:q quit
:r restart
:save <file> save term to file <file>.bin
:load <file> load term from file <file>.bin
:bundle <pkg> <term1> ... <termN> bundle multiple terms to <pkg>.bin
:h display this message
Information about shell commands can be found at ‘:h’.
>Modal Homotopy Type System.
type exp =
| EPre of Z.t | EKan of Z.t | EVar of name | EHole (* Cosmos *)
| ENat | EZero | ESucc of exp | EIndNat of exp * exp * exp (* Canonical Natural Numbers *)
| EPi of exp * (name * exp) | ELam of exp * (name * exp) | EApp of exp * exp (* Π *)
| ESig of exp * (name * exp) | EPair of tag * exp * exp | EFst of exp | ESnd of exp (* Σ *)
| EId of exp | ERef of exp | EJ of exp | EField of exp * string (* Strict Equality *)
| EEmpty | EIndEmpty of exp (* 𝟎 *)
| EUnit | EStar | EIndUnit of exp (* 𝟏 *)
| EBool | EFalse | ETrue | EIndBool of exp (* 𝟐 *)
| EW of exp * (name * exp) | ESup of exp * exp | EIndW of exp * exp * exp (* W *)
| EPathP of exp | EPLam of exp | EAppFormula of exp * exp (* Path Equality *)
| EI | EDir of dir | EAnd of exp * exp | EOr of exp * exp | ENeg of exp (* CCHM Interval *)
| ETransp of exp * exp | EHComp of exp * exp * exp * exp (* Kan Operations *)
| EPartial of exp | EPartialP of exp * exp | ESystem of exp System.t (* Partial Funs *)
| ESub of exp * exp * exp | EInc of exp * exp | EOuc of exp (* Cubical Subtypes *)
| EGlue of exp | EGlueElem of exp * exp * exp | EUnglue of exp (* Glueing *)
| ECoeq of exp | EIota of exp | EResp of exp | EIndCoeq of exp (* Coequalizer *)
| EDisc of exp | EBase of exp | EHub of exp | ESpoke of exp | EIndDisc of exp (* Disc *)
| EIm of exp | EInf of exp | EIndIm of exp * exp | EJoin of exp (* Infinitesimals *)
| EFla of exp | EFlaUnit of exp | EFlaCounit of exp | EIndFla of exp * exp (* Flat *)Anders is a HoTT proof assistant based on: classical MLTT-80 with N, 0, 1, 2, W types; CCHM in CHM flavour as cubical type system with hcomp/trans Kan operations; HTS sctrict equality on pretypes; de Rham stack and Flat modalities; Disc and Coequalizer primitives. We tend not to touch general recursive higher inductive schemes yet, instead we will try to express as much HIT as possible through W, Coequlizer and Hub Spokes Disc in the style of HoTT/Coq homotopy library and Three-HIT theorem.
- Homepage: https://anders.groupoid.space/
- Fibrant MLTT-style N-0-1-2-Π-Σ-W primitives with Uₙ hierarchy in 500 LOC
- Cofibrant CHM-style I (PathP) primitives with pretypes hierarchy Vₙ in 500 LOC
- Generalized Transport and Homogeneous Composition core Kan operations
- Partial Elements
- Cubical Subtypes
- Glue types
- Left Fibered Equivalence
- Strict Equality on pretypes
- Coequalizer
- Hub Spokes Disc
- Nat in Kernel for spectral goodness under higher homotopies
- Infinitesimal Shape Modality (de Rham Stack)
- Flat Modality (Sharp is derived)
- Parser in 180 LOC
- Lexer in 120 LOC
- Small Kernel in 2000 LOC
- UTF-8 support including universe levels
- Lean syntax for ΠΣW
- Poor man's records as Σ with named accessors to telescope variables
- 1D syntax with top-level declarations
- Groupoid Infinity CCHM Homotopy Library: https://anders.groupoid.space/library/
- Pure basis best suited for academic papers on W-types and well ordered type checking
transpⁱ N φ u₀ = u₀
transpⁱ U φ A = A
transpⁱ (Π (x : A), B) φ u₀ v = transpⁱ B(x/w) φ (u₀ w(i/0)), w = transp-Fill⁻ⁱ A φ v, v : A(i/1)
transpⁱ (Σ (x : A), B) φ u₀ = (transpⁱ A φ (u₀.1), transpⁱ B(x/v) φ(u₀.2)), v = transp-Fillⁱ A φ u₀.1
transpⁱ (Pathʲ A v w) φ u₀ = 〈j〉 compⁱ A [φ ↦ u₀ j, (j=0) ↦ v, (j=1) ↦ w] (u₀ j)
transpⁱ G ψ u₀ = glue [φ(i/1) ↦ t′₁] a′₁ : G(i/1), G = Glue [φ ↦ (T,w)] A
transpⁱ (W (x : A), B) φ (sup a f) = sup (transpⁱ A φ a) (transpⁱ (B(v) → W) φ f), v = transp-Fillⁱ A φ a
transpⁱ (Coequ A B f g) φ (ι₂ b) = ι₂ (transpⁱ B φ b)
transpⁱ (Coequ A B f g) φ (resp a j) = resp (transpⁱ A φ a) j
transpⁱ (Disc S A) φ (base a) = base (transpⁱ A φ a)
transpⁱ (Disc S A) φ (hub f) = hub (transpⁱ (S → Disc S A) φ f)
transpⁱ (Disc S A) φ (spoke f y j) = spoke (transpⁱ (S → Disc S A) φ f) (transpⁱ S φ y) j
transpⁱ (ℑ A) φ (ℑ-unit a) = ℑ-unit (transpⁱ A φ a)
transpⁱ (♭ A) φ (♭-unit a) = ♭-unit (transpⁱ A φ a)
transp⁻ⁱ A φ u = (transpⁱ A(i/1−i) φ u)(i/1−i) : A(i/0)
transp-Fillⁱ A φ u₀ = transpʲ A(i/i∧j) (φ∨(i=0)) u₀ : A
hcompⁱ N [φ ↦ 0] 0 = 0
hcompⁱ N [φ ↦ S u] (S u₀) = S (hcompⁱ N [φ ↦ u] u₀)
hcompⁱ U [φ ↦ E] A = Glue [φ ↦ (E(i/1), equivⁱ E(i/1−i))] A
hcompⁱ (Π (x : A), B) [φ ↦ u] u₀ v = hcompⁱ B(x/v) [φ ↦ u v] (u₀ v)
hcompⁱ (Σ (x : A), B) [φ ↦ u] u₀ = (v(i/1), compⁱ B(x/v) [φ ↦ u.2] u₀.2), v = hcomp-Fillⁱ A [φ ↦ u.1] u₀.1
hcompⁱ (Pathʲ A v w) [φ ↦ u] u₀ = 〈j〉 hcompⁱ A [ φ ↦ u j, (j = 0) ↦ v, (j = 1) ↦ w ] (u₀ j)
hcompⁱ G [ψ ↦ u] u₀ = glue [φ ↦ t₁] a₁ : G, G = Glue [φ ↦ (T,w)] A, t₁ = u(i/1) : T, a₁ = unglue u(i/1) : A, glue [φ ↦ t₁] a1 = t₁ : T
hcompⁱ (W (x : A), B) [φ ↦ sup a f] (sup a₀ f₀) = sup (hcompⁱ A [φ ↦ a] a₀) (hcompⁱ (B(v) → W) [φ ↦ f] f₀), v = hcomp-Fillⁱ A [φ ↦ a] a₀
hcompⁱ (Coequ A B f g) [φ ↦ ι₂ u] (ι₂ u₀) = ι₂ (hcompⁱ B [φ ↦ u] u₀)
hcompⁱ (Coequ A B f g) [φ ↦ resp a j] (resp a₀ j) = resp (hcompⁱ A [φ ↦ a] a₀) j
hcompⁱ (Disc S A) [φ ↦ base a] (base a₀) = base (hcompⁱ A [φ ↦ a] a₀)
hcompⁱ (Disc S A) [φ ↦ hub f] (hub f₀) = hub (hcompⁱ (S → Disc S A) [φ ↦ f] f₀)
hcompⁱ (Disc S A) [φ ↦ spoke f y j] (spoke f₀ y₀ j) = spoke (hcompⁱ (S → Disc S A) [φ ↦ f] f₀) (hcompⁱ S [φ ↦ y] y₀) j
hcompⁱ (ℑ A) [φ ↦ ℑ-unit u] (ℑ-unit u₀) = ℑ-unit (hcompⁱ A [φ ↦ u] u₀)
hcompⁱ (♭ A) [φ ↦ ♭-unit u] (♭-unit u₀) = ♭-unit (hcompⁱ A [φ ↦ u] u₀)
hсomp-Fillⁱ A [φ ↦ u] u₀ = hcompʲ A [φ ↦ u(i/i∧j), (i=0) ↦ u₀] u₀ : A
Type Checker is based on classical MLTT-80 with 0, 1, 2 and W-types.
- Intuitionistic Type Theory [Martin-Löf]
Anders was built by strictly following CCHM publications:
- CTT: a constructive interpretation of the univalence axiom [Cohen, Coquand, Huber, Mörtberg]
- On Higher Inductive Types in Cubical Type Theory [Coquand, Huber, Mörtberg]
- Canonicity for Cubical Type Theory [Huber]
- Canonicity and homotopy canonicity for cubical type theory [Coquand, Huber, Sattler]
- Cubical Synthetic Homotopy Theory [Mörtberg, Pujet]
- Unifying Cubical Models of Univalent Type Theory [Cavallo, Mörtberg, Swan]
- Cubical Agda: A Dependently Typed PL with Univalence and HITs [Vezzosi, Mörtberg, Abel]
- A Cubical Type Theory for Higher Inductive Types [Huber]
- Gluing for type theory [Kaposi, Huber, Sattler]
- Cubical Methods in HoTT/UF [Mörtberg]
We tried to bring in as little of ourselves as possible.
Anders supports classical Homotopy Type System with two identities.
- A simple type system with two identity types [Voevodsky]
- Two-level type theory and applications [Annenkov, Capriotti, Kraus, Sattler]
- Syntax for two-level type theory [Bonacina, Ahrens]
Infinitesimal Modality was added for direct support of Synthetic Differential Geometry.
- Differential cohomology in a cohesive ∞-topos [Schreiber]
- Cartan Geometry in Modal Homotopy Type Theory [Cherubini]
- Differential Cohesive Type Theory [Gross, Licata, New, Paykin, Riley, Shulman, Cherubini]
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory [Shulman]
- Three-HIT theorem [Bauer, van der Weide]
Intel i5-12400 or M4: Compilation in 5 seconds, full library checks in 5 sec with K(G,n)-η.
% time dune build
3.15s user 2.54s system 121% cpu 4.693 total
% time dune exec anders preeval check library/book.anders
3.21s user 0.13s system 86% cpu 3.848 total
Here is given the Anders Homotopy Library.
In the foundations folder presented the MLTT, Modal and Univalent base libraries:
anders.groupoid.space/foundations/
├── mltt/
│ ├── bool/
│ ├── either/
│ ├── fin/
│ ├── induction/
│ ├── list/
│ ├── maybe/
│ ├── mltt/
│ ├── nat/
│ ├── pi/
│ ├── sigma/
│ └── vec/
├── modal/
│ ├── flat/
│ ├── sharp/
│ ├── modality/
│ └── infinitesimal/
└── univalent/
├── equiv/
├── hedberg/
├── extensionality/
├── iso/
├── path/
└── prop/
In the mathematics folder you will find Mathematical Components for HTS:
anders.groupoid.space/mathematics/
├── algebra/
│ ├── algebra/
│ ├── homology/
│ └── int/
├── analysis/
│ ├── real/
│ └── topology/
├── categories/
│ ├── abelian/
│ ├── category/
│ ├── functor/
│ ├── topos/
│ └── groupoid/
├── geometry/
│ ├── bundle/
│ ├── etale/
│ └── formalDisc/
└── homotopy/
├── KG1/
├── KGn/
├── S1/
├── Sn/
├── coequalizer/
├── disc/
├── hopf/
├── loop/
├── pcoequ/
├── colimit/
├── pullback/
├── pushout/
├── quotient/
├── quotient2/
├── suspension/
└── truncation/
- Максим Сохацький. Презентація кубічного CCHM прувера Anders 0.7.2. 2021-07-18
- Максим Сохацький. Anders: верификатор математики. 2022-01-17
- Максим Сохацький. Anders: Modal Homotopy Type System. 2022-01-17
- Максим Сохацький. Система формальних мов Групоїд Інфініті. 2024-11-26