The Groupoid Infinity Cubical Base Library is dedicated to cubical-compatible typecheckers based on homotopy interval [0,1] and MLTT as a core. The base library is founded on top of 5 core modules: proto (composition, id, const), path (subst, trans, cong, refl, singl, sym), propset (isContr, isProp, isSet), equiv (fiber, eqiuv) and iso (lemIso, isoPath). This machinery is enough to prove univalence axiom.
(i) The library has rich recursion scheme primitives in lambek module, while very basic nat, list, stream functionality. (ii) The very basic theorems are given in pi, iso_pi, sigma, iso_sigma, retract modules. (iii) The library has category theory theorems from HoTT book in cat, fun and category modules. (iv) The library also includes some impredicative categorical encoding sketches in coproduct_set. lambek also includes inductive semantics modeled with cata/ana recursion and fixpoint adjoints in/out.
This library is best to read with HoTT book at http://groupoid.space/mltt/types/
- bool — Boolean
- control — Control Free/CoFree, fix, pure/applicative typeclasses)
- eq — Runtime equality typeclass
- functor — Runtime Functor typeclass
- either — Runtime Either
- maybe — Runtime Maybe
- nat — Runtime Nat
- list — Runtime List
- stream — Runtime Stream
- vector — Runtime Vector
- function — Runtime Function
- equiv — Core Equivalence
- propset — Core isContr isProp isSet isGroupoid
- path — Core Path Type
- proto — Core Proto File
- iso — Core Iso
- iso_pi — Iso Pi Theorems
- iso_sigma — Iso Sigma Theorems
- pi — Pi
- sigma — Sigma
- lambek — Inductive Models
- cat — HoTT Category
- univ — HoTT Univalence
- circle — HoTT Circle
- retract — HoTT Retract
- fun — HoTT Categorical Functor
- Maxim Sokhatsky
- Eugene Smolanka
- Andy Melnikov
- Denis Stoyanov
- Dmitry Astapov