Skip to content

Kan Operations

Choose a tag to compare

@5HT 5HT released this 14 Jul 19:45
  • 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