{-# OPTIONS --without-K #-}
module Util.HoTT.Univalence.Statement where

open import Util.HoTT.Equiv
open import Util.Prelude


Univalence :  α  Set (lsuc α)
Univalence α = {A B : Set α}  IsEquiv (≡→≃ {A = A} {B = B})