Report or block benediktahrens
Contact Support about this user's behavior.Report abuse
Coq code accompanying several articles on semantics of functional programming languages
Forked from vladimirias/Foundations
Development of the univalent foundations of mathematics in Coq
Heterogeneous substitution systems
Cohomology in HoTT
We give a proof in Univalent Foundations that the Sigma type of types in a universe of hlevel n is itself of hlevel n+1.