Anders Versions Save

🧊 Модальний гомотопічний верифікатор математики

1.1.1

2 years ago
  • 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)

0.12.1

2 years ago
  • 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

0.7.2

2 years ago
  • 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

0.7.1

2 years ago

0.7

2 years ago
  • 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