RedPRL

受 Nuprl 启发而开发的基于策略的计算笛卡尔立方类型理论证明助手。RedPRL 实现了两级立方类型理论，其中包括单等式宇宙、一些高级归纳类型和带有等式反射的严格等式类型。「A tactic-based proof assistant for computational Cartesian cubical type theory inspired by Nuprl. RedPRL implements a two-level cubical type theory which includes univalent universes, some higher inductive types, and strict equality types with equality reflection.」