Tesseract and K(G,n)-η

• Added strict canonical Nat to Kernel for spectral goodness at higher homotopies.
• Fix constcubes.anders module with improved DNF solver in formula.ml.
• Constructive K(G,n)-η in KGn.anders.
• Sn.anders and truncation.anders are using inernal Nat.
• Homotopy Nat with homotopical canonicity (only) is in natw.anders module.
• Updated Article: https://anders.groupoid.space/doc/anders.pdf

Complete Kernel

• Disc and Hub Spokes kernel primitives
• Hub Spokes Disc in W
• Lambda in W
• Borel sets
• Basic Topology
• Locally Small Categories
• Symmetric Monoidal Categories
• OCaml 5.0

Univalence

• Glue Type
• 0, 1, 2, W Types
• Coequalizer Type
• Hub-Spokes Disc Type
• Infinitesimal Shape Modality
• Univalence, Unimorphism, Minivalence
• Fibre Bundles
• Homotopy (Co)Limits, Suspension, Sphere, Truncations, Quotients
• Propositions
• K(G,n)

Categorical Library

• Sigma with auto projections
• Modules: algebra, cat, fun, topos, ab, kraus
• LaTeX paper [LIPIcs]
• Improved Huber rules
• Support for PartialP primitive
• Improved reduction rules for hypercubes

Kan Operations

• Strict Equality (Id, ref, idJ)
• Cubical Subtypes (Sub, inc, ouc)
• Partials, Systems (Partial, [φ ↦ u])
• Kan Operations (hcomp, transp)
• Eliminate neutral elements (Mini-TT)
• Fast type checking
• Fast compilation
• Initial Base Library (OPAM share folder)
• New options silent and indices

Binary Distribution

• Minor optimizations
• OPAM package
• ISC license
• Homepage: https://anders.groupoid.space/

MLTT Internalization

• Fibrant MLTT-style ΠΣ primitives with Leibniz equality in 500 LOC
• Cofibrant CHM-style I primitives with pretypes hierarchy Vₙ in 500 LOC
• Generalized Transport
• Parser in 80 LOC
• Lexer in 80 LOC