anders

Modal Homotopy Type System
README


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.

CCHM

Anders was built by strictly following CCHM publications:

We tried to bring in as little of ourselves as possible.

HTS

Anders supports classical Homotopy Type System with two identities.

Modalities

Infinitesimal Modality was added for direct support of Synthetic Differential Geometry.

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

Authors

Install
Sources
1.1.1.zip
md5=265c4b61dabe697e90a6ca2db300542b
sha512=9474fb6be18950afeea0bcc31489b2152209332e92d40ec10262100528ecf596196e05746ced7d687bc7e09695a1bcb52f52032ca8b2cfdc4a7fca454960fd49
Dependencies
menhir
>= "20200123"
ocaml
>= "4.10"
zarith
>= "1.12"
dune
>= "2.0"
Reverse Dependencies