The locale of propositions

Content created by Fredrik Bakke.

Created on 2025-01-07.
Last modified on 2025-01-07.

module foundation.locale-of-propositions where
Imports 
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.large-locale-of-propositions
open import foundation.logical-equivalences
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.function-types

open import order-theory.frames
open import order-theory.greatest-lower-bounds-posets
open import order-theory.large-posets
open import order-theory.large-preorders
open import order-theory.meet-semilattices
open import order-theory.meet-suplattices
open import order-theory.posets
open import order-theory.preorders
open import order-theory.suplattices
open import order-theory.top-elements-posets

Idea

The locale of propositions consists of all the propositions of any universe level and is ordered by the implications between them. Conjunction gives this poset the structure of a meet-semilattice, and existential quantification gives it the structure of a suplattice.

Definitions

The preorder of propositions

Prop-Preorder : (l : Level) → Preorder (lsuc l) l
Prop-Preorder = preorder-Large-Preorder Prop-Large-Preorder

The poset of propositions

Prop-Poset : (l : Level) → Poset (lsuc l) l
Prop-Poset = poset-Large-Poset Prop-Large-Poset

The largest element in the poset of propositions

has-top-element-Prop-Locale :
  {l : Level} → has-top-element-Poset (Prop-Poset l)
has-top-element-Prop-Locale {l} = (raise-unit-Prop l , λ _ _ → raise-star)

Meets in the poset of propositions

is-meet-semilattice-Prop-Locale :
  {l : Level} → is-meet-semilattice-Poset (Prop-Poset l)
is-meet-semilattice-Prop-Locale P Q =
  ( P ∧ Q , is-greatest-binary-lower-bound-conjunction-Prop P Q)

Prop-Order-Theoretic-Meet-Semilattice :
  (l : Level) → Order-Theoretic-Meet-Semilattice (lsuc l) l
Prop-Order-Theoretic-Meet-Semilattice l =
  Prop-Poset l , is-meet-semilattice-Prop-Locale

Prop-Meet-Semilattice :
  (l : Level) → Meet-Semilattice (lsuc l)
Prop-Meet-Semilattice l =
  meet-semilattice-Order-Theoretic-Meet-Semilattice
    ( Prop-Order-Theoretic-Meet-Semilattice l)

Suprema in the poset of propositions

is-suplattice-lzero-Prop-Locale :
  {l : Level} → is-suplattice-Poset lzero (Prop-Poset l)
is-suplattice-lzero-Prop-Locale I P = (∃ I P , inv-iff ∘ up-exists)

is-suplattice-Prop-Locale :
  {l : Level} → is-suplattice-Poset l (Prop-Poset l)
is-suplattice-Prop-Locale I P = (∃ I P , inv-iff ∘ up-exists)

Prop-Suplattice :
  (l : Level) → Suplattice (lsuc l) l l
Prop-Suplattice l = Prop-Poset l , is-suplattice-Prop-Locale

is-meet-suplattice-Prop-Locale :
  {l : Level} → is-meet-suplattice-Meet-Semilattice l (Prop-Meet-Semilattice l)
is-meet-suplattice-Prop-Locale I P = ？

Prop-Meet-Suplattice :
  (l : Level) → Meet-Suplattice (lsuc l) l
Prop-Meet-Suplattice l =
  Prop-Meet-Semilattice l , is-meet-suplattice-Prop-Locale

The frame of propositions

Prop-Frame : (l : Level) → Frame (lsuc l) l
Prop-Frame l = Prop-Meet-Suplattice l , ？

The locale of propositions

Prop-Locale : Locale lsuc (_⊔_) lzero
Prop-Locale = Prop-Frame

See also

Recent changes