Topos theory

Open HuStmpHrrr opened this issue 5 years ago • 1 comments

I think now the library is almost ready to do some topos theory. I think the first step is to turn the definition of topos to the "structure" style. then some properties should follow. it should be a good idea to make Topos a top level module.

Mar 31 '20 22:03 HuStmpHrrr

I have a preliminary implementation of sieves that might be useful for this. Will tidy it up and make a PR in the next few days.

Mar 31 '20 23:03 TOTBWF