Contents

  1. Kinds
  2. Global Univalence
  3. Global function extensionality
  4. Global univalence implies global function extensionality
{-# OPTIONS --without-K --safe #-}

module univalence-global where 

open import mltt
open import twocatconstructions
open import basichomotopy
open import univalence-base
open import univalence-funext

open ≡-Reasoning
open ◾-lemmas

A global univalence axiom is one that applies to all universes. Similarly for global function extensionality. Doing so is occasionally simpler than lifting things between universes. It requires grappling with the consequences of universe polymorphism in Agda, in particular with Setω.

Kinds

In brief, according to the docs, although one might think that the universe hierarchy Set₀, Set₁, … exists so that any expression can have a type, universe polymorphism, i.e. ability to abstract an expression over the universe level break this again.

As an example, consider the possibility of defining a universe-dependent Unit type:

data Unit (ℓ : Level) : Set ℓ where
  <> : Unit ℓ

Its type is

Unit : (ℓ : Level) → Set ℓ

The right-hand side is a well-defined Agda expression, but it does not belong to any Universe, because, if it did, its type would have to be something like

Level → Universe

where Universe would have to be some sort of container for all the Set ℓ. But since all the terms of Universe are types, Universe is itself a universe and then we would have Universe : Universe, bringing us back to the usual paradoxes. Thus the expression

(ℓ : Level) → Set ℓ

is a type, but does not have a type. It does have a “kind”, which Agda calls Setω.

Setω is a valid Agda type, but it cannot appear as part of an Agda term. Compare:

LargeType : Setω
LargeType = (ℓ : Level) → Set ℓ

which is valid Agda code, with

Large𝟚 : ((ℓ : Level) → Set ℓ) → ((ℓ : Level) → Set ℓ)
Large𝟚 = Unit + Unit

which is not. This is different from the evaluation at specific levels, as in:

Poly𝟚 : (ℓ : Level) → Set ℓ
Poly𝟚 ℓ = Unit ℓ + Unit ℓ

which type-checks just fine.

top ⇑

Global Univalence

Global Univalence is simply the statement that all universes are univalent. Since we are quantifying over the universe levels, we must use the kind Setω in order to be able to state it. Aside from this difference, the stance is the same: by wriing its kind, we are free to assume a term of that kind whenever we wish to assume the axiom of global univalence.

Univalence : Setω
Univalence = (ℓ : Level) → is-univalent ℓ

top ⇑

Global function extensionality

Same thing for global function extensionality:

HFunext : Setω
HFunext = (ℓ ℓ' : Level) → hfunext ℓ ℓ'

DFunext : Setω
DFunext = (ℓ ℓ' : Level) → dfunext ℓ ℓ'

top ⇑

Global univalence implies global function extensionality

Univalence→HFunext : Univalence → HFunext
Univalence→HFunext UA ℓ ℓ' = univalence→hfunext (UA (ℓ ⊔ ℓ'))

Univalence→DFunext : Univalence → DFunext
Univalence→DFunext UA ℓ ℓ' = univalence→dfunext (UA (ℓ ⊔ ℓ'))

top ⇑