Axiom L

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Fernando Chu, Julian KG, fernabnor and louismntnu.

Created on 2022-08-26.
Last modified on 2023-06-25.

module foundation.axiom-l where
Imports 
open import foundation.dependent-pair-types
open import foundation.sets
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.univalence

Idea

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, in the sense that both univalence and axiom K imply axiom L.

Definition

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

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

Properties

Axiom L generalizes the univalence axiom

axiom-L-univalence :
  {l : Level} → ((A B : UU l) → UNIVALENCE A B) → axiom-L l
axiom-L-univalence ua A B = is-emb-is-equiv (ua A B)

Axiom L generalizes axiom K

axiom-L-axiom-K :
  {l : Level} → ((A : UU l) → axiom-K A) → axiom-K (UU l) → axiom-L l
axiom-L-axiom-K K K-UU A B =
  is-emb-is-prop-is-set
    ( is-set-axiom-K K-UU A B)
    ( is-set-equiv-is-set
      ( is-set-axiom-K (K A))
      ( is-set-axiom-K (K B)))

See also

Recent changes