Add is-set-prod (2.6.2 and 3.1.5)

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