- quotient: My own implementation of quotient with resizing rules as axioms
- rapport: Master Thesis (may be wrong)
- reform: Formalization of the translation between MLTT + reflection and MLTT + axioms (given up)
TheoWinterhalter/resizing-reflection
Master Thesis with Nicolas Tabareau on Resizing Rules and Reflection
Coq