Skip to content

nasosev/topos-tool

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

47 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

topos-tool

Computational tool for tiny presheaf topoi.

version: prerelease


how to

  • fsharp
  • building
    • in the root directory, build by entering at your terminal:
      dotnet build -c release
      
  • notebooks
  • 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

About

Computational tool for tiny presheaf topoi

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published