HoTTEST Summer School HoTT Notes 4

Universes

Why

• We need to define type families by induction, so that we can prove things like $$ 0 \underset{\mathbb{N}}{=} 1 \rightarrow \varnothing $$
• We should have a method to abstract over types, eg. instead of writing $id_A:A\rightarrow A$ for each type, we can write $id^{\mathcal{U}}:\Pi_{(X:\mathcal{U})} \mathcal{T}(X) \rightarrow \mathcal{T}(X)$
• To do category theory in a streamlined way. (Grothendieck universe¹)

What is a Universe?

In some type theories, especially in systems with dependent types, types themselves can be regarded as terms. There is a type called the universe (often denoted $\mathcal {U}$) which has types as its elements. To avoid paradoxes such as Girard's paradox (an analogue of Russell's paradox for type theory), type theories are often equipped with a countably infinite hierarchy of such universes, with each universe being a term of the next one. —— Wikipedia

Basically it is type of types.

A universe in type theory is a type $\mathcal{U}$ in the empty context, equipped with a type family² $\mathcal{T}$³ over $\mathcal{U}$ called a universal family, that is closed under the type forming operations in the sense that it comes equipped with many existing structures⁴.

How we prevent Russell’s paradox

As I mentioned before, universe is type of types, so a universe can technically in another universe, and this leads to the famous Russell’s paradox.

To prevent this paradox from happening, and keep enough universes to use meanwhile, we organize the universes and types in them in this way:

• For every finite list of types： $$ \Gamma_1 \vdash A_1\ type\ \ \ \ \cdots \ \ \ \ \Gamma_n \vdash A_n\ type $$ there is a universe $\mathcal{U}$ that contains each $A_i$ in the sense that $\mathcal{U}$ comes equipped with $$ \Gamma_i\vdash \check{A_i}:U $$ for which the judgement $$ \Gamma_i\vdash \mathcal{T}(\check{A_i}) \doteq A_i\ type $$ holds.

• $\mathcal{U_0}$ is the universe which contains no types.

• For each universe $\mathcal{U}$, there is a successor universe $\mathcal{U^+}$ that $$ \vdash \mathcal{U}\ type $$ $$ X: \mathcal{U} \vdash \mathcal{T}(X)\ type $$ $$ \vdash \check{\mathcal{U}}: \mathcal{U^+} $$ $$ \vdash \mathcal{T}^+(\check{\mathcal{U}})\doteq \mathcal{U}\ type $$ $$ X:\mathcal{U} \vdash \check{\mathcal{T}}(X): \mathcal{U^+} $$ $$ X:\mathcal{U} \vdash \mathcal{T}^+(\check{\mathcal{T}}(X)) \doteq \mathcal{T}(X)\ type $$ We can have an infinite tower with these universes: $$ \mathcal{U}, \mathcal{U^+}, \mathcal{U^{++}}, \mathcal{U^{+++}}, \cdots $$ and each universe is contained in the next.

• We can join universes, ie. $\mathcal{U} \sqcup \mathcal{V}$ contains all types in $\mathcal{U}$ and $\mathcal{V}$.

Example

Now we'll show why we need these universes.

We'll prove:

$$ true \neq_{bool} false $$

or in other words:

$$ true \underset{bool}{=} false \rightarrow \varnothing $$

So what we want to do is find a term:

$$ \require{bussproofs} \begin{prooftree} \AxiomC {} \UnaryInfC{$?: true \underset{bool}{=}false \rightarrow \varnothing $} \end{prooftree} $$

Start with $\rightarrow-intro$ as usual:

$$ \require{bussproofs} \begin{prooftree} \AxiomC {$t: true \underset{bool}{=}false \vdash ?:\varnothing$} \UnaryInfC{$?: true \underset{bool}{=}false \rightarrow \varnothing$} \end{prooftree} $$

We need a term of $\varnothing$, which can be constructed with "proof with contradiction", we pick $True → False$ and $\neg(True → False)$.

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$t: true \underset{bool}{=}false \vdash\ ? :True → False$} \AxiomC{$?:\neg(True → False)$} \BinaryInfC {$t: true \underset{bool}{=}false \vdash ?:\varnothing$} \UnaryInfC{$?: true \underset{bool}{=}false \rightarrow \varnothing$} \end{prooftree} $$

For $True → False$, we can use transport we mentioned in last lecture with a function (or dependent type constructor) $boolToType$. And you'll see why we need universes here, we need it to write the return type of this function.

$$ \displaylines { boolToType : Bool \rightarrow \mathcal{U}\\ boolToType true \doteq \mathbb{1}\\ boolToType false \doteq \varnothing\\ } $$

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$t: true \underset{bool}{=}false \vdash tr_{bool}(t): True → False$} \AxiomC{$?:\neg(True → False)$} \BinaryInfC {$t: true \underset{bool}{=}false \vdash ?:\varnothing$} \UnaryInfC{$?: true \underset{bool}{=}false \rightarrow \varnothing$} \end{prooftree} $$

