# Axiom L

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

Created on 2022-08-26.

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