Alex Gryzlov clayrat
clayrat
/ sheafify.v
Created
February 27, 2026 22:35
— forked from andrejbauer/sheafify.v
Sheafification with respect to a Lawvere-Tierney closure in logical form.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* The basic theory of Lawvere-Tierney operators and sheafification in logical form. | |
| This formalization is based on: | |
| Barbara Veit: A proof of the associated sheaf theorem by means of categorical logic, | |
| The Journal of Symbolic Logic , Volume 46 , Issue 1 , March 1981 , pp. 45–55 | |
| DOI: https://doi.org/10.2307/2273255 | |
| *) | |
| Require Import Utf8. |