3.1 sets and n-types

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

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
+            )
+        ))
+```
+

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)
+```