Groupoid Infinity

Infinity — Language with HITs
on top of MLTT core

Lambda Calculus