Merge pull request #15 from rzk-lang/3.1-sets-and-n-types

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

src/1-foundations/2-homotopy-type-theory/08-the-unit-type.rzk.md

@@ -5,3 +5,30 @@ This is a literate Rzk file:
 ```rzk
 #lang rzk-1
 ```
+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
+    -- provide a function - a constant map to unit
+  := (\ (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' → refl_{unit} = p')
+                ( \ x' → refl)
+                x y p
+            )
+        ))
+```
+

src/1-foundations/3-sets-and-logic/01-sets-and-n-types.rzk.md

@@ -0,0 +1,83 @@
+# 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 is-set
+    ( 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 is-set-Unit
+  : is-set 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)
+            refl)
+        -- 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)
+```