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


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.


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


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