# The preunivalence axiom

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-20.

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