Groupoid Infinity:

### Anders

CCHM/HTS Homotopy Type System with Strict Equality.

### Castle Bravo

Cubical type checker with definitional β-rule for Path types which allows us to avoid separate Id type like in cubicaltt. Computable winding.

### cubicaltt

The **cubicaltt** is a cubical type checker by Anders Mörtberg that supports path interval,
its connections, homogeneous path compositions, 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).

### Arend

**Arend** is a cartesian cubical type checker by JetBrains that supports HITs, extensible records,
type classes, implicit variables. It also contains Agda-style reasoning library.

- groupoid/arend — Groupoid Infinity cubical base library for Arend.
- JetBrains/Arend — Arend proof assistant.

### Lean

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++).

### Agda

This is a base library for **Agda** in cubical mode.

- groupoid/agda — Groupoid Infinity cubical base library for Agda.
- agda/agda — Agda proof assistant (Haskell).

Other Cubical Type Systems and Libraries:

### RedPRL

The **redtt** is a cartesian cubical type checker
that take its roots from RedPRL
and JonPRL.

- RedPRL/RedPRL — PRL-family proof assistant (Standard ML).
- RedPRL/redtt — cartesian cubical type checker (OCaml).
- RedPRL/cooltt — cartesian cubical type checker (OCaml).