From 801a8b9b95317b6dc57ff23e8eaff631b3cbaa31 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Thu, 14 Dec 2023 01:32:36 +0300
Subject: [PATCH] Split formalizations from seminar into proper files

---
 .../01-sets-and-n-types.rzk.md                | 140 +++++++++++--
 .../02-propositions-as-types.rzk copy.md      |   7 +
 .../03-mere-propositions.rzk.md               |  41 ++++
 .../11-contractibility.rzk.md                 |  33 +++
 .../iu-hott-seminar-2023-12-06.rzk.md         | 196 ------------------
 5 files changed, 208 insertions(+), 209 deletions(-)
 create mode 100644 src/1-foundations/3-sets-and-logic/02-propositions-as-types.rzk copy.md
 create mode 100644 src/1-foundations/3-sets-and-logic/03-mere-propositions.rzk.md
 create mode 100644 src/1-foundations/3-sets-and-logic/11-contractibility.rzk.md
 delete mode 100644 src/1-foundations/iu-hott-seminar-2023-12-06.rzk.md

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 d2adb96..327bc4c 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
@@ -6,6 +6,12 @@ This is a literate Rzk file:
 #lang rzk-1
 ```
 
+This module assumes function extensionality:
+
+```rzk
+#assume funext : FunExt
+```
+
 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.
 
@@ -13,18 +19,27 @@ 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 is-set
-    ( A : U)
+#def isSet
+  ( A : U)
   : U
-  := (x : A) → (y : A) → (p : x = y) → (q : x = y) → (p = q)
+  :=
+    ( x : A)
+  → ( y : A)
+  → ( p : x = y)
+  → ( q : x = y)
+  → ( p = q)
 ```
 
-!!! note "Example 3.1.2."
+## Some examples
+
+### Unit type is a set
+
+!!! example "Example 3.1.2."
     The type $\mathbb{1}$ is a set.
 
 ```rzk
-#def is-set-Unit
-  : is-set Unit
+#def isSet-Unit
+  : isSet Unit
   := \ x y p q → 3-path-concat
         ( x = y)
         -- p = f_inv (f(p)) = f_inv (f(q)) = q
@@ -46,15 +61,17 @@ We expect a type to be a set, if there is no higher homotopical information.
         ( ( second (second (second (paths-in-unit-equiv-unit x y)))) q)
 ```
 
-!!! note "Example 3.1.5."
+### Products of sets are sets
+
+!!! example "Example 3.1.5."
     If $A$ and $B$ are sets, then so is $A \times B$.
 
 ```rzk
-#def is-set-prod
+#def isSet-prod
   ( A B : U)
-  ( is-set-A : is-set A)
-  ( is-set-B : is-set B)
-  : is-set (prod A B)
+  ( isSet-A : isSet A)
+  ( isSet-B : isSet B)
+  : isSet (prod A B)
   := \ (a₁ , b₁) (a₂ , b₂) p q → 3-path-concat
     ( ( a₁ , b₁) = (a₂ , b₂))
     p
@@ -75,9 +92,106 @@ We expect a type to be a set, if there is no higher homotopical information.
         ( 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)))
+        ( ( isSet-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)
+      , isSet-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)
 ```
