Computational tool for tiny presheaf topoi.
version: prerelease
- fsharp
- building
- in the root directory, build by entering at your terminal:
dotnet build -c release
- in the root directory, build by entering at your terminal:
- notebooks
- this program is intended to be used in
.ipynbnotebook files within visual studio code or jupyter. see https://github.com/dotnet/interactive/blob/main/README.md for details on how to set this up. - examples are in the directory "nb".
- this program is intended to be used in
- tests
- in the root directory, run tests by entering at your terminal:
dotnet fsi test/Test.fsx
- in the root directory, run tests by entering at your terminal:
- latex output
- categories
- binary products/sums
- category of elements
- presheaves
- yoneda embedding
- binary products/sums
- pullbacks/pushouts
- equalisers/coequalisers
- exponentials
- isomorphisms
- truth objects
- internal logic
- biheyting algebra of subobjects
- meets/joins
- implication/subtraction
- negation/supplement
- boundary/coboundary
- quantifiers
- modal operators
- lawvere-tierney topologies
- general limits/colimits
- geometric and logical morphisms
- j-sheaves
- mitchell-benabou language
- ...
- Marie La Palme Reyes, Gonzalo E. Reyes, Houman Zolfaghari, Generic figures and their glueings. A constructive approach to functor categories, Polimetrica (2008), ISBN: 8876990046. pdf.
- Saunders Mac Lane, Ieke Moerdijk, Sheaves in geometry and logic. A first introduction to topos theory, Springer-Verlag (1994), ISBN: 0-387-97710-4.
- thanks to the awesome f# community at fsharp.slack.com for their guidance.