The Cartesian Closed Bicategory of Thin Spans of Groupoids

Pierre Clairambault, Simon Forest

Recently, there has been growing interest in bicategorical models of programming languages, which are "proof-relevant" in the sense that they keep distinct account of execution tra…