search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

Define the discrete locale over a set #253

Closed ayberkt closed 4 months ago

ayberkt commented 4 months ago

This PR adds a definition of the discrete locale over a set, and it also defines the locale 2 as an instance.