🧊 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 *)

Anders is a HoTT proof assistant based on: classical MLTT-80 with 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 modality 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 HubSpokes Disc in the style of HoTT/Coq homotopy library and Three-HIT theorem.

Features

Homepage: https://anders.groupoid.space/
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 Homotopy Library: https://anders.groupoid.space/lib/
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/book.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

Intel i7-8700.

$ time dune build

real    0m1.456s
user    0m2.794s
sys     0m0.564s

$ time dune exec anders check library/book.anders

real    0m0.468s
user    0m0.051s
sys     0m0.032s

Anders: Homotopy Library

Here is given the Anders Homotopy Library.

Foundations

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/
│   └── infinitesimal/
└── univalent/
    ├── equiv/
    ├── extensionality/
    ├── iso/
    ├── path/
    └── prop/

Mathematics

In the mathematics folder you will find Mathematical Components for HTS:

anders.groupoid.space/mathematics/
├── algebra/
│   ├── homology/
│   └── algebra/
├── analysis/
│   └── real/
├── categories/
│   ├── abelian/
│   ├── category/
│   ├── functor/
│   └── groupoid/
├── geometry/
│   ├── bundle/
│   ├── etale/
│   └── formalDisc/
├── homotopy/
│   ├── KGn/
│   ├── S1/
│   ├── Sn/
│   ├── coequalizer/
│   ├── hubSpokes/
│   ├── pullback/
│   ├── pushout/
│   ├── quotient/
│   ├── suspension/
│   └── truncation/
└── topoi/
    └── topos/

Usage

The main purpose of Anders is doing Homotopy Theory:

$ dune exec anders repl

Anders Proof Assistant version 1.4.0
Copyright © 2021–2022 Groupoid Infinity.

For help type ‘:h’.

>

Mentions

Maxim Sokhatsky. Презентація кубічного CCHM прувера Anders 0.7.2 від Групоїд Інфініті. 2021-07-18
Maxim Sokhatsky. Anders: верификатор математики. 2022-01-17
Maxim Sokhatsky. Anders: Modal Homotopy Type System. 2022-01-17

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

groupoid / anders

Programming Languages

Labels

Projects that are alternatives of or similar to anders