Lawvere–Tierney topologies

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-11-05.
Last modified on 2024-11-05.

module orthogonal-factorization-systems.lawvere-tierney-topologies where
Imports 
open import foundation.cartesian-product-types
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.logical-equivalences
open import foundation.propositional-extensionality
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.unit-type
open import foundation.universe-levels

Idea

A (small) {#concept “Lawvere–Tierney topology” Disambiguation=“on types”} on types is a map

  j : Prop → Prop

that is idempotent and preserves the unit type and binary products

  j (j P) ≃ j P      j unit ≃ unit      j (P ∧ Q) ≃ j P ∧ j Q

such operations give rise to a notion of j-sheaves of types.

Definitions

The predicate on an operator on propositions of defining a Lawvere-Tierney topology

module _
  {l : Level} (j : Prop l → Prop l)
  where

  is-lawvere-tierney-topology-Prop : Prop (lsuc l)
  is-lawvere-tierney-topology-Prop =
    product-Prop
      ( Π-Prop (Prop l) (λ P → j (j P) ⇔ j P))
      ( product-Prop
        ( j (raise-unit-Prop l) ⇔ unit-Prop)
        ( Π-Prop
          ( Prop l)
          ( λ P →
            Π-Prop (Prop l) (λ Q → j (P ∧ Q) ⇔ j P ∧ j Q))))

  is-lawvere-tierney-topology : UU (lsuc l)
  is-lawvere-tierney-topology = type-Prop is-lawvere-tierney-topology-Prop

  is-prop-is-lawvere-tierney-topology : is-prop is-lawvere-tierney-topology
  is-prop-is-lawvere-tierney-topology =
    is-prop-type-Prop is-lawvere-tierney-topology-Prop

The set of Lawvere-Tierney topologies

lawvere-tierney-topology : (l : Level) → UU (lsuc l)
lawvere-tierney-topology l = Σ (Prop l → Prop l) (is-lawvere-tierney-topology)

is-set-lawvere-tierney-topology :
  {l : Level} → is-set (lawvere-tierney-topology l)
is-set-lawvere-tierney-topology =
  is-set-type-subtype is-lawvere-tierney-topology-Prop (is-set-subtype)

set-lawvere-tierney-topology : (l : Level) → Set (lsuc l)
set-lawvere-tierney-topology l =
  (lawvere-tierney-topology l , is-set-lawvere-tierney-topology)

Examples

The identity function on propositions defines a Lawvere–Tierney topology

is-lawvere-tierney-topology-id :
  (l : Level) → (is-lawvere-tierney-topology (id {A = Prop l}))
pr1 (is-lawvere-tierney-topology-id l) P =
  id-iff
pr1 (pr2 (is-lawvere-tierney-topology-id l)) =
  iff-equiv (inv-compute-raise-unit l)
pr2 (pr2 (is-lawvere-tierney-topology-id l)) Q P =
  id-iff

id-lawvere-tierney-topology : (l : Level) → lawvere-tierney-topology l
id-lawvere-tierney-topology l = (id , is-lawvere-tierney-topology-id l)

See also

References

Lawvere–Tierney topologies in the context of Homotopy Type Theory are introduced and studied in Chapter 6 of [Qui16].

[Qui16]
Kevin Quirin. Lawvere–Tierney sheafification in Homotopy Type Theory. PhD thesis, École des Mines de Nantes, December 2016. URL: https://kevinquirin.github.io/thesis/main.pdf.

Recent changes