+
+### Function types into sets form sets
+
+!!! example "Example 3.1.6"
+
+    If $A$ is _any_ type and $B : A \to \mathcal{U}$ is such that each $B(x)$ is a set, then the type $\prod_{(x:A)} B(x)$ is a set.
+
+```rzk
+#define weak-isSet-function
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p q : homotopy A (\ _ → B) f g)
+  : homotopy A (\ x → f x = g x) p q
+  := \ x → isSet-B (f x) (g x) (p x) (q x)
+
+#define weak-isSet-function₁
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p q : f = g)
+  : homotopy A (\ x → f x = g x)
+    ( happly A (\ _ → B) f g p)
+    ( happly A (\ _ → B) f g q)
+  :=
+  weak-isSet-function A B isSet-B f g
+  ( happly A (\ _ → B) f g p)
+  ( happly A (\ _ → B) f g q)
+
+#define weak-isSet-function₂ uses (funext)
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p q : f = g)
+  : happly A (\ _ → B) f g p
+  = happly A (\ _ → B) f g q
+  :=
+  map-funext funext A (\ x → f x = g x)
+  ( happly A (\ _ → B) f g p)
+  ( happly A (\ _ → B) f g q)
+  ( weak-isSet-function₁ A B isSet-B f g p q)
+
+#define weak-isSet-function₃ uses (funext)
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p q : f = g)
+  : map-funext funext A (\ _ → B) f g (happly A (\ _ → B) f g p)
+  = map-funext funext A (\ _ → B) f g (happly A (\ _ → B) f g q)
+  :=
+  ap
+  ( homotopy A (\ _ → B) f g)
+  ( f = g)
+  ( map-funext funext A (\ _ → B) f g)
+  ( happly A (\ _ → B) f g p)
+  ( happly A (\ _ → B) f g q)
+  ( weak-isSet-function₂ A B isSet-B f g p q)
+
+#define funext-happly-eq-id uses (funext)
+  ( A B : U)
+  ( isSet-B : isSet B)
+  ( f g : A → B)
+  ( p : f = g)
+  : map-funext funext A (\ _ → B) f g (happly A (\ _ → B) f g p)
+  = p
+  := second (second (funext A (\ _ → B) f g)) p
+
+#define path-concat3
+  ( A : U)
+  ( x y z w : A)
+  : ( x = y) → (y = z) → (z = w) → (x = w)
+  :=
+  \ p q r →
+    path-concat A x z w
+      ( path-concat A x y z p q)
+      r
+
+#define isSet-function uses (funext)
+  ( A B : U)
+  ( isSet-B : isSet B)
+  : isSet (A → B)
+  :=
+  \ f g p q →
+    path-concat3 (f = g)
+
+      p
+      ( map-funext funext A (\ _ → B) f g (happly A (\ _ → B) f g p))
+      ( map-funext funext A (\ _ → B) f g (happly A (\ _ → B) f g q))
+      q
+
+      ( path-sym (f = g)
+        ( map-funext funext A (\ _ → B) f g (happly A (\ _ → B) f g p))
+        p
+        ( funext-happly-eq-id A B isSet-B f g p))
+      ( weak-isSet-function₃ A B isSet-B f g p q)
+      ( funext-happly-eq-id A B isSet-B f g q)
+```
diff --git a/src/1-foundations/3-sets-and-logic/02-propositions-as-types.rzk copy.md b/src/1-foundations/3-sets-and-logic/02-propositions-as-types.rzk copy.md
new file mode 100644
index 0000000..4c053dd
--- /dev/null
+++ b/src/1-foundations/3-sets-and-logic/02-propositions-as-types.rzk copy.md	
@@ -0,0 +1,7 @@
+# Propositions as types?
+
+This is a literate Rzk file:
+
+```rzk
+#lang rzk-1
+```
diff --git a/src/1-foundations/3-sets-and-logic/03-mere-propositions.rzk.md b/src/1-foundations/3-sets-and-logic/03-mere-propositions.rzk.md
new file mode 100644
index 0000000..cdb07d7
--- /dev/null
+++ b/src/1-foundations/3-sets-and-logic/03-mere-propositions.rzk.md
@@ -0,0 +1,41 @@
+# Mere propositions
+
+This is a literate Rzk file:
+
+```rzk
+#lang rzk-1
+```
+
+This module assumes function extensionality:
+
+```rzk
+#assume funext : FunExt
+```
+
+!!! note "Definition 3.3.1"
+
+    A type $P$ is a __mere proposition__ if for all $x, y : P$ we have $x = y$.
+
+```rzk
+#define isProp
+  ( A : U)
+  : U
+  := (x : A) → (y : A) → x = y
+```
+
+## Examples
+
+```rzk
+#define isProp-Unit
+  : isProp Unit
+  := \ unit unit → refl
+```
+
+```rzk
+#define isProp-function uses (funext)
+  ( A : U)
+  ( B : A → U)
+  ( isProp-B : (a : A) → isProp (B a))
+  : isProp ((a : A) → B a)
+  := \ f g → map-funext funext A B f g (\ a → isProp-B a (f a) (g a))
+```
diff --git a/src/1-foundations/3-sets-and-logic/11-contractibility.rzk.md b/src/1-foundations/3-sets-and-logic/11-contractibility.rzk.md
new file mode 100644
index 0000000..ff794e0
--- /dev/null
+++ b/src/1-foundations/3-sets-and-logic/11-contractibility.rzk.md
@@ -0,0 +1,33 @@
+# Contractibility
+
+This is a literate Rzk file:
+
+```rzk
+#lang rzk-1
+```
+
+!!! note "Definition 3.11.1"
+
+    A type $A$ is __contractible__, or a __singleton__,
+    if there is $a : A$, called the __center of contraction__,
+    such that $a = x$ for all $x : A$.
+    We denote the specified path $a = x$ by $\mathsf{contr}_{x}$.
+
+```rzk
+#define isContr
+  ( A : U)
+  : U
+  := Σ (a : A) , (x : A) → a = x
+
+#define center
+  ( A : U)
+  : isContr A → A
+  := \ (a , _) → a
+
+#define contr
+  ( A : U)
+  ( isContr-A : isContr A)
+  ( x : A)
+  : center A isContr-A = x
+  := second isContr-A x
+```
diff --git a/src/1-foundations/iu-hott-seminar-2023-12-06.rzk.md b/src/1-foundations/iu-hott-seminar-2023-12-06.rzk.md
deleted file mode 100644
index d78b03e..0000000
--- a/src/1-foundations/iu-hott-seminar-2023-12-06.rzk.md
+++ /dev/null
@@ -1,196 +0,0 @@
-# IU HoTT Seminar 2023-12-06
-
-```rzk
-#lang rzk-1
-```
-
-# Sets and logic in HoTT
-
-
-```rzk title="HoTT Book, Definition 2.4.10"
-#define is-equiv
-  ( A B : U)
-  ( f : A → B)
-  : U
-  :=
-  prod
-    ( Σ ( g : B → A) , (y : B) → f (g y) = y)
-    ( Σ ( g : B → A) , (x : A) → g (f x) = x)
-```
-
-```rzk title="HoTT Book, Definition 2.9.2"
-#define happly
-  ( A : U)
-  ( B : A → U)
-  ( f g : (a : A) → B a)
-  : ( f = g) → homotopy A B f g
-  :=
-  path-ind ((a : A) → B a)
-  ( \ f' g' _ → homotopy A B f' g')
-  ( \ f' _ → refl)
-  f g
-```
-
-
-```rzk title="HoTT Book, Axiom 2.9.3"
-#define FunExt
-  : U
-  :=
-    ( A : U)
-  → ( B : A → U)
-  → ( f : (a : A) → B a)
-  → ( g : (a : A) → B a)
-  → is-equiv
-    ( f = g)
-    ( homotopy A B f g)
-    ( happly A B f g)
-```
-
-```rzk
-#assume funext' : FunExt
-```
-
-```rzk
-#define funext uses (funext')
-  ( A : U)
-  ( B : A → U)
-  ( f g : (a : A) → B a)
-  : homotopy A B f g → f = g
-  := first (second (funext' A B f g))
-```
-
-```rzk
-#define weak-is-set-function
-  ( A B : U)
-  ( is-set-B : is-set B)
-  ( f g : A → B)
-  ( p q : homotopy A (\ _ → B) f g)
-  : homotopy A (\ x → f x = g x) p q
-  := \ x → is-set-B (f x) (g x) (p x) (q x)
-
-#define weak-is-set-function₁
-  ( A B : U)
-  ( is-set-B : is-set B)
-  ( f g : A → B)
-  ( p q : f = g)
-  : homotopy A (\ x → f x = g x)
-    ( happly A (\ _ → B) f g p)
-    ( happly A (\ _ → B) f g q)
-  :=
-  weak-is-set-function A B is-set-B f g
-  ( happly A (\ _ → B) f g p)
-  ( happly A (\ _ → B) f g q)
-
-#define weak-is-set-function₂ uses (funext')
-  ( A B : U)
-  ( is-set-B : is-set B)
-  ( f g : A → B)
-  ( p q : f = g)
-  : happly A (\ _ → B) f g p
-  = happly A (\ _ → B) f g q
-  :=
-  funext A (\ x → f x = g x)
-  ( happly A (\ _ → B) f g p)
-  ( happly A (\ _ → B) f g q)
-  ( weak-is-set-function₁ A B is-set-B f g p q)
-
-#define weak-is-set-function₃ uses (funext')
-  ( A B : U)
-  ( is-set-B : is-set B)
-  ( f g : A → B)
-  ( p q : f = g)
-  : funext A (\ _ → B) f g (happly A (\ _ → B) f g p)
-  = funext A (\ _ → B) f g (happly A (\ _ → B) f g q)
-  :=
-  ap
-  ( homotopy A (\ _ → B) f g)
-  ( f = g)
-  ( funext A (\ _ → B) f g)
-  ( happly A (\ _ → B) f g p)
-  ( happly A (\ _ → B) f g q)
-  ( weak-is-set-function₂ A B is-set-B f g p q)
-
-#define funext-happly-eq-id uses (funext')
-  ( A B : U)
-  ( is-set-B : is-set B)
-  ( f g : A → B)
-  ( p : f = g)
-  : funext A (\ _ → B) f g (happly A (\ _ → B) f g p)
-  = p
-  := second (second (funext' A (\ _ → B) f g)) p
-
-#define path-concat3
-  ( A : U)
-  ( x y z w : A)
-  : ( x = y) → (y = z) → (z = w) → (x = w)
-  :=
-  \ p q r →
-    path-concat A x z w
-      ( path-concat A x y z p q)
-      r
-
-#define is-set-function uses (funext')
-  ( A B : U)
-  ( is-set-B : is-set B)
-  : is-set (A → B)
-  :=
-  \ f g p q →
-    path-concat3 (f = g)
-
-      p
-      ( funext A (\ _ → B) f g (happly A (\ _ → B) f g p))
-      ( funext A (\ _ → B) f g (happly A (\ _ → B) f g q))
-      q
-
-      ( path-sym (f = g)
-        ( funext A (\ _ → B) f g (happly A (\ _ → B) f g p))
-        p
-        ( funext-happly-eq-id A B is-set-B f g p))
-      ( weak-is-set-function₃ A B is-set-B f g p q)
-      ( funext-happly-eq-id A B is-set-B f g q)
-```
-
-## Logic
-
-```rzk
-#define is-prop
-  ( A : U)
-  : U
-  := (x : A) → (y : A) → x = y
-```
-
-```rzk
-#define is-contr
-  ( A : U)
-  : U
-  := Σ (a : A) , (x : A) → a = x
-```
-
-```rzk
-#define is-prop-Unit
-  : is-prop Unit
-  := \ unit unit → refl
-
-#define is-prop-function uses (funext')
-  ( A : U)
-  ( B : A → U)
-  ( is-prop-B : (a : A) → is-prop (B a))
-  : is-prop ((a : A) → B a)
-  := \ f g → funext A B f g (\ a → is-prop-B a (f a) (g a))
-
--- #define is-set-if-is-prop
---   (A : U)
---   (is-prop-A : is-prop A)
---   : is-set A
---   :=
---   \ x y p q →
---     path-ind (x = y)
---     (\ x' y' p' → x=x' p' y'=y = q)
---     (\ x' → refl)
---     x y p
-
--- #define is-prop-is-prop
---   (A : U)
---   : is-prop ((a : A) → (b : A) → a = b)
---   :=
-```