Skip to main content
Share Your Experience: Take the 2024 Developer Survey

New answers tagged

3 votes

Why Normalisation by Evaluation needs to use a different representation of programs?

It is good to know some basic facts about section-retraction pairs. Suppose $f : X \to Y$ of and $g : Y \to X$ are maps such that $g \circ f = \mathrm{id}_X$. We say that they form a section-...
Andrej Bauer's user avatar
  • 30.8k

Top 50 recent answers are included