The preunivalence axiom

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-20.
Last modified on 2024-01-31.

module foundation.preunivalence where
Imports 
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.sets
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.subtypes

Idea

The preunivalence axiom, or axiom L, which is due to Peter Lumsdaine, asserts that for any two types X and Y in a common universe, the map X ＝ Y → X ≃ Y is an embedding. This axiom is a common generalization of the univalence axiom and axiom K.

Definition

instance-preunivalence : {l : Level} (X Y : UU l) → UU (lsuc l)
instance-preunivalence X Y = is-emb (equiv-eq {A = X} {B = Y})

based-preunivalence-axiom : {l : Level} (X : UU l) → UU (lsuc l)
based-preunivalence-axiom {l} X = (Y : UU l) → instance-preunivalence X Y

preunivalence-axiom-Level : (l : Level) → UU (lsuc l)
preunivalence-axiom-Level l = (X Y : UU l) → instance-preunivalence X Y

preunivalence-axiom : UUω
preunivalence-axiom = {l : Level} → preunivalence-axiom-Level l

emb-preunivalence :
  preunivalence-axiom → {l : Level} (X Y : UU l) → (X ＝ Y) ↪ (X ≃ Y)
pr1 (emb-preunivalence L X Y) = equiv-eq
pr2 (emb-preunivalence L X Y) = L X Y

emb-map-preunivalence :
  preunivalence-axiom → {l : Level} (X Y : UU l) → (X ＝ Y) ↪ (X → Y)
emb-map-preunivalence L X Y =
  comp-emb (emb-subtype is-equiv-Prop) (emb-preunivalence L X Y)

Properties

Preunivalence generalizes axiom K

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

module _
  {l : Level} (A B : UU l)
  where

  instance-preunivalence-instance-axiom-K :
    instance-axiom-K (UU l) → instance-axiom-K A → instance-axiom-K B →
    instance-preunivalence A B
  instance-preunivalence-instance-axiom-K K-Type K-A K-B =
    is-emb-is-prop-is-set
      ( is-set-axiom-K K-Type A B)
      ( is-set-equiv-is-set (is-set-axiom-K K-A) (is-set-axiom-K K-B))

preunivalence-axiom-axiom-K : axiom-K → preunivalence-axiom
preunivalence-axiom-axiom-K K {l} X Y =
  instance-preunivalence-instance-axiom-K X Y (K (UU l)) (K X) (K Y)

Preunivalence generalizes univalence

module _
  {l : Level} (A B : UU l)
  where

  instance-preunivalence-instance-univalence :
    instance-univalence A B → instance-preunivalence A B
  instance-preunivalence-instance-univalence = is-emb-is-equiv

preunivalence-axiom-univalence-axiom : univalence-axiom → preunivalence-axiom
preunivalence-axiom-univalence-axiom UA X Y =
  instance-preunivalence-instance-univalence X Y (UA X Y)

Preunivalence holds in univalent foundations

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

See also

Recent changes