Groupoid Infinity cubical base library for cubicaltt
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

Build Status

Groupoid Infinity

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


  • 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