Dedekind finiteness of various notions of finite type

references.bib

@@ -10,6 +10,22 @@ @online{100theorems
   url           = {https://www.cs.ru.nl/~freek/100/},
 }
 
+@article{ABFJ20,
+  title         = {A generalized {B}lakers-{M}assey theorem},
+  author        = {Anel, Mathieu and Biedermann, Georg and Finster, Eric and Joyal, Andr\'e},
+  year          = 2020,
+  journal       = {J. Topol.},
+  fjournal      = {Journal of Topology},
+  volume        = 13,
+  number        = 4,
+  pages         = {1521--1553},
+  doi           = {10.1112/topo.12163},
+  issn          = {1753-8416,1753-8424},
+  mrclass       = {18N20 (18B25 18N45 55U35)},
+  mrnumber      = 4186137,
+  mrreviewer    = {Charles Rezk},
+}
+
 @article{AKS15,
   title         = {Univalent Categories and the {{Rezk}} Completion},
   author        = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},

src/category-theory/terminal-category.lagda.md

@@ -112,7 +112,7 @@ is-category-terminal-Category x y =
   is-equiv-is-contr
     ( iso-eq-Precategory terminal-Precategory x y)
     ( is-prop-unit x y)
-    ( is-contr-Σ is-contr-unit star
+    ( is-contr-Σ-unit
       ( is-proof-irrelevant-is-prop
         ( is-prop-is-iso-Precategory terminal-Precategory star)
         ( star , refl , refl)))

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

@@ -9,6 +9,8 @@ module elementary-number-theory.distance-natural-numbers where
 ```agda
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.minimum-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.strict-inequality-natural-numbers
@@ -19,6 +21,8 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.negation
 open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
@@ -66,6 +70,12 @@ dist-eq-ℕ' (succ-ℕ n) = dist-eq-ℕ' n
 dist-eq-ℕ : (m n : ℕ) → m ＝ n → is-zero-ℕ (dist-ℕ m n)
 dist-eq-ℕ m .m refl = dist-eq-ℕ' m
 
+dist-neq-ℕ : (m n : ℕ) → m ≠ n → is-nonzero-ℕ (dist-ℕ m n)
+dist-neq-ℕ m n = map-neg (eq-dist-ℕ m n)
+
+dist-neq-ℕ' : (m n : ℕ) → m ≠ n → is-successor-ℕ (dist-ℕ m n)
+dist-neq-ℕ' m n np = is-successor-is-nonzero-ℕ (dist-neq-ℕ m n np)
+
 is-one-dist-succ-ℕ : (x : ℕ) → is-one-ℕ (dist-ℕ x (succ-ℕ x))
 is-one-dist-succ-ℕ zero-ℕ = refl
 is-one-dist-succ-ℕ (succ-ℕ x) = is-one-dist-succ-ℕ x
@@ -283,7 +293,7 @@ leq-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
 
 ```agda
 strict-upper-bound-dist-ℕ :
-  (b x y : ℕ) → le-ℕ x b → le-ℕ y b → le-ℕ (dist-ℕ x y) b
+  (b x y : ℕ) → x <-ℕ b → y <-ℕ b → dist-ℕ x y <-ℕ b
 strict-upper-bound-dist-ℕ (succ-ℕ b) zero-ℕ y H K = K
 strict-upper-bound-dist-ℕ (succ-ℕ b) (succ-ℕ x) zero-ℕ H K = H
 strict-upper-bound-dist-ℕ (succ-ℕ b) (succ-ℕ x) (succ-ℕ y) H K =
@@ -294,14 +304,14 @@ strict-upper-bound-dist-ℕ (succ-ℕ b) (succ-ℕ x) (succ-ℕ y) H K =
 
 ```agda
 right-successor-law-dist-ℕ :
-  (x y : ℕ) → leq-ℕ x y → dist-ℕ x (succ-ℕ y) ＝ succ-ℕ (dist-ℕ x y)
+  (x y : ℕ) → x ≤-ℕ y → dist-ℕ x (succ-ℕ y) ＝ succ-ℕ (dist-ℕ x y)
 right-successor-law-dist-ℕ zero-ℕ zero-ℕ star = refl
 right-successor-law-dist-ℕ zero-ℕ (succ-ℕ y) star = refl
 right-successor-law-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
   right-successor-law-dist-ℕ x y H
 
 left-successor-law-dist-ℕ :
-  (x y : ℕ) → leq-ℕ y x → dist-ℕ (succ-ℕ x) y ＝ succ-ℕ (dist-ℕ x y)
+  (x y : ℕ) → y ≤-ℕ x → dist-ℕ (succ-ℕ x) y ＝ succ-ℕ (dist-ℕ x y)
 left-successor-law-dist-ℕ zero-ℕ zero-ℕ star = refl
 left-successor-law-dist-ℕ (succ-ℕ x) zero-ℕ star = refl
 left-successor-law-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
@@ -368,3 +378,18 @@ right-distributive-mul-dist-ℕ x y k =
   ( ( left-distributive-mul-dist-ℕ x y k) ∙
     ( ap-dist-ℕ (commutative-mul-ℕ k x) (commutative-mul-ℕ k y)))
 ```
+
+### The distance is the difference between the maximum and the minimum
+
+```agda
+eq-max-dist-min-ℕ : (x y : ℕ) → dist-ℕ x y +ℕ min-ℕ x y ＝ max-ℕ x y
+eq-max-dist-min-ℕ zero-ℕ y = refl
+eq-max-dist-min-ℕ (succ-ℕ x) zero-ℕ = refl
+eq-max-dist-min-ℕ (succ-ℕ x) (succ-ℕ y) = ap succ-ℕ (eq-max-dist-min-ℕ x y)
+
+dist-max-min-ℕ : (x y : ℕ) → dist-ℕ x y ＝ dist-ℕ (max-ℕ x y) (min-ℕ x y)
+dist-max-min-ℕ zero-ℕ zero-ℕ = refl
+dist-max-min-ℕ zero-ℕ (succ-ℕ y) = refl
+dist-max-min-ℕ (succ-ℕ x) zero-ℕ = refl
+dist-max-min-ℕ (succ-ℕ x) (succ-ℕ y) = dist-max-min-ℕ x y
+```

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

@@ -10,6 +10,7 @@ module elementary-number-theory.maximum-natural-numbers where
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
 
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
@@ -40,7 +41,7 @@ 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
+ap-max-ℕ p = ap-binary max-ℕ p
 
 max-ℕ' : ℕ → (ℕ → ℕ)
 max-ℕ' x y = max-ℕ y x
@@ -103,6 +104,26 @@ is-least-upper-bound-max-ℕ m n =
     ( λ x (H , K) → leq-max-ℕ x m n H K)
 ```
 
+### The maximum computes to the greater of the two numbers
+
+```agda
+abstract
+  leq-left-max-ℕ : (m n : ℕ) → n ≤-ℕ m → max-ℕ m n ＝ m
+  leq-left-max-ℕ zero-ℕ zero-ℕ p = refl
+  leq-left-max-ℕ (succ-ℕ m) zero-ℕ p = refl
+  leq-left-max-ℕ (succ-ℕ m) (succ-ℕ n) p = ap succ-ℕ (leq-left-max-ℕ m n p)
+
+  le-left-max-ℕ : (m n : ℕ) → n <-ℕ m → max-ℕ m n ＝ m
+  le-left-max-ℕ m n p = leq-left-max-ℕ m n (leq-le-ℕ n m p)
+
+  leq-right-max-ℕ : (m n : ℕ) → m ≤-ℕ n → max-ℕ m n ＝ n
+  leq-right-max-ℕ zero-ℕ n p = refl
+  leq-right-max-ℕ (succ-ℕ m) (succ-ℕ n) p = ap succ-ℕ (leq-right-max-ℕ m n p)
+
+  le-right-max-ℕ : (m n : ℕ) → m <-ℕ n → max-ℕ m n ＝ n
+  le-right-max-ℕ m n p = leq-right-max-ℕ m n (leq-le-ℕ m n p)
+```
+
 ### Associativity of `max-ℕ`
 
 ```agda

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

@@ -10,6 +10,7 @@ module elementary-number-theory.minimum-natural-numbers where
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.strict-inequality-natural-numbers
 
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
@@ -87,6 +88,26 @@ is-greatest-lower-bound-min-ℕ l m =
     ( λ x (H , K) → leq-min-ℕ x l m H K)
 ```
 
+### The minimum computes to the lesser of the two numbers
+
+```agda
+abstract
+  leq-left-min-ℕ : (m n : ℕ) → m ≤-ℕ n → min-ℕ m n ＝ m
+  leq-left-min-ℕ zero-ℕ n p = refl
+  leq-left-min-ℕ (succ-ℕ m) (succ-ℕ n) p = ap succ-ℕ (leq-left-min-ℕ m n p)
+
+  le-left-min-ℕ : (m n : ℕ) → m <-ℕ n → min-ℕ m n ＝ m
+  le-left-min-ℕ m n p = leq-left-min-ℕ m n (leq-le-ℕ m n p)
+
+  leq-right-min-ℕ : (m n : ℕ) → n ≤-ℕ m → min-ℕ m n ＝ n
+  leq-right-min-ℕ zero-ℕ zero-ℕ p = refl
+  leq-right-min-ℕ (succ-ℕ m) zero-ℕ p = refl
+  leq-right-min-ℕ (succ-ℕ m) (succ-ℕ n) p = ap succ-ℕ (leq-right-min-ℕ m n p)
+
+  le-right-min-ℕ : (m n : ℕ) → n <-ℕ m → min-ℕ m n ＝ n
+  le-right-min-ℕ m n p = leq-right-min-ℕ m n (leq-le-ℕ n m p)
+```
+
 ### Associativity of `min-ℕ`
 
 ```agda

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

@@ -81,8 +81,8 @@ one-ℕ⁺ = one-nonzero-ℕ
 
 ```agda
 succ-nonzero-ℕ : nonzero-ℕ → nonzero-ℕ
-pr1 (succ-nonzero-ℕ (pair x _)) = succ-ℕ x
-pr2 (succ-nonzero-ℕ (pair x _)) = is-nonzero-succ-ℕ x
+pr1 (succ-nonzero-ℕ (x , _)) = succ-ℕ x
+pr2 (succ-nonzero-ℕ (x , _)) = is-nonzero-succ-ℕ x
 ```
 
 ### The successor function from the natural numbers to the nonzero natural numbers
@@ -116,8 +116,8 @@ is-section-pred-nonzero-ℕ n = refl
 ```agda
 quotient-div-nonzero-ℕ :
   (d : ℕ) (x : nonzero-ℕ) (H : div-ℕ d (pr1 x)) → nonzero-ℕ
-pr1 (quotient-div-nonzero-ℕ d (pair x K) H) = quotient-div-ℕ d x H
-pr2 (quotient-div-nonzero-ℕ d (pair x K) H) = is-nonzero-quotient-div-ℕ H K
+pr1 (quotient-div-nonzero-ℕ d (x , K) H) = quotient-div-ℕ d x H
+pr2 (quotient-div-nonzero-ℕ d (x , K) H) = is-nonzero-quotient-div-ℕ H K
 ```
 
 ### Addition of nonzero natural numbers
@@ -152,13 +152,21 @@ _*ℕ⁺_ = mul-nonzero-ℕ
 ```agda
 le-ℕ⁺ : ℕ⁺ → ℕ⁺ → UU lzero
 le-ℕ⁺ (p , _) (q , _) = le-ℕ p q
+
+infix 30 _<-ℕ⁺_
+_<-ℕ⁺_ : ℕ⁺ → ℕ⁺ → UU lzero
+_<-ℕ⁺_ = le-ℕ⁺
 ```
 
 ### Inequality on nonzero natural numbers
 
 ```agda
 leq-ℕ⁺ : ℕ⁺ → ℕ⁺ → UU lzero
 leq-ℕ⁺ (p , _) (q , _) = leq-ℕ p q
+
+infix 30 _≤-ℕ⁺_
+_≤-ℕ⁺_ : ℕ⁺ → ℕ⁺ → UU lzero
+_≤-ℕ⁺_ = leq-ℕ⁺
 ```
 
 ### Addition of nonzero natural numbers is a strictly inflationary map
@@ -169,7 +177,7 @@ le-left-add-nat-ℕ⁺ m (n , n≠0) =
   tr
     ( λ p → le-ℕ p (m +ℕ n))
     ( right-unit-law-add-ℕ m)
-    ( preserves-le-left-add-ℕ m zero-ℕ n (le-is-nonzero-ℕ n n≠0))
+    ( preserves-le-left-add-ℕ m 0 n (le-is-nonzero-ℕ n n≠0))
 ```
 
 ### The predecessor function from the nonzero natural numbers reflects inequality

src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md

@@ -57,7 +57,7 @@ abstract
   trichotomy-sign-ℚ :
     {l : Level} {A : UU l} (x : ℚ) →
     ( is-negative-ℚ x → A) →
-    ( Id x zero-ℚ → A) →
+    ( x ＝ zero-ℚ → A) →
     ( is-positive-ℚ x → A) →
     A
   trichotomy-sign-ℚ x neg zero pos =

src/foundation-core/injective-maps.lagda.md

@@ -196,3 +196,4 @@ is-injective-is-contr f H p = eq-is-contr H
 
 - [Embeddings](foundation-core.embeddings.md)
 - [Path-cosplit maps](foundation.path-cosplit-maps.md)
+- [Noninjective maps](foundation.noninjective-maps.md)

src/foundation.lagda.md

@@ -322,6 +322,7 @@ open import foundation.multivariable-sections public
 open import foundation.negated-equality public
 open import foundation.negation public
 open import foundation.noncontractible-types public
+open import foundation.noninjective-maps public
 open import foundation.null-homotopic-maps public
 open import foundation.operations-span-diagrams public
 open import foundation.operations-spans public

src/foundation/axiom-of-choice.lagda.md

@@ -98,7 +98,7 @@ AC0 = {l1 l2 : Level} → level-AC0 l1 l2
 ```agda
 is-set-projective-AC0 :
   {l1 l2 l3 : Level} → level-AC0 l2 (l1 ⊔ l2) →
-  (X : UU l3) → is-set-projective l1 l2 X
+  (X : UU l3) → is-set-projective-Level l1 l2 X
 is-set-projective-AC0 ac X A B f h =
   map-trunc-Prop
     ( ( map-Σ
@@ -110,7 +110,7 @@ is-set-projective-AC0 ac X A B f h =
 
 AC0-is-set-projective :
   {l1 l2 : Level} →
-  ({l : Level} (X : UU l) → is-set-projective (l1 ⊔ l2) l1 X) →
+  ({l : Level} (X : UU l) → is-set-projective-Level (l1 ⊔ l2) l1 X) →
   level-AC0 l1 l2
 AC0-is-set-projective H A B K =
   map-trunc-Prop
@@ -122,6 +122,15 @@ AC0-is-set-projective H A B K =
         ( id))
 ```
 
+## Comments
+
+The axiom of choice fails to hold for arbitrary types. Indeed, it already fails
+to hold for the 0-connected 1-type $\operatorname{B}ℤ₂$ as demonstrated in
+Corollary 17.5.3 of {{#cite Rij22}}. This counterexample is formalized in
+[`foundation.global-choice`](foundation.global-choice.md). Hence it is both
+incompatible with univalence and with the existence of higher inductive types to
+assume the axiom of choice for all types.
+
 ## See also
 
 - [Diaconescu's theorem](foundation.diaconescus-theorem.md), which states that

src/foundation/cantor-schroder-bernstein-escardo.lagda.md

@@ -200,3 +200,14 @@ Cantor-Schröder-Bernstein lem A B f g =
   {{#cite TypeTopology}}
 
 {{#bibliography}}
+
+## See also
+
+The Cantor–Schröder–Bernstein–Escardó theorem holds constructively for many
+notions of finite type, including
+
+- [Finite types](univalent-combinatorics.finite-types.md) (unformalized)
+- [Subfinite types](univalent-combinatorics.subfinite-types.md)
+- [Kuratowski finite sets](univalent-combinatorics.kuratowski-finite-sets.md)
+- [Subfinitely enumerable types](univalent-combinatorics.subfinitely-enumerable-types.md)
+- [Dedekind finite types](univalent-combinatorics.dedekind-finite-types.md)

src/foundation/connected-maps.lagda.md

@@ -264,6 +264,20 @@ module _
       ( is-connected-map-connected-map f)
 ```
 
+### Right cancellation of connected maps
+
+```agda
+is-connected-map-left-factor :
+  {l1 l2 l3 : Level} (k : 𝕋)
+  {A : UU l1} {B : UU l2} {C : UU l3}
+  {g : B → C} {h : A → B} →
+  is-connected-map k h → is-connected-map k (g ∘ h) → is-connected-map k g
+is-connected-map-left-factor k {g = g} {h} H GH z =
+  is-connected-base k
+    ( H ∘ pr1)
+    ( is-connected-equiv' (compute-fiber-comp g h z) (GH z))
+```
+
 ### The total map induced by a family of maps is `k`-connected if and only if all maps in the family are `k`-connected
 
 ```agda