Large 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.large-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.propositions
open import foundation.unit-type
open import foundation.universe-levels

open import orthogonal-factorization-systems.lawvere-tierney-topologies

Idea

A {#concept “Lawvere–Tierney topology” Disambiguation=“on types”} on types is a hierarchy of maps

  j : {l : Level} → Prop l → Prop (δ l)

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

record
  is-large-lawvere-tierney-topology
    {δ : Level → Level} (j : {l : Level} → Prop l → Prop (δ l)) : UUω
  where
  field
    is-idempotent-is-large-lawvere-tierney-topology :
      {l : Level} (P : Prop l) → type-Prop (j (j P) ⇔ j P)

    preserves-unit-is-large-lawvere-tierney-topology :
      type-Prop (j unit-Prop ⇔ unit-Prop)

    preserves-conjunction-is-large-lawvere-tierney-topology :
      {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
      type-Prop (j (P ∧ Q) ⇔ j P ∧ j Q)

open is-large-lawvere-tierney-topology public

The large type of Lawvere-Tierney topologies

record
  large-lawvere-tierney-topology (δ : Level → Level) : UUω
  where
  field
    operator-large-lawvere-tierney-topology : {l : Level} → Prop l → Prop (δ l)

    is-large-lawvere-tierney-topology-large-lawvere-tierney-topology :
      is-large-lawvere-tierney-topology operator-large-lawvere-tierney-topology

  is-idempotent-large-lawvere-tierney-topology :
    {l : Level} (P : Prop l) →
    type-Prop
      ( operator-large-lawvere-tierney-topology
        ( operator-large-lawvere-tierney-topology P) ⇔
        operator-large-lawvere-tierney-topology P)
  is-idempotent-large-lawvere-tierney-topology =
    is-idempotent-is-large-lawvere-tierney-topology
      ( is-large-lawvere-tierney-topology-large-lawvere-tierney-topology)

  preserves-unit-large-lawvere-tierney-topology :
    type-Prop (operator-large-lawvere-tierney-topology unit-Prop ⇔ unit-Prop)
  preserves-unit-large-lawvere-tierney-topology =
    preserves-unit-is-large-lawvere-tierney-topology
      ( is-large-lawvere-tierney-topology-large-lawvere-tierney-topology)

  preserves-conjunction-large-lawvere-tierney-topology :
    {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
    type-Prop
      ( operator-large-lawvere-tierney-topology (P ∧ Q) ⇔
        operator-large-lawvere-tierney-topology P ∧
        operator-large-lawvere-tierney-topology Q)
  preserves-conjunction-large-lawvere-tierney-topology =
    preserves-conjunction-is-large-lawvere-tierney-topology
      ( is-large-lawvere-tierney-topology-large-lawvere-tierney-topology)

  type-operator-large-lawvere-tierney-topology : {l : Level} → Prop l → UU (δ l)
  type-operator-large-lawvere-tierney-topology =
    type-Prop ∘ operator-large-lawvere-tierney-topology

open large-lawvere-tierney-topology public

Examples

The identity large Lawvere-Tierney topology

is-large-lawvere-tierney-topology-id : is-large-lawvere-tierney-topology id
is-large-lawvere-tierney-topology-id =
  λ where
  .is-idempotent-is-large-lawvere-tierney-topology P → id-iff
  .preserves-unit-is-large-lawvere-tierney-topology → id-iff
  .preserves-conjunction-is-large-lawvere-tierney-topology P Q → id-iff

id-large-lawvere-tierney-topology : large-lawvere-tierney-topology (λ l → l)
id-large-lawvere-tierney-topology =
  λ where
  .operator-large-lawvere-tierney-topology →
    id
  .is-large-lawvere-tierney-topology-large-lawvere-tierney-topology →
    is-large-lawvere-tierney-topology-id

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