This archive contains a Rocq formalization accompanying the paper "Sheaves as oracle computations" by Danel Ahman and Andrej Bauer, presented at Formal Structures for Computation and Deduction (FSCD) 2026. It covers Sections 2-4 of the paper: containers, modalities and oracle modalities, instance reducibility, sheaves for oracle modalities, sheafification as a quotient-inductive type, and equifoliate trees together with their descent map to the sheafification. Section 5 (realizability) is not formalized.