Split formalizations from seminar into proper files

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

@@ -6,25 +6,40 @@ 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.
 
 !!! 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)
+#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)
+```

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

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

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