This paper is mightily bad-ass. Already the logically prior work that gives a semantics for a lambda calculus in categories of presheaves was stretching the limits of my category theory knowledge. How that stuff works is by an elegant generalization of ordinary Kripke semantics for intuitionistic logic: instead of a poset of worlds W, and instead of it being an all-or-nothing fact that w ⊩ A ("world w forces proposition A") which satisfies monotonicity, we have a category C of worlds, and a collection of reasons (which one might think of as proofs) why each proposition is true at each world, with monotonicity being replaced by the "arrow part" of the functor from C to Setsop --- it tells us how proofs evolve over time.
But to get normal forms for coproducts, it seems to be necessary to consider contexts plus constraints. This somehow translates in category-land to sheaves instead of mere presheaves. These sheaves are over a Grothendieck topology where the locality condition --- the requirment that every matching family has a unique amalgamation --- amounts, by a clever choice of topology, to the fact that every pair of terms that look like two branches of a case statement have a unique amalgamation into a normal form which is βη equal to actually casing over those two branches.
All I can say is, omg, sheaves.
