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
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


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.


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)


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)

  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-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)

  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