In Cantor Space No One Can Hear You Stream

Abstract

Abstract We revisit the famous notion of sheaves through the lens of type theory and side-effects. Using the language of $$\textsf{MLTT}$$ MLTT , we show that they inductively approximate idealized functional objects as decision trees, realizing a generalized form of continuity. We materialize this intuition in $$\textsf{MLTT}^{\textsf{F}}$$ MLTT F , a case-study sheaf extension of $$\textsf{MLTT}$$ MLTT with a Cohen real and leverage it to show uniform continuity of all $$\textsf{MLTT}$$ MLTT functionals of type $$({\mathbb {N}}\rightarrow {\mathbb {B}}) \rightarrow {\mathbb {N}}$$ ( N → B ) → N . The latter results were mechanized in Rocq.