Closure properties of π-finite types

src/elementary-number-theory/maximum-natural-numbers.lagda.md

@@ -39,11 +39,11 @@ max-ℕ 0 n = n
 max-ℕ (succ-ℕ m) 0 = succ-ℕ m
 max-ℕ (succ-ℕ m) (succ-ℕ n) = succ-ℕ (max-ℕ m n)
 
-ap-max-ℕ : {x x' y y' : ℕ} → x ＝ x' → y ＝ y' → max-ℕ x y ＝ max-ℕ x' y'
-ap-max-ℕ p q = ap-binary max-ℕ p q
-
 max-ℕ' : ℕ → (ℕ → ℕ)
 max-ℕ' x y = max-ℕ y x
+
+ap-max-ℕ : {x x' y y' : ℕ} → x ＝ x' → y ＝ y' → max-ℕ x y ＝ max-ℕ x' y'
+ap-max-ℕ p q = ap-binary max-ℕ p q
 ```
 
 ### Maximum of elements of standard finite types

src/finite-group-theory/finite-groups.lagda.md

@@ -51,8 +51,8 @@ open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.finitely-many-connected-components
 open import univalent-combinatorics.function-types
-open import univalent-combinatorics.pi-finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.truncated-pi-finite-types
 open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
@@ -424,10 +424,10 @@ is-untruncated-π-finite-Group-of-Order {l} k n =
         is-untruncated-π-finite-is-finite k
           ( is-finite-is-group-Semigroup n X)))
 
-is-π-finite-Group-of-Order :
-  {l : Level} (n : ℕ) → is-π-finite 1 (Group-of-Order l n)
-is-π-finite-Group-of-Order n =
-  is-π-finite-is-untruncated-π-finite 1
+is-truncated-π-finite-Group-of-Order :
+  {l : Level} (n : ℕ) → is-truncated-π-finite 1 (Group-of-Order l n)
+is-truncated-π-finite-Group-of-Order n =
+  is-truncated-π-finite-is-untruncated-π-finite 1
     ( is-1-type-Group-of-Order n)
     ( is-untruncated-π-finite-Group-of-Order 1 n)
 ```

src/finite-group-theory/finite-monoids.lagda.md

@@ -38,8 +38,8 @@ open import univalent-combinatorics.dependent-pair-types
 open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.finitely-many-connected-components
-open import univalent-combinatorics.pi-finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.truncated-pi-finite-types
 open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
@@ -217,10 +217,10 @@ is-untruncated-π-finite-Monoid-of-Order {l} k n =
         is-untruncated-π-finite-is-finite k
           ( is-finite-is-unital-Semigroup n X)))
 
-is-π-finite-Monoid-of-Order :
-  {l : Level} (n : ℕ) → is-π-finite 1 (Monoid-of-Order l n)
-is-π-finite-Monoid-of-Order n =
-  is-π-finite-is-untruncated-π-finite 1
+is-truncated-π-finite-Monoid-of-Order :
+  {l : Level} (n : ℕ) → is-truncated-π-finite 1 (Monoid-of-Order l n)
+is-truncated-π-finite-Monoid-of-Order n =
+  is-truncated-π-finite-is-untruncated-π-finite 1
     ( is-1-type-Monoid-of-Order n)
     ( is-untruncated-π-finite-Monoid-of-Order 1 n)
 ```

src/finite-group-theory/finite-semigroups.lagda.md

@@ -32,8 +32,8 @@ open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.finitely-many-connected-components
 open import univalent-combinatorics.function-types
-open import univalent-combinatorics.pi-finite-types
 open import univalent-combinatorics.standard-finite-types
+open import univalent-combinatorics.truncated-pi-finite-types
 open import univalent-combinatorics.untruncated-pi-finite-types
 ```
 
