The literate programming vibe of this blog post (with Agda) is absolutely fantastic.

Nice! Finally sheaves are entering into this level of discussion. Been waiting for this for a while.

For a deeper look at the sensor-integration perspective, try “Sheaves are the canonical datastructure for sensor integration”.