From 5d73a285864f45a580f1ec753c66a8d2b43f04ee Mon Sep 17 00:00:00 2001 From: eyihluyc Date: Mon, 27 Nov 2023 15:11:48 +0300 Subject: [PATCH 1/3] Add 2.8 and 3.1.2 --- mkdocs.yml | 2 + .../08-the-unit-type.rzk.md | 38 +++++++++++++++ .../01-sets-and-n-types.rzk.md | 47 +++++++++++++++++++ 3 files changed, 87 insertions(+) create mode 100644 src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md diff --git a/mkdocs.yml b/mkdocs.yml index a9d1f4f..511e29a 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -35,6 +35,8 @@ nav: - "2.14 Example: equality of structures": 1-foundations/2-homotopy-type-theory/14-example-equality-of-structures.rzk.md - 2.15 Universal properties: 1-foundations/2-homotopy-type-theory/15-universal-properties.rzk.md - Exercises: 1-foundations/2-homotopy-type-theory/exercises/README.md + - 3 Sets and Logic: + - 3.1 Sets and n-types: 1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md markdown_extensions: - admonition diff --git a/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md b/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md index 165c595..249261c 100644 --- a/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md +++ b/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md @@ -5,3 +5,41 @@ This is a literate Rzk file: ```rzk #lang rzk-1 ``` + +!!! note "Lemma. Any two elements of $\mathbb{1}$ are equal" + For any $x,y:\mathbb{1}$, we have $x = y$. + +```rzk +#def units-eq + (x y : Unit) + : x = y + := path-concat Unit x unit y (Unit-uniq x) (path-sym Unit y unit (Unit-uniq y)) +``` + +!!! note "Theorem 2.8.1." + For any $x,y:\mathbb{1}$, we have $(x=y) \simeq \mathbb{1}$. + +```rzk +#def paths-in-unit-equiv-unit + (x y : Unit) + : equivalence (x = y) Unit + -- provide a function - a constant map to unit + := ( \ (p : x = y) → unit, ( + -- provide right inverse - a constant map to an inhabitant of x = y + (\ (u : Unit) → units-eq x y, + -- prove that composition is homotopical to id_Unit, via the proof that any inhabitant of unit is equal to unit + \ (u : Unit) → path-sym Unit u unit (Unit-uniq u)), + -- provide left same inverse (choose same as right inverse) + (\ (u : Unit) → units-eq x y, + -- prove that composition is homotopical to id_{x = y}, in other words, that + -- concatenation of paths (x = unit) and (unit = y) is equal to p; use path induction on p to show that + -- concatenation of paths (x = unit) and (unit = x) is equal to refl, with the "concat with inverse is refl" theorem + \ (p : x = y) → path-ind + Unit + ( \ x' y' p' → units-eq x' y' = p') + ( \ x' → inverse-r Unit x' unit (Unit-uniq x')) + x y p + ) + )) +``` + diff --git a/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md b/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md new file mode 100644 index 0000000..c3d2d3a --- /dev/null +++ b/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md @@ -0,0 +1,47 @@ +# 3.1 Sets and $n$-types + +This is a literate Rzk file: + +```rzk +#lang rzk-1 +``` + +In general, types behave like spaces or higher groupoids, but there is a subclass of types that behave more like sets in a traditional sense. +We expect a type to be a set, if there is no higher homotopical information. + +!!! note "Definition 3.1.1." + A type $A$ is a **set** if for all $x, y : A$ and all $p, q : x = y$, we have $p = q$. + +```rzk +#def isSet + (A : U) + : U + := (x : A) → (y : A) → (p : x = y) → (q : x = y) → (p = q) +``` + +!!! note "Example 3.1.2." + The type $\mathbb{1}$ is a set. + +```rzk +#def unit-isSet + : isSet Unit + := \ x y p q → 3-path-concat + (x = y) + -- p = f_inv (f(p)) = f_inv (f(q)) = q + p + ((first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) p)) + ((first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) q)) + q + -- p = f_inv (f(p)) : use the proof embedded in the equivalence + (path-sym (x = y) (((first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) p))) p + ((second (second (second (paths-in-unit-equiv-unit x y)))) p)) + -- f_inv (f(p)) = f_inv (f(q)) : use the fact that f(p) and f(q) are of type Unit and therefore there is equality between them + (ap + Unit (x = y) + (first (second (second (paths-in-unit-equiv-unit x y)))) + ((first (paths-in-unit-equiv-unit x y)) p) + ((first (paths-in-unit-equiv-unit x y)) q) + (units-eq ((first (paths-in-unit-equiv-unit x y)) p) ((first (paths-in-unit-equiv-unit x y)) q))) + -- f_inv (f(q)) = q : use the proof embedded in the equivalence + ((second (second (second (paths-in-unit-equiv-unit x y)))) q) +``` From 80f3c7fab55fac06d6578b771c1cb41a4a450600 Mon Sep 17 00:00:00 2001 From: eyihluyc Date: Tue, 12 Dec 2023 18:27:55 -0500 Subject: [PATCH 2/3] Improve is-set-Unit --- .../08-the-unit-type.rzk.md | 39 +++++++------------ .../01-sets-and-n-types.rzk.md | 31 ++++++++------- 2 files changed, 30 insertions(+), 40 deletions(-) diff --git a/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md b/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md index 249261c..a4eb878 100644 --- a/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md +++ b/src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md @@ -5,39 +5,28 @@ This is a literate Rzk file: ```rzk #lang rzk-1 ``` - -!!! note "Lemma. Any two elements of $\mathbb{1}$ are equal" - For any $x,y:\mathbb{1}$, we have $x = y$. - -```rzk -#def units-eq - (x y : Unit) - : x = y - := path-concat Unit x unit y (Unit-uniq x) (path-sym Unit y unit (Unit-uniq y)) -``` +For `Unit` type, uniqueness principle is built-in. That is, for any `x, y : Unit`, we have `refl : x = y` !!! note "Theorem 2.8.1." For any $x,y:\mathbb{1}$, we have $(x=y) \simeq \mathbb{1}$. ```rzk #def paths-in-unit-equiv-unit - (x y : Unit) - : equivalence (x = y) Unit + ( x y : Unit) + : equivalence (x = y) Unit -- provide a function - a constant map to unit - := ( \ (p : x = y) → unit, ( - -- provide right inverse - a constant map to an inhabitant of x = y - (\ (u : Unit) → units-eq x y, - -- prove that composition is homotopical to id_Unit, via the proof that any inhabitant of unit is equal to unit - \ (u : Unit) → path-sym Unit u unit (Unit-uniq u)), - -- provide left same inverse (choose same as right inverse) - (\ (u : Unit) → units-eq x y, - -- prove that composition is homotopical to id_{x = y}, in other words, that - -- concatenation of paths (x = unit) and (unit = y) is equal to p; use path induction on p to show that - -- concatenation of paths (x = unit) and (unit = x) is equal to refl, with the "concat with inverse is refl" theorem - \ (p : x = y) → path-ind + := (\ (p : x = y) → unit , ( + -- provide right inverse - a constant map to refl_{unit} + ( \ (u : Unit) → refl_{unit} + , -- prove that composition is homotopical to id_Unit + \ (u : Unit) → refl) + , -- provide left inverse - a constant map to refl_{unit} + ( \ (u : Unit) → refl_{unit} + , -- prove that composition is homotopical to id_{x = y}; use path induction on p + \ (p : x = y) → path-ind Unit - ( \ x' y' p' → units-eq x' y' = p') - ( \ x' → inverse-r Unit x' unit (Unit-uniq x')) + ( \ x' y' p' → refl_{unit} = p') + ( \ x' → refl) x y p ) )) diff --git a/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md b/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md index c3d2d3a..fa611f9 100644 --- a/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md +++ b/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md @@ -13,8 +13,8 @@ We expect a type to be a set, if there is no higher homotopical information. A type $A$ is a **set** if for all $x, y : A$ and all $p, q : x = y$, we have $p = q$. ```rzk -#def isSet - (A : U) +#def is-set + ( A : U) : U := (x : A) → (y : A) → (p : x = y) → (q : x = y) → (p = q) ``` @@ -23,25 +23,26 @@ We expect a type to be a set, if there is no higher homotopical information. The type $\mathbb{1}$ is a set. ```rzk -#def unit-isSet - : isSet Unit +#def is-set-Unit + : is-set Unit := \ x y p q → 3-path-concat - (x = y) + ( x = y) -- p = f_inv (f(p)) = f_inv (f(q)) = q p - ((first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) p)) - ((first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) q)) + ( ( first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) p)) + ( ( first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) q)) q -- p = f_inv (f(p)) : use the proof embedded in the equivalence - (path-sym (x = y) (((first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) p))) p - ((second (second (second (paths-in-unit-equiv-unit x y)))) p)) + ( path-sym (x = y) (((first (second (second (paths-in-unit-equiv-unit x y)))) ((first (paths-in-unit-equiv-unit x y)) p))) p + ( ( second (second (second (paths-in-unit-equiv-unit x y)))) p)) -- f_inv (f(p)) = f_inv (f(q)) : use the fact that f(p) and f(q) are of type Unit and therefore there is equality between them - (ap + ( ap Unit (x = y) - (first (second (second (paths-in-unit-equiv-unit x y)))) - ((first (paths-in-unit-equiv-unit x y)) p) - ((first (paths-in-unit-equiv-unit x y)) q) - (units-eq ((first (paths-in-unit-equiv-unit x y)) p) ((first (paths-in-unit-equiv-unit x y)) q))) + ( first (second (second (paths-in-unit-equiv-unit x y)))) + ( ( first (paths-in-unit-equiv-unit x y)) p) + ( ( first (paths-in-unit-equiv-unit x y)) q) + refl) -- f_inv (f(q)) = q : use the proof embedded in the equivalence - ((second (second (second (paths-in-unit-equiv-unit x y)))) q) + ( ( second (second (second (paths-in-unit-equiv-unit x y)))) q) +``` ``` From 49038fd626c6b7d138d75aba37112f57a5f9e5ba Mon Sep 17 00:00:00 2001 From: eyihluyc Date: Tue, 12 Dec 2023 18:29:39 -0500 Subject: [PATCH 3/3] Add is-set-prod (2.6.2 and 3.1.5) --- .../06-cartesian-product-types.rzk.md | 58 +++++++++++++++++++ .../01-sets-and-n-types.rzk.md | 41 ++++++++++++- 2 files changed, 96 insertions(+), 3 deletions(-) diff --git a/src/1-foundations/2-homotopy-type-theory/06-cartesian-product-types.rzk.md b/src/1-foundations/2-homotopy-type-theory/06-cartesian-product-types.rzk.md index 8480afa..f19d84e 100644 --- a/src/1-foundations/2-homotopy-type-theory/06-cartesian-product-types.rzk.md +++ b/src/1-foundations/2-homotopy-type-theory/06-cartesian-product-types.rzk.md @@ -5,3 +5,61 @@ This is a literate Rzk file: ```rzk #lang rzk-1 ``` + +For any elements $x, y : A \times B$ and a path $p : x =_{A \times B} y$, by functoriality we can extract paths $\mathsf{pr}_1(p) : \mathsf{pr}_1(x) =_A \mathsf{pr}_1(y)$ and $\mathsf{pr}_2(p) : \mathsf{pr}_2(x) =_B \mathsf{pr}_2(y)$. + +```rzk +#def path-in-prod-to-prod-of-paths + ( A B : U) + ( x y : prod A B) + : ( x = y) → prod (pr₁ A B x = pr₁ A B y) (pr₂ A B x = pr₂ A B y) + := \ p → (ap (prod A B) A (pr₁ A B) x y p , ap (prod A B) B (pr₂ A B) x y p) +``` + + +!!! note "Theorem 2.6.2. Paths in a product space are pairs of paths" + The function + + $$(x =_{A \times B} y) → (\mathsf{pr}_1(x) =_A \mathsf{pr}_1(y)) \times (\mathsf{pr}_2(x) =_B \mathsf{pr}_2(y)).$$ + + is an equivalence + +```rzk +#def prod-of-paths-to-path-in-prod + ( A B : U) + ( a₁ a₂ : A) + ( b₁ b₂ : B) + : ( prod (a₁ = a₂) (b₁ = b₂)) → (a₁ , b₁) = (a₂ , b₂) + := \ (pa , pb) → path-ind A + ( \ x y p → (x , b₁) = (y , b₂)) + ( \ x → path-ind B + ( \ x' y' p' → (x , x') = (x , y')) + ( \ x' → refl) + b₁ b₂ pb + ) + a₁ a₂ pa +``` + + +```rzk +#def prod-path-qinv + ( A B : U) + ( a₁ a₂ : A) + ( b₁ b₂ : B) + : qinv ((a₁ , b₁) = (a₂ , b₂)) (prod (a₁ = a₂) (b₁ = b₂)) (path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂)) + := (prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂ + , ( \ (pa , pb) → path-ind A + ( \ x y p → (path-in-prod-to-prod-of-paths A B (x , b₁) (y , b₂)) (prod-of-paths-to-path-in-prod A B x y b₁ b₂ (p , pb)) = (p , pb)) + ( \ x → path-ind B + ( \ x' y' p' → ((path-in-prod-to-prod-of-paths A B (x , x') (x , y')) (prod-of-paths-to-path-in-prod A B x x x' y' (refl , p')) = (refl , p'))) + ( \ x' → refl) + b₁ b₂ pb + ) + a₁ a₂ pa + , \ pab → path-ind (prod A B) + ( \ (a₁' , b₁') (a₂' , b₂') pab' → prod-of-paths-to-path-in-prod A B a₁' a₂' b₁' b₂' (path-in-prod-to-prod-of-paths A B (a₁' , b₁') (a₂' , b₂') pab') = pab') + ( \ x → refl) + ( a₁ , b₁) (a₂ , b₂) pab + ) + ) +``` diff --git a/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md b/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md index fa611f9..d2adb96 100644 --- a/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md +++ b/src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md @@ -15,8 +15,8 @@ We expect a type to be a set, if there is no higher homotopical information. ```rzk #def is-set ( A : U) - : U - := (x : A) → (y : A) → (p : x = y) → (q : x = y) → (p = q) + : U + := (x : A) → (y : A) → (p : x = y) → (q : x = y) → (p = q) ``` !!! note "Example 3.1.2." @@ -25,7 +25,7 @@ We expect a type to be a set, if there is no higher homotopical information. ```rzk #def is-set-Unit : is-set Unit - := \ x y p q → 3-path-concat + := \ x y p q → 3-path-concat ( x = y) -- p = f_inv (f(p)) = f_inv (f(q)) = q p @@ -45,4 +45,39 @@ We expect a type to be a set, if there is no higher homotopical information. -- f_inv (f(q)) = q : use the proof embedded in the equivalence ( ( second (second (second (paths-in-unit-equiv-unit x y)))) q) ``` + +!!! note "Example 3.1.5." + If $A$ and $B$ are sets, then so is $A \times B$. + +```rzk +#def is-set-prod + ( A B : U) + ( is-set-A : is-set A) + ( is-set-B : is-set B) + : is-set (prod A B) + := \ (a₁ , b₁) (a₂ , b₂) p q → 3-path-concat + ( ( a₁ , b₁) = (a₂ , b₂)) + p + ( prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂ (path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂) p)) + ( prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂ (path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂) q)) + q + ( path-sym ((a₁ , b₁) = (a₂ , b₂)) + ( prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂ (path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂) p)) + p + ( second (second (prod-path-qinv A B a₁ a₂ b₁ b₂)) p)) + ( ap (prod (a₁ = a₂) (b₁ = b₂)) ((a₁ , b₁) = (a₂ , b₂)) + ( \ x → (prod-of-paths-to-path-in-prod A B a₁ a₂ b₁ b₂ x)) + ( path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂) p) + ( path-in-prod-to-prod-of-paths A B (a₁ , b₁) (a₂ , b₂) q) + -- proof that (pa, pb) = (qa, qb) + ( prod-of-paths-to-path-in-prod (a₁ = a₂) (b₁ = b₂) + ( ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) p) + ( ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) q) + ( ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) p) + ( ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) q) + ( ( is-set-A a₁ a₂ (ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) p) (ap (prod A B) A (pr₁ A B) (a₁ , b₁) (a₂ , b₂) q) + , is-set-B b₁ b₂ (ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) p) (ap (prod A B) B (pr₂ A B) (a₁ , b₁) (a₂ , b₂) q))) + ) + ) + ( second (second (prod-path-qinv A B a₁ a₂ b₁ b₂)) q) ```