@@ -205,10 +205,10 @@ is-untruncated-π-finite-Semigroup-of-Order k n =
     ( compute-Semigroup-of-Order n)
     ( is-untruncated-π-finite-Semigroup-of-Order' k n)
 
-is-π-finite-Semigroup-of-Order :
-  {l : Level} (n : ℕ) → is-π-finite 1 (Semigroup-of-Order l n)
-is-π-finite-Semigroup-of-Order {l} n =
-  is-π-finite-is-untruncated-π-finite 1
+is-truncated-π-finite-Semigroup-of-Order :
+  {l : Level} (n : ℕ) → is-truncated-π-finite 1 (Semigroup-of-Order l n)
+is-truncated-π-finite-Semigroup-of-Order {l} n =
+  is-truncated-π-finite-is-untruncated-π-finite 1
     ( is-1-type-Semigroup-of-Order n)
     ( is-untruncated-π-finite-Semigroup-of-Order 1 n)
 ```

src/foundation.lagda.md

@@ -24,6 +24,7 @@ open import foundation.action-on-identifications-binary-dependent-functions publ
 open import foundation.action-on-identifications-binary-functions public
 open import foundation.action-on-identifications-dependent-functions public
 open import foundation.action-on-identifications-functions public
+open import foundation.addition-truncation-levels public
 open import foundation.apartness-relations public
 open import foundation.arithmetic-law-coproduct-and-sigma-decompositions public
 open import foundation.arithmetic-law-product-and-pi-decompositions public
@@ -161,6 +162,7 @@ open import foundation.equality-coproduct-types public
 open import foundation.equality-dependent-function-types public
 open import foundation.equality-dependent-pair-types public
 open import foundation.equality-fibers-of-maps public
+open import foundation.equality-truncation-levels public
 open import foundation.equivalence-classes public
 open import foundation.equivalence-extensionality public
 open import foundation.equivalence-induction public
@@ -239,6 +241,7 @@ open import foundation.implicit-function-types public
 open import foundation.impredicative-encodings public
 open import foundation.impredicative-universes public
 open import foundation.induction-principle-propositional-truncation public
+open import foundation.inequality-truncation-levels public
 open import foundation.infinitely-coherent-equivalences public
 open import foundation.inhabited-subtypes public
 open import foundation.inhabited-types public
@@ -276,13 +279,15 @@ open import foundation.locally-small-types public
 open import foundation.logical-equivalences public
 open import foundation.maps-in-global-subuniverses public
 open import foundation.maps-in-subuniverses public
+open import foundation.maximum-truncation-levels public
 open import foundation.maybe public
 open import foundation.mere-embeddings public
 open import foundation.mere-equality public
 open import foundation.mere-equivalences public
 open import foundation.mere-functions public
 open import foundation.mere-logical-equivalences public
 open import foundation.mere-path-cosplit-maps public
+open import foundation.merely-truncated-types public
 open import foundation.monomorphisms public
 open import foundation.morphisms-arrows public
 open import foundation.morphisms-binary-relations public

src/foundation/addition-truncation-levels.lagda.md

@@ -0,0 +1,195 @@
+# Addition of truncation levels
+
+```agda
+module foundation.addition-truncation-levels where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.negation
+open import foundation.truncation-levels
+```
+
+</details>
+
+## Idea
+
+We define the partial
+{{#concept "addition" Disambiguation="of truncation levels" Agda=add-𝕋 Agda=_+𝕋_}}
+binary operation on [truncation levels](foundation-core.truncation-levels.md).
+
+## Definitions
+
+### Addition of truncation levels
+
+```agda
+add-𝕋' : 𝕋 → 𝕋 → 𝕋
+add-𝕋' neg-two-𝕋 neg-two-𝕋 = neg-two-𝕋
+add-𝕋' neg-two-𝕋 (succ-𝕋 neg-two-𝕋) = neg-two-𝕋
+add-𝕋' neg-two-𝕋 (succ-𝕋 (succ-𝕋 l)) = l
+add-𝕋' (succ-𝕋 neg-two-𝕋) neg-two-𝕋 = neg-two-𝕋
+add-𝕋' (succ-𝕋 neg-two-𝕋) (succ-𝕋 l) = l
+add-𝕋' (succ-𝕋 (succ-𝕋 k)) neg-two-𝕋 = k
+add-𝕋' (succ-𝕋 (succ-𝕋 k)) (succ-𝕋 l) = succ-𝕋 (add-𝕋' (succ-𝕋 k) (succ-𝕋 l))
+
+add-𝕋 : 𝕋 → 𝕋 → 𝕋
+add-𝕋 k r = add-𝕋' r k
+```
+
+Agda is not happy with the following definition due to the `--exact-split` flag.
+
+```text
+add-𝕋 : 𝕋 → 𝕋 → 𝕋
+add-𝕋 neg-two-𝕋 neg-two-𝕋 = neg-two-𝕋
+add-𝕋 (succ-𝕋 neg-two-𝕋) neg-two-𝕋 = neg-two-𝕋
+add-𝕋 (succ-𝕋 (succ-𝕋 k)) neg-two-𝕋 = k
+add-𝕋 neg-two-𝕋 (succ-𝕋 neg-two-𝕋) = neg-two-𝕋
+add-𝕋 (succ-𝕋 k) (succ-𝕋 neg-two-𝕋) = k
+add-𝕋 neg-two-𝕋 (succ-𝕋 (succ-𝕋 r)) = r
+add-𝕋 (succ-𝕋 k) (succ-𝕋 (succ-𝕋 r)) = succ-𝕋 (add-𝕋 (succ-𝕋 k) (succ-𝕋 r))
+```
+
+```agda
+infixl 35 _+𝕋_
+_+𝕋_ = add-𝕋
+```
+
+### The double successor of addition on truncation levels
+
+```agda
+add+2-𝕋 : 𝕋 → 𝕋 → 𝕋
+add+2-𝕋 x neg-two-𝕋 = x
+add+2-𝕋 x (succ-𝕋 y) = succ-𝕋 (add+2-𝕋 x y)
+```
+
+```agda
+ap-add-𝕋 : {m n m' n' : 𝕋} → m ＝ m' → n ＝ n' → m +𝕋 n ＝ m' +𝕋 n'
+ap-add-𝕋 p q = ap-binary add-𝕋 p q
+```
+
+## Properties
+
+### Unit laws for addition of truncation levels
+
+```agda
+left-unit-law-add-𝕋 : (k : 𝕋) → zero-𝕋 +𝕋 k ＝ k
+left-unit-law-add-𝕋 neg-two-𝕋 = refl
+left-unit-law-add-𝕋 (succ-𝕋 neg-two-𝕋) = refl
+left-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 k)) =
+  ap succ-𝕋 (left-unit-law-add-𝕋 (succ-𝕋 k))
+
+right-unit-law-add-𝕋 : (k : 𝕋) → k +𝕋 zero-𝕋 ＝ k
+right-unit-law-add-𝕋 neg-two-𝕋 = refl
+right-unit-law-add-𝕋 (succ-𝕋 neg-two-𝕋) = refl
+right-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 neg-two-𝕋)) = refl
+right-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 (succ-𝕋 k))) = refl
+
+left-unit-law-add+2-𝕋 : (k : 𝕋) → add+2-𝕋 neg-two-𝕋 k ＝ k
+left-unit-law-add+2-𝕋 neg-two-𝕋 = refl
+left-unit-law-add+2-𝕋 (succ-𝕋 k) =
+  ap succ-𝕋 (left-unit-law-add+2-𝕋 k)
+
+right-unit-law-add+2-𝕋 : (k : 𝕋) → add+2-𝕋 k neg-two-𝕋 ＝ k
+right-unit-law-add+2-𝕋 neg-two-𝕋 = refl
+right-unit-law-add+2-𝕋 (succ-𝕋 k) = refl
+```
+
+### Successor laws for addition of truncation levels
+
+```agda
+right-successor-law-add-𝕋 :
+  (n k : 𝕋) → k +𝕋 iterated-succ-𝕋 3 n ＝ succ-𝕋 (k +𝕋 iterated-succ-𝕋 2 n)
+right-successor-law-add-𝕋 n neg-two-𝕋 = refl
+right-successor-law-add-𝕋 n (succ-𝕋 k) = refl
+
+left-successor-law-add-𝕋 :
+  (k n : 𝕋) → iterated-succ-𝕋 3 n +𝕋 k ＝ succ-𝕋 (iterated-succ-𝕋 2 n +𝕋 k)
+left-successor-law-add-𝕋 neg-two-𝕋 n = refl
+left-successor-law-add-𝕋 (succ-𝕋 neg-two-𝕋) n = refl
+left-successor-law-add-𝕋 (succ-𝕋 (succ-𝕋 k)) n =
+  ap succ-𝕋 (left-successor-law-add-𝕋 (succ-𝕋 k) n)
+```
+
+### The balancing law of the successor function over addition
+
+```agda
+balance-succ-add-𝕋 : (k r : 𝕋) → succ-𝕋 k +𝕋 r ＝ k +𝕋 succ-𝕋 r
+balance-succ-add-𝕋 neg-two-𝕋 neg-two-𝕋 = refl
+balance-succ-add-𝕋 neg-two-𝕋 (succ-𝕋 neg-two-𝕋) = refl
+balance-succ-add-𝕋 neg-two-𝕋 (succ-𝕋 (succ-𝕋 r)) =
+  ap succ-𝕋 (balance-succ-add-𝕋 neg-two-𝕋 (succ-𝕋 r))
+balance-succ-add-𝕋 (succ-𝕋 k) neg-two-𝕋 = refl
+balance-succ-add-𝕋 (succ-𝕋 k) (succ-𝕋 neg-two-𝕋) = refl
+balance-succ-add-𝕋 (succ-𝕋 k) (succ-𝕋 (succ-𝕋 r)) =
+  ap succ-𝕋 (balance-succ-add-𝕋 (succ-𝕋 k) (succ-𝕋 r))
+
+abstract
+  balance-iterated-succ-add-𝕋 :
+    (n : ℕ) (k r : 𝕋) → iterated-succ-𝕋 n k +𝕋 r ＝ k +𝕋 iterated-succ-𝕋 n r
+  balance-iterated-succ-add-𝕋 zero-ℕ k r = refl
+  balance-iterated-succ-add-𝕋 (succ-ℕ n) k r =
+    ( balance-iterated-succ-add-𝕋 n (succ-𝕋 k) r) ∙
+    ( balance-succ-add-𝕋 k (iterated-succ-𝕋 n r)) ∙
+    ( ap (k +𝕋_) (inv (reassociate-iterated-succ-𝕋 n r)))
+```
+
+### The double successor of addition is the double successor of addition
+
+```agda
+abstract
+  compute-add+2-𝕋 :
+    (k r : 𝕋) → add+2-𝕋 k r ＝ iterated-succ-𝕋 2 k +𝕋 r
+  compute-add+2-𝕋 k neg-two-𝕋 = refl
+  compute-add+2-𝕋 k (succ-𝕋 neg-two-𝕋) = refl
+  compute-add+2-𝕋 neg-two-𝕋 (succ-𝕋 (succ-𝕋 r)) =
+    left-unit-law-add+2-𝕋 (succ-𝕋 (succ-𝕋 r)) ∙
+    inv (left-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 r)))
+  compute-add+2-𝕋 (succ-𝕋 k) (succ-𝕋 (succ-𝕋 r)) =
+    ap succ-𝕋 (compute-add+2-𝕋 (succ-𝕋 k) (succ-𝕋 r))
+
+abstract
+  compute-add+2-𝕋' :
+    (k r : 𝕋) → add+2-𝕋 k r ＝ k +𝕋 iterated-succ-𝕋 2 r
+  compute-add+2-𝕋' k r = compute-add+2-𝕋 k r ∙ balance-iterated-succ-add-𝕋 2 k r
+```
+
+### Addition is not associative
+
+```agda
+example-not-associative-add-𝕋 :
+  (neg-two-𝕋 +𝕋 neg-two-𝕋) +𝕋 one-𝕋 ≠ neg-two-𝕋 +𝕋 (neg-two-𝕋 +𝕋 one-𝕋)
+example-not-associative-add-𝕋 ()
+
+not-associative-add-𝕋 : ¬ ((x y z : 𝕋) → (x +𝕋 y) +𝕋 z ＝ x +𝕋 (y +𝕋 z))
+not-associative-add-𝕋 α =
+  example-not-associative-add-𝕋 (α neg-two-𝕋 neg-two-𝕋 one-𝕋)
+```
+
+### Addition is commutative
+
+```agda
+abstract
+  commutative-add-𝕋 : (x y : 𝕋) → x +𝕋 y ＝ y +𝕋 x
+  commutative-add-𝕋 neg-two-𝕋 neg-two-𝕋 = refl
+  commutative-add-𝕋 neg-two-𝕋 (succ-𝕋 neg-two-𝕋) = refl
+  commutative-add-𝕋 neg-two-𝕋 (succ-𝕋 (succ-𝕋 y)) = refl
+  commutative-add-𝕋 (succ-𝕋 neg-two-𝕋) neg-two-𝕋 = refl
+  commutative-add-𝕋 (succ-𝕋 neg-two-𝕋) (succ-𝕋 neg-two-𝕋) = refl
+  commutative-add-𝕋 (succ-𝕋 neg-two-𝕋) (succ-𝕋 (succ-𝕋 y)) =
+    ap succ-𝕋 (commutative-add-𝕋 (succ-𝕋 neg-two-𝕋) (succ-𝕋 y))
+  commutative-add-𝕋 (succ-𝕋 (succ-𝕋 x)) neg-two-𝕋 = refl
+  commutative-add-𝕋 (succ-𝕋 (succ-𝕋 x)) (succ-𝕋 neg-two-𝕋) =
+    ap succ-𝕋 (commutative-add-𝕋 (succ-𝕋 x) (succ-𝕋 neg-two-𝕋))
+  commutative-add-𝕋 (succ-𝕋 (succ-𝕋 x)) (succ-𝕋 (succ-𝕋 y)) =
+    ap
+      ( succ-𝕋)
+      ( balance-succ-add-𝕋 (succ-𝕋 x) (succ-𝕋 y) ∙
+        commutative-add-𝕋 (succ-𝕋 x) (succ-𝕋 (succ-𝕋 y)))
+```

src/foundation/connected-maps.lagda.md

@@ -7,6 +7,7 @@ module foundation.connected-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.addition-truncation-levels
 open import foundation.connected-types
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
@@ -422,7 +423,7 @@ module _
 
 ```agda
 is-trunc-map-precomp-Π-is-connected-map :
