3 papers
cs.LO2026
The very dependent recursive structure of iterated parametricity in indexed form
Hugo Herbelin, Ramkumar Ramachandra
Reynolds' parametricity originally equips types with proof-irrelevant binary propositional relations over the types. But such relations can also be taken proof-relevant or unary, a…
cs.LO2024
A parametricity-based formalization of semi-simplicial and semi-cubical sets
Hugo Herbelin, Ramkumar Ramachandra
Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alterna…
math.AT2022
Operads in Derived Deformation Theory
Ramkumar Ramachandra
A theorem by Pridham and Lurie provides an equivalence between formal moduli problems and Lie algebras in characteristic zero. In his work, Lurie has distilled the axioms that the…