Improve is-set-Unit

rzk-lang · Dec 13, 2023 · eb5b149 · eb5b149
1 parent ccc209e
commit eb5b149
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 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
@@ -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
@@ -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)
+```
 ```