search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
441 stars 134 forks source link

Topological modalities #1125

Closed awswan closed 2 months ago

awswan commented 2 months ago

I needed some results about topological modalities for a project, and I think it makes sense to add these to the library in case anyone else wants to use them. I'm not 100% sure about the naming, so feel free to change if necessary. There are a couple of naming clashes that come from the literature, so there's not much I can do about them: 1. Separated is a general definition that applies to any modality, whereas in the library (and many places in the literature) it is specific to the double negation modality; 2. So far Injective in the library is only referring to functions, I think, but I also use it for injective objects, as in https://ncatlab.org/nlab/show/injective+object .

awswan commented 2 months ago

Thanks! I've made both those changes.