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.
Ok sir, I will consider providing description in the upcoming release 5.5.0.
Could you please also leave message for Menhir, it also lack description and we need proper visibility for LR(1) parses in OCaml community.
This announce also lack information on sources.
By saying we, what do you even mean here? Who gave you that authority?
As a new user when I can find policy on publishing and properly announcing new packages?
I read all information and made all comparisons but I hit Menhir Obstacle.
OCaml lacks proper description too. Btw. How are you sleeping with that?
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…
I couldn’t set announce tag because I was banned 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 It doesn’t need to be promoted as web framework.
not because I missed. I didn’t know that I have only one chance to publish being a verified member already.