topos-tool

Computational tool for tiny presheaf topoi.

version: prerelease

---

how to

• fsharp
  • you will need fsharp installed:
    • linux
    • mac
    • win
    • freebsd
• building
  • in the root directory, build by entering at your terminal:

    dotnet build -c release
    

• notebooks
  • this program is intended to be used in .ipynb notebook 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".
• tests
  • in the root directory, run tests by entering at your terminal:

    dotnet fsi test/Test.fsx
    

features

• 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

to do

• general limits/colimits
• geometric and logical morphisms
• j-sheaves
• mitchell-benabou language
• ...

references

• 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.

acknowledgements

• thanks to the awesome f# community at fsharp.slack.com for their guidance.