Groupoidal Realizability: Formalizing the Topological BHK Interpretation
Elementary Simplicial Collapses in Cubical Agda