Locales.NotationalConventions

Ayberk Tosun, 13 September 2023


{-# OPTIONS --safe --without-K #-}

open import UF.PropTrunc
open import UF.FunExt

module Locales.NotationalConventions (pt : propositional-truncations-exist)
                                     (fe : Fun-Ext) where

open import Locales.SmallBasis                 pt fe
open import Locales.Spectrality.SpectralLocale pt fe


\section{Data vs. property distinction}

As we work in Univalent Foundations, we maintain a careful distinction between
structures and properties.

To emphasise that we are working with the structural version of a definition
that has a version that is a property, we use the superscript `_ᴰ` (for "data").

For example, we have `spectralᴰ` which denotes the structure involved in
spectrality.


_ = spectralᴰ


The version that is a property is called `is-spectral`.


_ = is-spectral


\section{Locales vs. frames}

TODO