=====================================
  Introduction to Univalent Foundations
  =====================================


In this course, I will give a very brief overview of Univalent
Foundations.  The overview is necessarily incomplete. I will give
pointers to further material in the course of the lecture, in the form
"[Section X.Y]". Such a pointer refers to Section X.Y of the book

Homotopy Type Theory: Univalent Foundations of Mathematics

which is available under a free license from

https://homotopytypetheory.org/book/ .


\begin{code}

--this flag changes the behaviour of Agda with respect to the equality
--type; we need to activate the flag to switch to "path" mode

{-# OPTIONS --without-K #-}
--{-# OPTIONS --type-in-type #-}


Type : Set₁
Type = Set

\end{code}


Types and terms
===============

Unit type
---------

We define the Unit type with a single element tt:

\begin{code}

data Unit : Type where
  tt : Unit

rec_Unit : {A : Type} (a : A) → Unit → A
rec_Unit a tt = a

\end{code}


Type of Booleans
----------------

\begin{code}

data Bool : Type where
  true : Bool
  false : Bool

rec_Bool : {A : Type} (a a' : A) → Bool → A
rec_Bool a a' true = a
rec_Bool a a' false = a'

\end{code}


Type of natural numbers
-----------------------

\begin{code}

data Nat : Type where
  zero : Nat
  succ : Nat → Nat

rec_Nat : {A : Type} (z : A) (s : A → A) → Nat → A
rec_Nat z s zero = z
rec_Nat z s (succ n) = s (rec_Nat z s n)

\end{code}



Type of pairs (cartesian product)
---------------------------------

The type A × B

\begin{code}

data _×_ (A B : Type) : Type where
  _,_ : A → B → A × B


swap : {A B : Type} → A × B → B × A
swap (a , b) = (b , a)

rec-× : {A B C : Type} (p : A → B → C) → A × B → C
rec-× p (a , b) = p a b

fst : {A B : Type} → A × B → A
fst (a , b) = a

snd : {A B : Type} → A × B → B
snd (a , b) = b

\end{code}




Type of dependent pairs
-----------------------

We define the type of dependent pairs, and the cartesian product as a
special case afterwards.

\begin{code}

data Σ {X : Type} (T : X → Type) : Type where
  _,,_ : (x : X) (y : T x) → Σ T

Σ-pr1 : {X : Type} {T : X → Type} → Σ T → X
Σ-pr1 (a ,, b) = a

Σ-pr2 : {X : Type} {T : X → Type} (t : Σ T) → T (Σ-pr1 t)
Σ-pr2 (a ,, b) = b


\end{code}

Exercises:
----------

Write a function of type A × B → B × A
\begin{code}
\end{code}


Write a function of type (A × B) × C → A × (B × C)
\begin{code}
assoc : {A B C : Type} → (A × B) × C → A × (B × C)
assoc t = fst (fst t), (snd (fst t) , snd t)
\end{code}



The type of paths
=================


\begin{code}

module UF where

data _⟿_ {X : Type} : X → X → Type where
  Id-Path : (x : X) → x ⟿ x

\end{code}

[Section 1.12]

Exercise: write a term of type pr2 (tt , false) ⟿ false
\begin{code}

foo : snd ( tt , false) ⟿ false
foo = Id-Path false

\end{code}


Given a predicate T : X → Type on X, it can be transported along a
path:

\begin{code}

transport : {X : Type} (T : X → Type)
  → {a b : X}
  → (e : a ⟿ b )
  → T a → T b
transport T (Id-Path _) p = p

\end{code}


swap is an involution:

\begin{code}

swap-involution : {A B : Type} (t : A × B) → swap(swap t) ⟿ t
swap-involution (a , b) = Id-Path (a , b)

\end{code}



Paths between paths
===================


\begin{code}

J : {X : Type}
  → (P : (x y : X) → x ⟿ y → Type)
  → ((x : X) → P x x (Id-Path x))
  → (x y : X) (p : x ⟿ y) → P x y p
J A f _ _ (Id-Path x) = f x

\end{code}



We can deform any path from x to y into the the constant path on x:


\begin{code}

ConeContraction : {X : Type} (x : X)
  → (y : X) (q : x ⟿ y)
  → (y ,, q) ⟿ (x ,, (Id-Path x))
ConeContraction x _ (Id-Path .x)  = Id-Path (x ,, Id-Path x)

\end{code}


Operations on paths
===================

See also [Section 2.1].

We have operations on paths analogous to those on equalities:
- symmetry becomes path inversion (going a path backwards)
- transitivity becomes concatenation of paths

These operations are analogous to reversal and concatentation of lists
or vectors.

\begin{code}

inv : {X : Type}
  → {a b : X}
  → a ⟿ b → b ⟿ a
inv (Id-Path a) = Id-Path a

_·_ : {X : Type}
  → {a b c : X}
  → a ⟿ b
  → b ⟿ c
  → a ⟿ c
Id-Path a · p = p

\end{code}


We can show that thes operations on paths satisfy some laws
reminiscent of the group laws: - associativity - left and right
neutrality - inverse

Actually, since these laws hold up to a "path between paths",
we call them "(higher) groupoid laws":

\begin{code}

·-assoc : {X : Type} {a b c d : X}
  → (p : a ⟿ b)
  → (q : b ⟿ c)
  → (r : c ⟿ d)
  → (p · (q · r)) ⟿ ((p · q) · r)
·-assoc (Id-Path a) q r = Id-Path (q · r)

·Id-Path : {X : Type} {a b : X}
  → (p : a ⟿ b)
  → (p · Id-Path b) ⟿ p
·Id-Path (Id-Path a) = Id-Path (Id-Path a)

Id-Path· : {X : Type} {a b : X}
  → (p : a ⟿ b)
  → (Id-Path a · p) ⟿ p
Id-Path· (Id-Path a) = Id-Path (Id-Path a)

inv· : {X : Type}
  → {a b : X}
  → (p : a ⟿ b)
  → ((inv p) · p) ⟿ Id-Path b
inv· (Id-Path x) = Id-Path (Id-Path x)


\end{code}


More operations involving paths
===============================


A function f : X → Y not only maps points of X to
points of Y; it also maps paths in X to paths in Y:

\begin{code}

function-on-paths : {X Y : Type}
  → (f : X → Y)
  → {a b : X}
  → a ⟿ b
  → f a ⟿ f b
function-on-paths f (Id-Path x) = Id-Path (f x)

\end{code}




Propositions
============

See also [Section 3.3].

In one of the first lectures, you have learned about the
"propositions-as-types" paradigm. There, you have learned that any
type can be considered a proposition, and its elements are the proofs
of that proposition. In particular, you learned about ⊤ ⊥ ∧ ∨ (and
Σ?).

In Univalent Foundations, only those types that satisfy a certain
condition will be called "proposition":

\begin{code}

is-a-proposition : Type → Type
is-a-proposition X = (a b : X) → a ⟿ b

\end{code}

A proposition is hence a type in which any two points are connected by
a path. Reading ⟿ as ≡ , it means that a proposition has at most one
element.

Here are some examples of types that are propositions:

\begin{code}

data ⊥ : Type where

data ⊤ : Type where
  tt : ⊤

×-Path : {A B : Type}
  → {a a' : A}
  → {b b' : B}
  → (a ⟿ a') → (b ⟿ b')
  → (a , b) ⟿ (a' , b')
×-Path (Id-Path a) (Id-Path b) = Id-Path (a , b)


is-a-proposition-⊤ : is-a-proposition ⊤ 
is-a-proposition-⊤ tt tt = Id-Path tt

is-a-proposition-⊥ : is-a-proposition ⊥
is-a-proposition-⊥ a = λ ()

is-a-proposition_× : (X Y : Type)
  → is-a-proposition X
  → is-a-proposition Y
  → is-a-proposition (X × Y)
is-a-proposition_× X Y pX pY (a , b) (a' , b') = goal
  where
    p1 : a ⟿ a'
    p1 = pX a a'
    p2 : b ⟿ b'
    p2 = pY b b'
    goal : (a , b) ⟿ (a' , b')
    goal = ×-Path p1 p2

\end{code}

What about X ∨ Y ?

Even when X and Y are propositions, X ∨ Y does not need to be one.
Consider ⊤ ∨ ⊤:

\begin{code}

data _∨_ (X Y : Type) : Type where
  inl : X → X ∨ Y
  inr : Y → X ∨ Y

no-path-inl-inr : {X Y : Type}
  {a : X} {b : Y}
  → inl a ⟿ inr b → ⊥
no-path-inl-inr ()

not-a-proposition-⊤∨⊤ : is-a-proposition (⊤ ∨ ⊤) → ⊥
not-a-proposition-⊤∨⊤  x = goal
  where
    impossible-path : inl tt ⟿ inr tt
    impossible-path = x (inl tt) (inr tt)
    goal : ⊥
    goal = no-path-inl-inr impossible-path
    
\end{code}


To fix the problem that X ∨ Y is not a proposition, an additional type
constructor is added to type theory in Univalent Foundations: the
*propositional truncation*.

This type constructor associates to any type X another type, written
∥X∥, with the following structure:

1. ∥X∥ is a proposition
2. There is a function X → ∥X∥
3. Any map X → B with B a proposition factors via X → ∥X∥.

Intuitively, ∥X∥ is isomorphic to ⊤ if X is inhabited, and isomorphic
to ⊥ if X is empty.



Levels of types
===============

See also [Section 7].

In this section, we look at conditions that are analogous to that of
being a proposition.

Recall that a type X is a proposition if there is a path between any
two points of X. For reasons that will become clear later, we also say
that a type that is a proposition is *of level 1*.


We can also look at the following, similar, condition:

We say that "X is of level 2" if there is a path between any two
(parallel) paths between any two points of X.
Intuitively, this means that the space X has no "holes".

\begin{code}

is-of-level-2 : Type →  Type
is-of-level-2 X = (a b : X) (p q : a ⟿ b) → p ⟿ q

\end{code}

As we have seen, in the mode with K, one could show that there is a
path between any two paths between any x and y of a type X.  That
means that *with K, any type is of level 2*.

Without K, we can not show that every type is of level 2. But, with
the type theory that I have presented so far, we can also not
construct a type that is not of level 2. Indeed, defining a type that
is not of level 2 requires an additional axiom (postulate).


Examples of types of level 2:

1) Any type of level 1 is also of level 2.
2) The type bool is of level 2, but not of level 1.
3) The type nat of natural numbers is of level 2.

That is, a type is of level 2 if "there is a path between any
two (parallel) paths".

We can show that the booleans are of level 2, but not of level 1:

\begin{code}

bool-is-of-level-2 : is-of-level-2 Bool
bool-is-of-level-2 true .true (Id-Path .true) (Id-Path .true) =
  Id-Path (Id-Path true)
bool-is-of-level-2 false .false (Id-Path .false) (Id-Path .false) =
  Id-Path (Id-Path false)

not-bool-is-a-proposition : is-a-proposition Bool → ⊥
not-bool-is-a-proposition x = goal
  where
    T : Bool → Type
    T true = ⊤
    T false = ⊥
    f : T true → T false
    f = transport T (x true false)
    goal : ⊥
    goal = f tt

\end{code}


We can continue giving analogous definitions for any level n:

Say that the type  X is
- of level 1 if there is a path between any two points
- of level 2 if there is a path between any two paths between points
- of level 3 if there is a path between any two paths between any two paths between points
- of level 4 if......

We are missing level 0! We say that X is of level 0 if
- it has a distinguished element; and
- any other element has a path to that element

\begin{code}

data nat : Type where
  zero : nat
  succ : nat → nat

is-singleton : Type → Type
is-singleton X = Σ \(a : X) → (b : X) → a ⟿ b

is-of-level : (n : nat) → Type → Type
is-of-level zero X = is-singleton X
is-of-level (succ n) X = (a b : X) → is-of-level n (a ⟿ b) 

\end{code}

Showing that
`is-of-level 1`
is actually the same as
`is-a-proposition`
involves a small trick. Try at home!?

It can be shown that type constructors "are closed under levels":

* The cartesian product X × Y is of level n if X and Y are of level n.

* The function type X → Y is of level n if the target type Y is.

* The Sigma type ∑ \(x : X) → T x is of level n if X is and all (T x) are.

* The product type (x : X) → T x is of level n if all (T x) are.

* The type of lists over A is of level n if A is.

* ...


Actually, not all of these are provable without an axiom (a postulate)
that we will add:
the axiom of "function extensionality" is required to show that the level
is stable under product and function types.


Function extensionality
=======================

See also [Section 2.9].

Stating this axiom requires some work. If we think in terms of equality,
the axiom says that two functions are equal if they are pointwise equal:

postulate
  funext : (X Y : Type) (f g : X → Y) → ( (x : X) → f x ≡ g x ) → f ≡ g

In terms of paths, however, this is not the right formulation of this axiom.
The above postulate, expressed with paths, would give us *some* path f ⟿ g
from a family of paths (x : X) → f x ⟿ g x,
but we would not know how to reason about this path.

What we want to say instead is that the type of paths  f ⟿ g is
"the same" as the type of families ( (a : X) → f x ⟿ g x ).
In other words, we should say that these two types are *isomorphic*.

However, we do not want just any isomorphism between those two types;
we want an isomorphism that maps

Id-Path f   ---------->   \(x : X) → Id-Path (f x)

We first define a map from paths between functions to families of pointwise
paths:

\begin{code}

to-prod-paths : {X : Type} {T : X → Type}
  {f g : (a : X) → T a}
  → f ⟿ g → (a : X) → f a ⟿ g a
to-prod-paths (Id-Path f) a = Id-Path (f a)

\end{code}


Our new "function extensionality axiom should say that, for
any f, g : X → Y,

to-prod-paths {f} {g}

is an isomorphism.

We say that a function f : X → Y is an isomorphism by saying that the preimage
of any b : Y is a singleton.

\begin{code}

fiber : {X Y : Type} → (X → Y) → Y → Type
fiber f b = Σ \a → (f a) ⟿  b

is-iso : {X Y : Type} (f : X → Y) → Type
is-iso {X} {Y} f = (b : Y) → is-singleton (fiber f b)

iso  : Type → Type → Type
iso X Y = Σ λ (f : X → Y) →  is-iso f

postulate
  path-funext : {X : Type} {Y : X → Type} (f g : (a : X) → Y a)
    → is-iso (to-prod-paths {X} {Y} {f} {g})

\end{code}


With this postulate path-funext, we can show the stability of levels
under the aforementioned constructions.


Universes and the univalence axiom
==================================

See also [Section 2.10].


Unfortunately, I have not learned enough about Agda in time to teach
you about universes in Agda. As a consequence, at the end of this
section, there is some code that does not compile.

About universes: see blackboard explanation.

\begin{code}

id : (X : Type) → X → X
id X x = x

singleton-type : {X : Type} → X → Type
singleton-type x = Σ \y → y ⟿ x

η : {X : Type} (x : X) → singleton-type x
η x = (x ,, Id-Path x)

singleton-types-are-singletons : {X : Type} (x : X) → is-singleton(singleton-type x)
singleton-types-are-singletons {X} = h
 where
  A : (y x : X) → y ⟿ x → Type
  A y x p = (η x) ⟿ (y ,, p)
  f : (x : X) → A x x (Id-Path x)
  f x = Id-Path (η x)
  φ : (y x : X) (p : y ⟿ x) → (η x) ⟿ (y ,, p)
  φ = J A f
  g : (x : X) (σ : singleton-type x) → (η x) ⟿ σ
  g x (y ,, p) = φ y x p
  h : (x : X) → Σ \(c : singleton-type x) → (σ : singleton-type x) → c ⟿ σ
  h x = (η x ,, g x)


idIsEquiv : (X : Type) → is-iso(id X)
idIsEquiv X = g
 where
  g : (x : X) → is-singleton (fiber (id X) x)
  g = singleton-types-are-singletons

\end{code}



The following results in a universe problem, and hence does not
compile. The problem is that the type of paths is defined for types
that are elements of "Type", not for "Type" itself.

Put differently, given X : Type and x and y in X, we have defined
x ⟿_X y ,
where we make the type X explicit. But we have not defined
X ⟿_Type Y yet.

The following code is a sketch of what the univalence axiom looks like
naïvely.

You *can* make the code compile by uncommenting the --type-in-type
pragma at the beginning of the file.


IdToEq : (X Y : Type) → X ⟿ Y → iso X Y
IdToEq = J A f
 where
  A : (X Y : Type) → X ⟿ Y → Type
  A X Y p = iso X Y
  f : (X : Type) → A X X (Id-Path X)
  f X = (id X ,, idIsEquiv X)

isUnivalent : Type
isUnivalent = (X Y : Type) → is-iso (IdToEq X Y)


For a proper formulation of the Univalence Axiom, see Martin Escardo's
article "A self-contained, brief and complete formulation of
Voevodsky's Univalence Axiom" and the accompanying Agda file at
https://arxiv.org/abs/1803.02294







Paths in cartesian products
===========================

As an example, we consider the cartesian product type:

\begin{code}


pr1 : {A B : Type}
  → A × B → A
pr1 (a , b) = a

pr2 : {A B : Type}
  → A × B → B
pr2 (a , b) = b

\end{code}


We want to show that the type of paths between pairs (a, b) and (c, d)
is isomorphic to the type of pairs of paths from a to c and from b to d.
We first define maps in both directions:

\begin{code}
dirprod-eq-pr1 : {A B : Type}
  → (s t : A × B)
  → s ⟿ t → pr1 s ⟿ pr1 t
dirprod-eq-pr1 s t p = function-on-paths pr1 p

dirprod-eq-pr2 : {A B : Type}
  → (s t : A × B)
  → s ⟿ t → pr2 s ⟿ pr2 t
dirprod-eq-pr2 s t p = function-on-paths pr2 p

dirprod-eq : {A B : Type}
  → {a a' : A}
  → {b b' : B}
  → (a ⟿ a') × (b ⟿ b')
  → (a , b) ⟿ (a' , b')
dirprod-eq ((Id-Path a) , (Id-Path b)) = Id-Path (a , b)

\end{code}