CUBICAL

Groupoid Infinity Language Nucleus Experiments:

Smiling Buddha

The cubicaltt is a cubical CCHM type checker (Mörtberg) that supports path interval, connections, homogeneous compositions and generalized transport, higher inductive types, gluening of types and values. Recursive HITs have complete support only in hcomp version.

• groupoid/cubical — Groupoid Infinity cubical base library for cubicaltt type checker.
• groupoid/hopf — Hopf Fibrations for cubicaltt type checker.
• groupoid/hts — cubical syntax.
• mortberg/cubicaltt — cubical type checker (Haskell) with recursive HITs.
• mortberg/yacctt — cartesian cubical type checker (Haskell).
• simhu/cubical — early prototype of CCHM by Simon Huber.

Anders

Homotopy Type System (Voevodsky) with Strict Equality and CCHM Agda primitives.

Castle Bravo

Cubical type checker of HoTT-∂ Type System (Siegment) with definitional β-rule for Path types which allows us to avoid separate Id type like in cubicaltt. Computable winding.

Hurricane

Cubical type checker of HoTT-I Type System (Valery Isaev) with definitional β-rule for Path types.

Ground Zero

Ground Zero is a cubical model and cubical base library embedded into Lean.

• groupoid/lean — Ground Zero cubical base library for Lean 3 proof assistant.
• gebner/hott3 — HoTT library for Lean 3.
• leanprover/lean — Lean 3.4.1 (C++).