For $\neg(True → False)$, it's quiet easy to construct a term.

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$t: true \underset{bool}{=}false \vdash tr_{bool}(t): True → False$} \AxiomC{$h: True \rightarrow False \vdash ind_{\varnothing}(h\ True):(True → False) → False$} \BinaryInfC {$t: true \underset{bool}{=}false, h:True \rightarrow False \vdash ?:\varnothing$} \UnaryInfC{$?: true \underset{bool}{=}false \rightarrow \varnothing$} \end{prooftree} $$

And fill the $?$s:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$t: true \underset{bool}{=}false \vdash tr_{bool}(t): True → False$} \AxiomC{$h: True \rightarrow False \vdash ind_{\varnothing}(h\ True):(True → False) → False$} \BinaryInfC {$t: true \underset{bool}{=}false \vdash absurd(tr_{bool}(t), \lambda h.ind_{\varnothing}(h\ True)):\varnothing$} \UnaryInfC{$\lambda t.absurd(tr_{bool}(t), \lambda h.ind_{\varnothing}(h\ True)): true \underset{bool}{=}false \rightarrow \varnothing$} \end{prooftree} $$

In lean, I won't use Agda this time since in Agda a simple λ () will do the prove, it's convenient but too far from what we want to show here:

def boolToType x :=
  match x with
  | true   => True
  | false  => False

theorem notTrueImpliesFalseType : ¬(True → False) :=
  λ (h: True → False) => False.elim (h True.intro)

theorem trueIsNotFalse : true ≠ false :=
  Ne.intro
    λ (t: true = false) => absurd (Eq.mp (congrArg boolToType t)) notTrueImpliesFalseType

Observational equality of the natural numbers

In dependent type theory, sometimes one could inductively define an equality type directly on an inductive type, rather than using Martin-Loef’s identity types using the j-rule. This equality type is called observational equality. —— nLab

We define the observational equality of natural numbers like:

$$ Eq_{\mathbb{N}} : \mathbb{N} → (\mathbb{N} → \mathcal{U}_0) $$

$$ Eq_{\mathbb{N}}\ 0\ 0 \doteq \mathbb{1} $$

$$ Eq_{\mathbb{N}}\ succ(n)\ 0 \doteq \varnothing $$

$$ Eq_{\mathbb{N}}\ 0\ succ(n) \doteq \varnothing $$

$$ Eq_{\mathbb{N}}\ succ(m)\ succ(n) \doteq Eq_{\mathbb{N}}\ m\ n $$

Curry-Howard interpretation

Definition omitted, since we've already very familiar with it.

Example

We define: if $d, n: \mathbb{N}$, then we can say d divides n if there exists an element of type

$$ m | n := \Sigma_{(k:ℕ)}{k \times m = n} $$

And we can write some properties of division like:

Every natural number is divisible by 1 and itself

$$ \Pi_{(n:ℕ)}{1 | n ∧ n | n} $$

Proof⁵:

open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Nat.Divisibility using (_∣_; divides)
open import Data.Nat.Properties using (*-identityʳ; *-identityˡ)
open import Relation.Binary.PropositionalEquality using (sym)
open import Data.Product renaming (_×_ to _∧_)

div1 : ∀ (n : ℕ) → 1 ∣ n
div1 n = divides n (sym (*-identityʳ n)) 

divn : ∀ (n : ℕ) → n ∣ n
divn n = divides 1 (sym (*-identityˡ n))

div1n : ∀ (n : ℕ) → (1 ∣ n) ∧ (n ∣ n)
div1n n = (div1 n) , (divn n)

Every natural number divides 0

div0 : ∀ (n : ℕ) → n ∣ 0
div0 n = divides zero refl

Axiom of Choice in Type Theory

I knew what AC is intuitively, it means we can find a choice function for any set in a collection of sets to select an element of it out, now I'll show the formalized form:

$$ \forall X [\varnothing \notin X \Rightarrow \exists f:X\rightarrow \bigcup X \ \ \ \ \forall A \in X(f(A) \in A)] $$

Or in type theory:

$$ \Pi_{(x:A)}\Sigma_{(y:B)}R(x, y) \rightarrow \Sigma_{(f: A\rightarrow B)} \Pi_{(x:A)} R(x, f(x)) $$

This is actually provable:

open import Data.Product

choice : {A B : Set} {R : A → B → Set} →
   ((x : A) → Σ B (λ y → R x y)) →
   Σ (A → B) (λ f → (x : A) → R x (f x))
choice h = (λ z → fst (h z)) , (λ x → snd (h x))

And the reverse proposition is also provable:

$$ \Sigma_{(f: A\rightarrow B)} \Pi_{(x:A)} R(x, f(x)) \rightarrow \Pi_{(x:A)}\Sigma_{(y:B)}R(x, y) $$

choice-rev : {A B : Set} (R : A → B → Set) →
   Σ (A → B) (λ f → (x : A) → R x (f x)) →
   ((x : A) → Σ B (λ y → R x y))
choice-rev R h' = λ x → (fst h' x) , (snd h' x)

However this direct "Curry-Howard translation" of AC is not as powerful as it is in set theory, I guess we move the complexity of AC to somewhere else in the type theory. Anyway, we'll see a more complex form of AC representing in later courses.

Materials

Lecture Note

HoTTEST_Lecture_4.pdf

Record on Youtube