A reimplementation of the type system by Siles and Herbelin with Autosubst 2.
The system in this repository has a fixed predicative universe hierarchy, though the confluence theorem is derived from the type exchange property, which holds for general pure type systems. The repository is still a WIP, but I have already proven the diamond property for the typed parallel reduction relation.