The category of locales #
This file defines Locale
, the category of locales. This is the opposite of the category of frames.
Equations
- Locale.instCoeSortType = { coe := fun (X : Locale) => ↑(Opposite.unop X) }
Construct a bundled Locale
from a Frame
.
Instances For
Equations
- Locale.instInhabited = { default := Locale.of PUnit.{?u.3 + 1} }
@[simp]