[ANN] anders 0.7.1

The HTS language proposed by Voevodsky exposes two different presheaf models of type theory: the inner one is homotopy type system presheaf that models HoTT and the outer one is traditional Martin-Löf type system presheaf that models set theory with UIP. The motivation behind this doubling is to have an ability to express semisemplicial types. Theoretical work on merging meta-theoretical and homotopical languages was continued in 2LTT [Anenkov, Capriotti, Kraus, Sattler].

While we are on our road to HTS with Lean-like tactic language, currently we are at the stage of regular cubical (HoTT) type checker with CHM-style primitives, or more general CCHM type checker. You may try it at Github: groupoid/anders.

$ opam install anders
$ anders
Anders theorem prover [PTS][MLTT][CCHM-4][HTS].

   invoke = anders | anders list
     list = [] | command list
  command = check filename     | lex filename
          | parse filename     | help
          | cubicaltt filename | girard
          | trace

Anders is idiomatic and educational. We carefully draw the favourite Lean-compatible syntax to fit 130 LOC in Menhir, the MLTT core (based on Mini-TT) is 500 LOC and pretypes presheaf is another 500 LOC.

3 Likes