{-# OPTIONS --without-K --exact-split --two-level #-}

module Extension.Univalence where

open import Extension.Prelude

private
  variable
    𝓤 : Level

-- Univalence as a hypothesis, rather than the ambient library constant.
Univalence : (𝓤 : Level) → UU (lsuc 𝓤)
Univalence 𝓤 = (A B : UU 𝓤) → isEquiv (idtoeqv {A = A} {B = B})

-- The inverse of idtoeqv supplied by a chosen univalence witness.
ua-from : {A B : UU 𝓤} → Univalence 𝓤 → A ≃ B → Id A B
ua-from {A = A} {B = B} U = inv idtoeqv (U A B)

ua-from-β : {A B : UU 𝓤} (U : Univalence 𝓤) (e : A ≃ B)
          → Id (idtoeqv (ua-from U e)) e
ua-from-β {A = A} {B = B} U = inv-is-section idtoeqv (U A B)