[ANN] Anders Modal Homotopy Type System 5.1.0

Community
1

The main news in new version is an ability to derive full computable tower of K(G,n) with computable η MLTT uniqueness rule for Eilenberg-MacLance spaces K(G,n) by using pure CCHM core with Well-founded Trees, Homotopy Interval, Coequalizer, Hub Spokes Disc w/o General Higher Inductive Schemes (HIT) in the style of Coq/HoTT library and Three-HIT theorem.

def K-η (G : abgroup) (n : nat) (P : Π (k : nat), K G k → U) (h : Π (k : nat)
 (z : K G k), P k z) : Path (Π (z : K G n), P n z) (h n) (λ (z : K G n), 
  K-ind G n P (λ (g : G.1.1), h zero g) (λ (k : nat) (prev : Π (y : K G k),
 P k y) (y : K G (succ k)), h (succ k) y) z) 
  := ind-nat (λ (k : nat), Path (Π (z : K G k), P k z) (h k) (λ (z : K G k),
  K-ind G k P (λ (g : G.1.1), h zero g) (λ (m : nat) (pr : Π (y : K G m), 
 P m y) (y : K G (succ m)), h (succ m) y) z)) (<_> (h zero)) (λ (k : nat)
 (prev : Path (Π (z : K G k), P k z) (h k) (λ (z : K G k), K-ind G k P (λ (g :
 G.1.1), h zero g) (λ (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)),
 h (succ m) y) z)), <_> (h (succ k))) n

In the upcoming release the new Flat Modality in Kernel is awaiting along with Differential Geometry modules in Base Library: LIBRARY

Also more robust DNF solver for Homotopy Tesseract replaced the old one. Native stuff for Coequalizer, Hub Spokes Disc was added. Canonical S^1 expressed as W+Path is given. Pullback/Pushout lemmas were filled. Computable Truncation and Suspension MLTT rules derived.

If you want to see minimal cubical type checker in OCaml look into https://per.groupoid.space, if you want to learn one axiom system in the style of CoC and PTS look into https://henk.groupoid.space. Despite they are targeting Erlang/OTP and BEAM VM they contain its OCaml model in each repository. For full list of Groupoid Infinity languages see: https://groupoid.space.

2 Likes
4

Is this an opam package?

1 Like
5

Sure, you can install it with

$ opam install anders

See project page for the official announcement: https://anders.groupoid.space

6

OK, thanks. Typically, we announce opam packages with a direct link: anders 5.1.0 (latest) · OCaml Package

And a link to the source code: GitHub - groupoid/anders: 🧊 Модальний гомотопічний верифікатор математики · GitHub

I also noticed that the opam package does not have a description. Please consider providing one for searchability.

Thanks!

1 Like
8

Hi, no harm intended. I am just trying to help expose your package to a wider audience. If you look at this thread history, it was actually unlisted for about an hour on May 2nd because Discourse thought it was AI spam. I thought that clear markers and links mentioning opam package and source info would make it clear that it’s not.

If you look at the announce tag in this forum, most people are following the convention of mentioning the package name and linking to the source code. There is no hard rule about this but it helps potential users find and understand your work, so…

2 Likes
9

I couldn’t set announce tag because I was banned :slight_smile: not because I missed. I didn’t know that I have only one chance to publish being a verified member already.

Frankly speaking Anders has near zero potential users :slight_smile: It doesn’t need to be promoted as web framework.