package anders

🧊 Anders

Modal Homotopy Type System.

type exp =
  | EPre of Z.t | EKan of Z.t | EVar of name | EHole                                 (* cosmos *)
  | EPi of exp * (name * exp) | ELam of exp * (name * exp) | EApp of exp * exp           (* pi *)
  | ESig of exp * (name * exp) | EPair of tag * exp * exp | EFst of exp | ESnd of exp (* sigma *)
  | EId of exp | ERef of exp | EJ of exp | EField of exp * string           (* strict equality *)
  | 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 functions *)
  | 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 *)
  | 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 *)
  | EIm of exp | EInf of exp | EIndIm of exp * exp | EJoin of exp    (* Infinitesimal Modality *)
  | 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 *)

Features

• Homepage: https://groupoid.space/homotopy
• Fibrant MLTT-style 0-1-2-Π-Σ-W primitives with Uₙ hierarchy in 500 LOC
• Cofibrant CHM-style I primitives with pretypes hierarchy Vₙ in 500 LOC
• Generalized Transport and Homogeneous Composition core Kan operations
• Partial Elements
• Cubical Subtypes
• Glue types
• Strict Equality on pretypes
• Coequalizer
• Hub Spokes Disc
• Infinitesimal Shape Modality (de Rham Stack)
• Parser in 80 LOC
• Lexer in 80 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 base library: https://groupoid.space/math
• Best suited for academic papers and fast type checking

Setup

$ opam install anders

Samples

You can find some examples in the share directory of the Anders package.

def comp-Path⁻¹ (A : U) (a b : A) (p : Path A a b) :
  Path (Path A a a) (comp-Path A a b a p (<i> p @ -i)) (<_> a) :=
<k j> hcomp A (∂ j ∨ k) (λ (i : I), [(j = 0) → a, (j = 1) → p @ -i ∧ -k, (k = 1) → a]) (p @ j ∧ -k)

def kan (A : U) (a b c d : A) (p : Path A a c) (q : Path A b d) (r : Path A a b) : Path A c d :=
<i> hcomp A (∂ i) (λ (j : I), [(i = 0) → p @ j, (i = 1) → q @ j]) (r @ i)

def comp (A : I → U) (r : I) (u : Π (i : I), Partial (A i) r) (u₀ : (A 0)[r ↦ u 0]) : A 1 :=
hcomp (A 1) r (λ (i : I), [(r = 1) → transp (<j>A (i ∨ j)) i (u i 1=1)]) (transp(<i> A i) 0 (ouc u₀))

def ghcomp (A : U) (r : I) (u : I → Partial A r) (u₀ : A[r ↦ u 0]) : A :=
hcomp A (∂ r) (λ (j : I), [(r = 1) → u j 1=1, (r = 0) → ouc u₀]) (ouc u₀)

$ anders check library/path.anders

MLTT

Type Checker is based on classical MLTT-80 with 0, 1, 2 and W-types.

• Intuitionistic Type Theory [Martin-Löf]

CCHM

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.

HTS

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]

Modalities

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]

Benchmarks

$ time make
real    0m4.936s
user    0m1.874s
sys     0m0.670s

$ time for i in library/* ; do ./anders.native check $i ; done
real    0m2.085s
user    0m1.982s
sys     0m0.105s

Acknowledgements

• Univalent People

Mentions

• Anders: верификатор математики 2022-01-17

Authors

• @siegment
• @5HT