===================================== 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}