type exp =
| EPre of Z.t | EKan of Z.t (* cosmos *)
| EVar of ident | EHole (* variables *)
| EPi of exp * (ident * exp) | ELam of exp * (ident * exp) | EApp of exp * exp (* pi *)
| ESig of exp * (ident * exp) | EPair of tag * exp * exp (* sigma *)
| EFst of exp | ESnd of exp | EField of exp * string (* simga elims/records *)
| EId of exp | ERef of exp | EJ of exp (* 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 * exp * exp (* glueing *)
| EEmpty | EIndEmpty of exp (* 𝟎 *)
| EUnit | EStar | EIndUnit of exp (* 𝟏 *)
| EBool | EFalse | ETrue | EIndBool of exp (* 𝟐 *)
| EW of exp * (ident * 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 *)Anders is a HoTT proof assistant based on CCHM in flavour of Cubical Agda plus strict equality for 2LTT and ℑ modality for synthetic differential geometry.
- 𝟎, 𝟏, 𝟐, W.
- Pretypes & strict equality.
- Generalized Transport and Homogeneous Composition as primitive Kan operations.
- Cubical subtypes.
- Glue types.
- Coequalizer.
- ℑ modality.
- UTF-8 support including universe levels (i.e.
U₁₂₃). - Lean syntax for ΠΣW.
- Poor man’s records as Σ with named accessors to telescope variables.
- 1D syntax with top-level declarations.
$ make
$ dune exec anders helpYou can find some examples in library/.
def inv′ (A : U) (a b : A) (p : Path A a b) : Path A b a :=
<i> hcomp A (∂ i) (λ (j : I), [(i = 0) → p @ j, (i = 1) → a]) a
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/everything.andersType Checker is based on classical MLTT-80 with 0, 1, 2 and W-types.
- Intuitionistic Type Theory [Martin-Löf]
- 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]
- 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]
- Univalent People