-  {l1 l2 l3 : Level} (k l n : 𝕋) → k +𝕋 (succ-𝕋 (succ-𝕋 n)) ＝ l →
+  {l1 l2 l3 : Level} (k l n : 𝕋) → succ-𝕋 (succ-𝕋 n) +𝕋 k ＝ l →
   {A : UU l1} {B : UU l2} {f : A → B} → is-connected-map k f →
   (P : B → Truncated-Type l3 l) →
   is-trunc-map
@@ -436,7 +437,7 @@ is-trunc-map-precomp-Π-is-connected-map
         pair
           ( type-Truncated-Type (P b))
           ( is-trunc-eq
-            ( right-unit-law-add-𝕋 k)
+            ( left-unit-law-add-𝕋 k)
             ( is-trunc-type-Truncated-Type (P b)))))
 is-trunc-map-precomp-Π-is-connected-map k ._ (succ-𝕋 n) refl {A} {B} {f} H P =
   is-trunc-map-succ-precomp-Π
@@ -446,7 +447,7 @@ is-trunc-map-precomp-Π-is-connected-map k ._ (succ-𝕋 n) refl {A} {B} {f} H P
           pair
             ( eq-value g h b)
             ( is-trunc-eq
-              ( right-successor-law-add-𝕋 k n)
+              ( left-successor-law-add-𝕋 k n)
               ( is-trunc-type-Truncated-Type (P b))
               ( g b)
               ( h b))))