This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
The large locale of propositions
module foundation.large-locale-of-propositions where
Imports
open import foundation.conjunction open import foundation.existential-quantification open import foundation.logical-equivalences open import foundation.propositional-extensionality open import foundation.unit-type open import foundation.universal-property-cartesian-product-types open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.propositions open import order-theory.large-frames open import order-theory.large-locales open import order-theory.large-meet-semilattices open import order-theory.large-posets open import order-theory.large-preorders open import order-theory.large-suplattices open import order-theory.least-upper-bounds-large-posets open import order-theory.top-elements-large-posets
Idea
The large locale of propositions consists of all the propositions of any universe level and is ordered by the implications between them. Conjunction gives this large poset the structure of a large meet-semilattice, and existential quantification gives it the structure of a large suplattice.
Note. The collection of all propositions is large because we do not assume propositional resizing.
Definitions
The large preorder of propositions
Prop-Large-Preorder : Large-Preorder lsuc (_⊔_) type-Large-Preorder Prop-Large-Preorder = Prop leq-prop-Large-Preorder Prop-Large-Preorder = hom-Prop refl-leq-Large-Preorder Prop-Large-Preorder P = id transitive-leq-Large-Preorder Prop-Large-Preorder P Q R g f = g ∘ f
The large poset of propositions
Prop-Large-Poset : Large-Poset lsuc (_⊔_) large-preorder-Large-Poset Prop-Large-Poset = Prop-Large-Preorder antisymmetric-leq-Large-Poset Prop-Large-Poset P Q = eq-iff
Meets in the large poset of propositions
has-meets-Prop-Large-Locale : has-meets-Large-Poset Prop-Large-Poset meet-has-meets-Large-Poset has-meets-Prop-Large-Locale = conjunction-Prop is-greatest-binary-lower-bound-meet-has-meets-Large-Poset has-meets-Prop-Large-Locale P Q R = is-greatest-binary-lower-bound-conjunction-Prop P Q R
The largest element in the large poset of propositions
has-top-element-Prop-Large-Locale : has-top-element-Large-Poset Prop-Large-Poset top-has-top-element-Large-Poset has-top-element-Prop-Large-Locale = unit-Prop is-top-element-top-has-top-element-Large-Poset has-top-element-Prop-Large-Locale P p = star
The large poset of propositions is a large meet-semilattice
is-large-meet-semilattice-Prop-Large-Locale : is-large-meet-semilattice-Large-Poset Prop-Large-Poset has-meets-is-large-meet-semilattice-Large-Poset is-large-meet-semilattice-Prop-Large-Locale = has-meets-Prop-Large-Locale has-top-element-is-large-meet-semilattice-Large-Poset is-large-meet-semilattice-Prop-Large-Locale = has-top-element-Prop-Large-Locale
Suprema in the large poset of propositions
is-large-suplattice-Prop-Large-Locale : is-large-suplattice-Large-Poset lzero Prop-Large-Poset sup-has-least-upper-bound-family-of-elements-Large-Poset ( is-large-suplattice-Prop-Large-Locale {I = I} P) = ∃ I P is-least-upper-bound-sup-has-least-upper-bound-family-of-elements-Large-Poset ( is-large-suplattice-Prop-Large-Locale {I = I} P) R = inv-iff (up-exists R)
The large frame of propositions
Prop-Large-Frame : Large-Frame lsuc (_⊔_) lzero large-poset-Large-Frame Prop-Large-Frame = Prop-Large-Poset is-large-meet-semilattice-Large-Frame Prop-Large-Frame = is-large-meet-semilattice-Prop-Large-Locale is-large-suplattice-Large-Frame Prop-Large-Frame = is-large-suplattice-Prop-Large-Locale distributive-meet-sup-Large-Frame Prop-Large-Frame = eq-distributive-conjunction-exists
The large locale of propositions
Prop-Large-Locale : Large-Locale lsuc (_⊔_) lzero Prop-Large-Locale = Prop-Large-Frame