The strong preunivalence axiom

Content created by Fredrik Bakke.

Created on 2025-02-10.
Last modified on 2025-02-10.

module foundation.strong-preunivalence where
Imports 
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.preunivalence
open import foundation.propositional-maps
open import foundation.propositions
open import foundation.sets
open import foundation.small-types
open import foundation.structured-equality-duality
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.function-types

Idea

The strong preunivalence axiom is a common generalization of the univalence axiom and axiom K. It asserts that for any type X : 𝒰 and any other universe 𝒱, the smallness predicate is-small 𝒱 X ≐ Σ (Y : 𝒱), (X ≃ Y) is a set.

The strong preunivalence axiom is a strengthening of the preunivalence axiom in the following way. If we restrict to 𝒱 ≐ 𝒰, subuniverse equality duality says that, for every X : 𝒰, Σ (Y : 𝒰), (X ≃ Y) is a set if and only if every binary family of maps

  (Z Y : 𝒰) → (Z ＝ Y) → (X ≃ Y)

is a binary family of embeddings. The preunivalence axiom asserts that the particular (unary) family of maps (Y : 𝒰) → (X ＝ Y) → (X ≃ Y) defined by identity induction by refl ↦ id-equiv is a family of embeddings.

While the strong preunivalence axiom is a strengthening of the preunivalence axiom, it is still a common generalization of the univalence axiom and axiom K: if we assume the univalence axiom then is-small 𝒱 X is a proposition, and if we assume axiom K then every type is a set.

Definitions

instance-strong-preunivalence :
  {l1 : Level} (l2 : Level) (X : UU l1) → UU (l1 ⊔ lsuc l2)
instance-strong-preunivalence l2 X = is-set (is-small l2 X)

strong-preunivalence-axiom-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
strong-preunivalence-axiom-Level l1 l2 =
  (X : UU l1) → instance-strong-preunivalence l2 X

strong-preunivalence-axiom : UUω
strong-preunivalence-axiom =
  {l1 l2 : Level} → strong-preunivalence-axiom-Level l1 l2

Properties

The strong preunivalence axiom strengthens the preunivalence axiom

based-preunivalence-instance-strong-preunivalence :
  {l : Level} (X : UU l) →
  instance-strong-preunivalence l X → based-preunivalence-axiom X
based-preunivalence-instance-strong-preunivalence X L Y =
  is-emb-is-prop-map
    ( backward-implication-subuniverse-equality-duality
      ( is-prop-Prop)
      ( L)
      ( X)
      ( λ _ → equiv-eq)
      ( Y))

preunivalence-axiom-strong-preunivalence-axiom :
  strong-preunivalence-axiom → preunivalence-axiom
preunivalence-axiom-strong-preunivalence-axiom L X =
  based-preunivalence-instance-strong-preunivalence X (L X)

The strong preunivalence axiom generalizes axiom K

To show that preunivalence generalizes axiom K, we assume axiom K for types of equivalences and for the universe itself.

instance-strong-preunivalence-instance-axiom-K :
  {l1 : Level} (l2 : Level) (A : UU l1) →
  instance-axiom-K (UU l2) →
  ((B : UU l2) → instance-axiom-K (A ≃ B)) →
  instance-strong-preunivalence l2 A
instance-strong-preunivalence-instance-axiom-K l2 A K-Type K-A≃B =
  is-set-Σ (is-set-axiom-K K-Type) (is-set-axiom-K ∘ K-A≃B)

strong-preunivalence-axiom-axiom-K : axiom-K → strong-preunivalence-axiom
strong-preunivalence-axiom-axiom-K K {l1} {l2} A =
  instance-strong-preunivalence-instance-axiom-K l2 A
    ( K (UU l2))
    ( λ B → K (A ≃ B))

The strong preunivalence axiom generalizes the univalence axiom

strong-preunivalence-axiom-univalence-axiom :
  univalence-axiom → strong-preunivalence-axiom
strong-preunivalence-axiom-univalence-axiom UA {l1} {l2} A =
  is-set-is-prop
  ( is-prop-is-proof-irrelevant
    ( λ (X , e) →
      is-contr-equiv'
        ( is-small l2 X)
        ( equiv-tot (equiv-precomp-equiv e))
        ( is-torsorial-equiv-based-univalence X (UA X))))

Strong preunivalence holds in univalent foundations

strong-preunivalence : strong-preunivalence-axiom
strong-preunivalence = strong-preunivalence-axiom-univalence-axiom univalence

See also

Recent changes