search

martinescardo / TypeTopology

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

Define frame isomorphisms #259

Closed ayberkt closed 5 months ago

ayberkt commented 5 months ago

This PR makes two changes.

  1. It factors out the notions of frame homomorphism and continuous map of locales from the Locales.Frame module into their own modules.
  2. Adds two variants of the notion of frame isomorphism together with a proof of their equivalence.