diff --git a/references.bib b/references.bib index 5aa8ba07ac..43a6c9ad75 100644 --- a/references.bib +++ b/references.bib @@ -10,6 +10,23 @@ @online{100theorems url = {https://www.cs.ru.nl/~freek/100/} } +@article{ABFJ20, + author = {Anel, Mathieu and Biedermann, Georg and Finster, Eric and + Joyal, Andr\'e}, + title = {A generalized {B}lakers-{M}assey theorem}, + journal = {J. Topol.}, + fjournal = {Journal of Topology}, + volume = {13}, + year = {2020}, + number = {4}, + pages = {1521--1553}, + issn = {1753-8416,1753-8424}, + mrclass = {18N20 (18B25 18N45 55U35)}, + mrnumber = {4186137}, + mrreviewer = {Charles Rezk}, + doi = {10.1112/topo.12163} +} + @article{AKS15, title = {Univalent Categories and the {{Rezk}} Completion}, author = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael}, diff --git a/src/category-theory/terminal-category.lagda.md b/src/category-theory/terminal-category.lagda.md index a8a8284077..148796feb6 100644 --- a/src/category-theory/terminal-category.lagda.md +++ b/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))) diff --git a/src/elementary-number-theory/distance-natural-numbers.lagda.md b/src/elementary-number-theory/distance-natural-numbers.lagda.md index 6026c735da..9684f71377 100644 --- a/src/elementary-number-theory/distance-natural-numbers.lagda.md +++ b/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 +``` diff --git a/src/elementary-number-theory/maximum-natural-numbers.lagda.md b/src/elementary-number-theory/maximum-natural-numbers.lagda.md index 97038be80f..d656c4912f 100644 --- a/src/elementary-number-theory/maximum-natural-numbers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/minimum-natural-numbers.lagda.md b/src/elementary-number-theory/minimum-natural-numbers.lagda.md index 71d9c60530..1f1d263d93 100644 --- a/src/elementary-number-theory/minimum-natural-numbers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/nonzero-natural-numbers.lagda.md b/src/elementary-number-theory/nonzero-natural-numbers.lagda.md index 9e4dc8c215..9984eccb26 100644 --- a/src/elementary-number-theory/nonzero-natural-numbers.lagda.md +++ b/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,6 +152,10 @@ _*ℕ⁺_ = mul-nonzero-ℕ ```agda le-ℕ⁺ : ℕ⁺ → ℕ⁺ → UU lzero le-ℕ⁺ (p , _) (q , _) = le-ℕ p q + +infix 30 _<-ℕ⁺_ +_<-ℕ⁺_ : ℕ⁺ → ℕ⁺ → UU lzero +_<-ℕ⁺_ = le-ℕ⁺ ``` ### Inequality on nonzero natural numbers @@ -159,6 +163,10 @@ le-ℕ⁺ (p , _) (q , _) = le-ℕ p q ```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 diff --git a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md b/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md index 31ad077ad0..3ac1335ce5 100644 --- a/src/elementary-number-theory/positive-and-negative-rational-numbers.lagda.md +++ b/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 = diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index 5d68b353e8..d295075633 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -402,7 +402,7 @@ not-leq-le-ℚ x y H K = trichotomy-le-ℚ : {l : Level} {A : UU l} (x y : ℚ) → ( le-ℚ x y → A) → - ( Id x y → A) → + ( x ＝ y → A) → ( le-ℚ y x → A) → A trichotomy-le-ℚ x y left eq right with decide-le-leq-ℚ x y | decide-le-leq-ℚ y x diff --git a/src/foundation-core/injective-maps.lagda.md b/src/foundation-core/injective-maps.lagda.md index 72003be269..7f9f17ec29 100644 --- a/src/foundation-core/injective-maps.lagda.md +++ b/src/foundation-core/injective-maps.lagda.md @@ -149,6 +149,9 @@ module _ is-injective-emb : (e : A ↪ B) → is-injective (map-emb e) is-injective-emb e {x} {y} = map-inv-is-equiv (is-emb-map-emb e x y) + + injection-emb : (A ↪ B) → injection A B + injection-emb e = (map-emb e , is-injective-emb e) ``` ### Any map out of a contractible type is injective @@ -164,3 +167,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) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index d99f9fbe70..47297a11f0 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -307,6 +307,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 diff --git a/src/foundation/axiom-of-choice.lagda.md b/src/foundation/axiom-of-choice.lagda.md index 26774379b7..6d195e79c1 100644 --- a/src/foundation/axiom-of-choice.lagda.md +++ b/src/foundation/axiom-of-choice.lagda.md @@ -88,7 +88,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-Σ @@ -100,7 +100,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 @@ -112,6 +112,14 @@ 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}}. 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 diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md index c48597b785..008d7180d1 100644 --- a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md +++ b/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) +- [Subfinite types](univalent-combinatorics.subfinite-types.md) +- [Kuratowski finite sets](univalent-combinatorics.kuratowski-finite-sets.md) +- [Subfinitely indexed types](univalent-combinatorics.subfinitely-indexed-types.md) +- [Dedekind finite types](univalent-combinatorics.dedekind-finite-types.md) diff --git a/src/foundation/connected-maps.lagda.md b/src/foundation/connected-maps.lagda.md index d893f11646..be43b567a7 100644 --- a/src/foundation/connected-maps.lagda.md +++ b/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 diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md index e7a26ab34e..06cf448eef 100644 --- a/src/foundation/connected-types.lagda.md +++ b/src/foundation/connected-types.lagda.md @@ -11,6 +11,7 @@ open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.diagonal-maps-of-types open import foundation.function-extensionality +open import foundation.function-types open import foundation.functoriality-truncation open import foundation.inhabited-types open import foundation.propositional-truncations @@ -110,6 +111,54 @@ is-connected-is-equiv-diagonal-exponential {k = k} {A} H = ( center (is-contr-map-is-equiv (H (trunc k A)) unit-trunc))) ``` +### Being connected is invariant under equivalence + +```agda +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} + where + + is-connected-is-equiv : + (f : A → B) → is-equiv f → is-connected k B → is-connected k A + is-connected-is-equiv f e = + is-contr-is-equiv + ( type-trunc k B) + ( map-trunc k f) + ( is-equiv-map-equiv-trunc k (f , e)) + + is-connected-equiv : + A ≃ B → is-connected k B → is-connected k A + is-connected-equiv f = + is-connected-is-equiv (map-equiv f) (is-equiv-map-equiv f) + +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} + where + + is-connected-equiv' : + A ≃ B → is-connected k A → is-connected k B + is-connected-equiv' f = is-connected-equiv (inv-equiv f) + + is-connected-is-equiv' : + (f : A → B) → is-equiv f → is-connected k A → is-connected k B + is-connected-is-equiv' f e = is-connected-equiv' (f , e) +``` + +### Retracts of `k`-connected types are `k`-connected + +```agda +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} + where + + is-connected-retract-of : + A retract-of B → + is-connected k B → + is-connected k A + is-connected-retract-of R = + is-contr-retract-of (type-trunc k B) (retract-of-trunc-retract-of R) +``` + ### A contractible type is `k`-connected for any `k` ```agda @@ -148,6 +197,31 @@ is-connected-Σ k H K = is-contr-equiv _ (equiv-trunc k (equiv-pr1 K) ∘e equiv-trunc-Σ k) H ``` +### If the total space of a family of `k`-connected types is `k`-connected so is the base + +**Proof.** We compute + +```text + ║Σ (x : A), B x║ₖ ≃ ║Σ (x : A), ║B x║ₖ║ₖ by equiv-trunc-Σ + ≃ ║Σ (x : A), 1 ║ₖ by k-connectedness of B + ≃ ║A║ₖ by the right unit law of Σ +``` + +and so, in particular, if the total space is `k`-connected so is the base. □ + +```agda +is-connected-base : + {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} → + ((x : A) → is-connected k (B x)) → is-connected k (Σ A B) → is-connected k A +is-connected-base k {A} {B} K = + is-contr-equiv' + ( type-trunc k (Σ A B)) + ( equivalence-reasoning + type-trunc k (Σ A B) + ≃ type-trunc k (Σ A (type-trunc k ∘ B)) by equiv-trunc-Σ k + ≃ type-trunc k A by equiv-trunc k (right-unit-law-Σ-is-contr K)) +``` + ### An inhabited type `A` is `k + 1`-connected if and only if its identity types are `k`-connected ```agda @@ -197,51 +271,3 @@ module _ ( λ where refl → refl) ( center (K a x))))) ``` - -### Being connected is invariant under equivalence - -```agda -module _ - {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} - where - - is-connected-is-equiv : - (f : A → B) → is-equiv f → is-connected k B → is-connected k A - is-connected-is-equiv f e = - is-contr-is-equiv - ( type-trunc k B) - ( map-trunc k f) - ( is-equiv-map-equiv-trunc k (f , e)) - - is-connected-equiv : - A ≃ B → is-connected k B → is-connected k A - is-connected-equiv f = - is-connected-is-equiv (map-equiv f) (is-equiv-map-equiv f) - -module _ - {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} - where - - is-connected-equiv' : - A ≃ B → is-connected k A → is-connected k B - is-connected-equiv' f = is-connected-equiv (inv-equiv f) - - is-connected-is-equiv' : - (f : A → B) → is-equiv f → is-connected k A → is-connected k B - is-connected-is-equiv' f e = is-connected-equiv' (f , e) -``` - -### Retracts of `k`-connected types are `k`-connected - -```agda -module _ - {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} - where - - is-connected-retract-of : - A retract-of B → - is-connected k B → - is-connected k A - is-connected-retract-of R = - is-contr-retract-of (type-trunc k B) (retract-of-trunc-retract-of R) -``` diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md index f4780285bd..051f6be3f1 100644 --- a/src/foundation/decidable-embeddings.lagda.md +++ b/src/foundation/decidable-embeddings.lagda.md @@ -641,3 +641,10 @@ module _ ( is-emb-terminal-map-is-prop (is-prop-type-Prop P))) ( p)) ``` + +## References + +Decidable embeddings are discussed in {{#cite Warn24}} under the name +_complemented embeddings_. + +{{#bibliography}} diff --git a/src/foundation/decidable-equality.lagda.md b/src/foundation/decidable-equality.lagda.md index 05a5b5b201..60edd06222 100644 --- a/src/foundation/decidable-equality.lagda.md +++ b/src/foundation/decidable-equality.lagda.md @@ -21,6 +21,7 @@ open import foundation.unit-type open import foundation.universe-levels open import foundation-core.cartesian-product-types +open import foundation-core.embeddings open import foundation-core.empty-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences @@ -128,6 +129,26 @@ abstract ( d (i x) (i y)) ``` +### Types with decidable equality are closed under injections + +```agda +has-decidable-equality-injection : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + injection A B → has-decidable-equality B → has-decidable-equality A +has-decidable-equality-injection (i , H) d x y = + is-decidable-iff H (ap i) (d (i x) (i y)) +``` + +### Types with decidable equality are closed under embeddings + +```agda +has-decidable-equality-emb : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + A ↪ B → has-decidable-equality B → has-decidable-equality A +has-decidable-equality-emb i = + has-decidable-equality-injection (injection-emb i) +``` + ### Types with decidable equality are closed under equivalences ```agda diff --git a/src/foundation/decidable-subtypes.lagda.md b/src/foundation/decidable-subtypes.lagda.md index 826dc8bc01..f7432a3c75 100644 --- a/src/foundation/decidable-subtypes.lagda.md +++ b/src/foundation/decidable-subtypes.lagda.md @@ -100,6 +100,11 @@ module _ (a : A) → is-prop (is-in-decidable-subtype a) is-prop-is-in-decidable-subtype = is-prop-is-in-subtype subtype-decidable-subtype + + is-proof-irrelevant-is-in-decidable-subtype : + (a : A) → is-proof-irrelevant (is-in-decidable-subtype a) + is-proof-irrelevant-is-in-decidable-subtype a = + is-proof-irrelevant-is-prop (is-prop-is-in-decidable-subtype a) ``` ### The underlying type of a decidable subtype diff --git a/src/foundation/double-negation.lagda.md b/src/foundation/double-negation.lagda.md index ee813f6384..a0cadde75d 100644 --- a/src/foundation/double-negation.lagda.md +++ b/src/foundation/double-negation.lagda.md @@ -7,6 +7,8 @@ module foundation.double-negation where
Imports ```agda +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types open import foundation.negation open import foundation.propositional-truncations open import foundation.universe-levels @@ -26,10 +28,10 @@ We define double negation and triple negation infix 25 ¬¬_ ¬¬¬_ ¬¬_ : {l : Level} → UU l → UU l -¬¬ P = ¬ (¬ P) +¬¬ P = ¬ ¬ P ¬¬¬_ : {l : Level} → UU l → UU l -¬¬¬ P = ¬ (¬ (¬ P)) +¬¬¬ P = ¬ ¬ ¬ P ``` We also define the introduction rule for double negation, and the action on maps @@ -42,6 +44,11 @@ intro-double-negation p f = f p map-double-negation : {l1 l2 : Level} {P : UU l1} {Q : UU l2} → (P → Q) → ¬¬ P → ¬¬ Q map-double-negation f = map-neg (map-neg f) + +map-binary-double-negation : + {l1 l2 l3 : Level} {P : UU l1} {Q : UU l2} {R : UU l3} → + (P → Q → R) → ¬¬ P → ¬¬ Q → ¬¬ R +map-binary-double-negation f nnp nnq nr = nnp (λ p → nnq (λ q → nr (f p q))) ``` ## Properties @@ -119,6 +126,22 @@ abstract map-double-negation unit-trunc-Prop ``` +### Distributivity over cartesian products + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + map-distributive-double-negation-product : ¬¬ (A × B) → (¬¬ A × ¬¬ B) + map-distributive-double-negation-product nnp = + ( map-double-negation pr1 nnp , map-double-negation pr2 nnp) + + map-inv-distributive-double-negation-product : (¬¬ A × ¬¬ B) → ¬¬ (A × B) + map-inv-distributive-double-negation-product (nna , nnb) = + map-binary-double-negation pair nna nnb +``` + ## See also - [Double negation elimination](logic.double-negation-elimination.md) diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md index 6631d6bead..9d0c224af3 100644 --- a/src/foundation/embeddings.lagda.md +++ b/src/foundation/embeddings.lagda.md @@ -127,6 +127,10 @@ module _ is-emb-left-map-triangle f g h H is-emb-g is-emb-h = is-emb-htpy H (is-emb-comp g h is-emb-g is-emb-h) + is-emb-map-comp-emb : + (g : B ↪ C) (f : A ↪ B) → is-emb (map-emb g ∘ map-emb f) + is-emb-map-comp-emb (g , H) (f , K) = is-emb-comp g f H K + comp-emb : (B ↪ C) → (A ↪ B) → (A ↪ C) pr1 (comp-emb (g , H) (f , K)) = g ∘ f diff --git a/src/foundation/functoriality-propositional-truncation.lagda.md b/src/foundation/functoriality-propositional-truncation.lagda.md index 1c895736c6..528189e246 100644 --- a/src/foundation/functoriality-propositional-truncation.lagda.md +++ b/src/foundation/functoriality-propositional-truncation.lagda.md @@ -29,7 +29,7 @@ open import foundation-core.propositions The universal property of propositional truncations can be used to define the functorial action of propositional truncations. -## Definition +## Definitions ```agda abstract @@ -47,6 +47,13 @@ abstract (A → B) → type-hom-Prop (trunc-Prop A) (trunc-Prop B) map-trunc-Prop f = pr1 (center (unique-map-trunc-Prop f)) + +abstract + map-binary-trunc-Prop : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} → + (A → B → C) → ║ A ║₋₁ → ║ B ║₋₁ → ║ C ║₋₁ + map-binary-trunc-Prop {C = C} f |a| |b| = + rec-trunc-Prop (trunc-Prop C) (λ a → map-trunc-Prop (f a) |b|) |a| ``` ## Properties diff --git a/src/foundation/inhabited-types.lagda.md b/src/foundation/inhabited-types.lagda.md index 93682e4ba5..f1c58d9901 100644 --- a/src/foundation/inhabited-types.lagda.md +++ b/src/foundation/inhabited-types.lagda.md @@ -167,7 +167,7 @@ module _ equiv-eq-Fam-Inhabited-Types ``` -### Inhabited types are closed under `Σ` +### Inhabited types are closed under Σ ```agda is-inhabited-Σ : @@ -193,6 +193,15 @@ pr2 (Σ-Inhabited-Type X Y) = ( λ x → is-inhabited-type-Inhabited-Type (Y x)) ``` +### The base of an inhabited Σ-type is inhabited + +```agda +is-inhabited-base-is-inhabited-Σ : + {l1 l2 : Level} {X : UU l1} {Y : X → UU l2} → + is-inhabited (Σ X Y) → is-inhabited X +is-inhabited-base-is-inhabited-Σ = map-trunc-Prop pr1 +``` + ### Inhabited types are closed under maps ```agda diff --git a/src/foundation/injective-maps.lagda.md b/src/foundation/injective-maps.lagda.md index 8ab3913353..a78c998391 100644 --- a/src/foundation/injective-maps.lagda.md +++ b/src/foundation/injective-maps.lagda.md @@ -44,17 +44,6 @@ maps between general types it is recommended to use the notion of ## Definitions -### Noninjective maps - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} - where - - is-not-injective : (A → B) → UU (l1 ⊔ l2) - is-not-injective f = ¬ (is-injective f) -``` - ### Any map out of an empty type is injective ```agda @@ -157,3 +146,4 @@ module _ - [Embeddings](foundation-core.embeddings.md) - [Path-cosplit maps](foundation.path-cosplit-maps.md) +- [Noninjective maps](foundation.noninjective-maps.md) diff --git a/src/foundation/isolated-elements.lagda.md b/src/foundation/isolated-elements.lagda.md index ebf38b94f7..b05d269f00 100644 --- a/src/foundation/isolated-elements.lagda.md +++ b/src/foundation/isolated-elements.lagda.md @@ -44,8 +44,9 @@ open import foundation-core.transport-along-identifications ## Idea -An element `a : A` is considered to be **isolated** if `a ＝ x` is -[decidable](foundation.decidable-types.md) for any `x`. +An element `a : A` is +{{#concept "isolated" Disambiguation="element of a type" Agda=is-isolated Agda=isolated-element}} +if `a ＝ x` is [decidable](foundation.decidable-types.md) for any `x`. ## Definitions diff --git a/src/foundation/noncontractible-types.lagda.md b/src/foundation/noncontractible-types.lagda.md index 98d2d49311..3bac075e07 100644 --- a/src/foundation/noncontractible-types.lagda.md +++ b/src/foundation/noncontractible-types.lagda.md @@ -120,3 +120,7 @@ the free loop. In fact, the free fixed point of the operation `1 + Σ(-)`, where `Σ` is the [suspension operator](synthetic-homotopy-theory.suspensions-of-types.md), is $n$-noncontractible for every $n ≥ 1$. + +## See also + +- [Noninjective maps](foundation.noninjective-maps.md) diff --git a/src/foundation/noninjective-maps.lagda.md b/src/foundation/noninjective-maps.lagda.md new file mode 100644 index 0000000000..f0ff9d93ee --- /dev/null +++ b/src/foundation/noninjective-maps.lagda.md @@ -0,0 +1,147 @@ +# Noninjective maps + +```agda +module foundation.noninjective-maps where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.functoriality-dependent-pair-types +open import foundation.functoriality-propositional-truncation +open import foundation.inhabited-types +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.repetitions-of-values +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.function-types +open import foundation-core.identity-types +open import foundation-core.injective-maps +open import foundation-core.propositions +``` + +
+ +## Idea + +_Noninjectivity_ is a positive way of stating that a map is +[not](foundation.negation.md) [injective](foundation-core.injective-maps.md). A +map `f : A → B` is +{{#concept "noninjective" Disambiguation="map of types" Agda=is-noninjective}} +if there [exists](foundation.existential-quantification.md) a +[pair of distinct elements](foundation.pairs-of-distinct-elements.md) `x ≠ y` of +`A` that are mapped to the [same](foundation-core.identity-types.md) value in +`B`, `f x ＝ f y`. In other words, if `f` +[repeats a value](foundation.repetitions-of-values.md). + +## Definitions + +### Not injective maps + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-not-injective : (A → B) → UU (l1 ⊔ l2) + is-not-injective f = ¬ (is-injective f) + + is-prop-is-not-injective : {f : A → B} → is-prop (is-not-injective f) + is-prop-is-not-injective = is-prop-neg + + is-not-injective-Prop : (A → B) → Prop (l1 ⊔ l2) + is-not-injective-Prop f = (is-not-injective f , is-prop-is-not-injective) +``` + +### Noninjective maps + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-noninjective-Prop : (A → B) → Prop (l1 ⊔ l2) + is-noninjective-Prop f = trunc-Prop (repetition-of-values f) + + is-noninjective : (A → B) → UU (l1 ⊔ l2) + is-noninjective f = type-Prop (is-noninjective-Prop f) + + is-prop-is-noninjective : {f : A → B} → is-prop (is-noninjective f) + is-prop-is-noninjective {f} = is-prop-type-Prop (is-noninjective-Prop f) +``` + +### The type of noninjective maps + +```agda +noninjective-map : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +noninjective-map A B = Σ (A → B) is-noninjective + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : noninjective-map A B) + where + + map-noninjective-map : A → B + map-noninjective-map = pr1 f + + is-noninjective-map-noninjective-map : is-noninjective map-noninjective-map + is-noninjective-map-noninjective-map = pr2 f +``` + +## Properties + +### Noninjective maps are not injective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + abstract + is-not-injective-is-noninjective : is-noninjective f → is-not-injective f + is-not-injective-is-noninjective = + rec-trunc-Prop + ( is-not-injective-Prop f) + ( λ ((x , y , x≠y) , p) H → x≠y (H p)) +``` + +### Noninjectivity of composites + +Given maps `f : A → B` and `g : B → C`, then + +- if `f` is noninjective then `g ∘ f` is noninjective. +- if `g` is injective and `g ∘ f` is noninjective then `f` is noninjective. + +```agda +module _ + {l1 l2 l3 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} + {f : A → B} {g : B → C} + where + + ap-repetition-of-values : + repetition-of-values f → repetition-of-values (g ∘ f) + ap-repetition-of-values (q , p) = (q , ap g p) + + is-noninjective-comp : + is-noninjective f → is-noninjective (g ∘ f) + is-noninjective-comp = + map-trunc-Prop ap-repetition-of-values + + inv-ap-repetition-of-values : + is-injective g → repetition-of-values (g ∘ f) → repetition-of-values f + inv-ap-repetition-of-values G (q , p) = (q , G p) + + is-noninjective-right-factor : + is-injective g → is-noninjective (g ∘ f) → is-noninjective f + is-noninjective-right-factor G = + map-trunc-Prop (inv-ap-repetition-of-values G) +``` + +## See also + +- [Noncontractible types](foundation.noncontractible-types.md) diff --git a/src/foundation/projective-types.lagda.md b/src/foundation/projective-types.lagda.md index f537366853..e700e804bb 100644 --- a/src/foundation/projective-types.lagda.md +++ b/src/foundation/projective-types.lagda.md @@ -10,6 +10,7 @@ module foundation.projective-types where open import elementary-number-theory.natural-numbers open import foundation.connected-maps +open import foundation.inhabited-types open import foundation.postcomposition-functions open import foundation.surjective-maps open import foundation.truncation-levels @@ -24,47 +25,57 @@ open import foundation-core.truncated-types ## Idea -A type `X` is said to be **set-projective** if for every surjective map -`f : A → B` into a set `B` the postcomposition function +A type `X` is said to be {{#concept "set-projective" Agda=is-set-projective}} if +for every [surjective map](foundation.surjective-maps.md) `f : A ↠ B` onto a +[set](foundation-core.sets.md) `B` the [postcomposition +function[(foundation-core.postcomposition-functions.md) ```text (X → A) → (X → B) ``` -is surjective. This is equivalent to the condition that for every equivalence -relation `R` on a type `A` the natural map +is surjective. This is [equivalent](foundation.logical-equivalences.md) to the +condition that for every [equivalence +relation[(foundation-core.equivalence-relations.md) `R` on a type `A` the +natural map ```text (X → A)/~ → (X → A/R) ``` -is an equivalence. The latter map is always an embedding, and it is an -equivalence for every `X`, `A`, and `R` if and only if the axiom of choice -holds. +is an [equivalence](foundation-core.equivalences.md). The latter map is always +an [embedding](foundation-core.embeddings.md), and it is an equivalence for +every `X`, `A`, and `R` if and only if +[the axiom of choice](foundation.axiom-of-choice.md) holds. -The notion of set-projectiveness generalizes to `n`-projectiveness, for `n : ℕ`. -A type `X` is said to be `k`-projective if the postcomposition function -`(X → A) → (X → B)` is surjective for every `k-1`-connected map `f : A → B` into -a `k`-truncated type `B`. +The notion of set-projectiveness generalizes to +{{#concept "`n`-projectiveness" Agda=is-trunc-projective}}, for every +[natural number](elementary-number-theory.natural-numbers.md) `n`. A type `X` is +said to be `k`-projective if the postcomposition function `(X → A) → (X → B)` is +surjective for every `k-1`-[connected map](foundation.connected-maps.md) +`f : A → B` into a `k`-[truncated type](foundation-core.truncated-types.md) `B`. ## Definitions ### Set-projective types ```agda -is-set-projective : +is-set-projective-Level : {l1 : Level} (l2 l3 : Level) → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) -is-set-projective l2 l3 X = +is-set-projective-Level l2 l3 X = (A : UU l2) (B : Set l3) (f : A ↠ type-Set B) → is-surjective (postcomp X (map-surjection f)) + +is-set-projective : {l1 : Level} → UU l1 → UUω +is-set-projective X = {l2 l3 : Level} → is-set-projective-Level l2 l3 X ``` ### `k`-projective types ```agda -is-projective : - {l1 : Level} (l2 l3 : Level) (k : ℕ) → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) -is-projective l2 l3 k X = +is-trunc-projective-Level : + {l1 : Level} (l2 l3 : Level) → ℕ → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) +is-trunc-projective-Level l2 l3 k X = ( A : UU l2) (B : Truncated-Type l3 (truncation-level-ℕ k)) ( f : connected-map @@ -72,9 +83,25 @@ is-projective l2 l3 k X = ( A) ( type-Truncated-Type B)) → is-surjective (postcomp X (map-connected-map f)) + +is-trunc-projective : {l1 : Level} → ℕ → UU l1 → UUω +is-trunc-projective k X = {l2 l3 : Level} → is-trunc-projective-Level l2 l3 k X +``` + +### Alternative statement of projectivity + +```agda +is-projective-Level' : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +is-projective-Level' l2 X = + (P : X → UU l2) → + ((x : X) → is-inhabited (P x)) → + is-inhabited ((x : X) → (P x)) + +is-projective' : {l1 : Level} → UU l1 → UUω +is-projective' X = {l2 : Level} → is-projective-Level' l2 X ``` ## See also -- The natural map `(X → A)/~ → (X → A/R)` was studied in - [foundation.exponents-set-quotients](foundation.exponents-set-quotients.md) +- The natural map `(X → A)/~ → (X → A/R)` is studied in + [`foundation.exponents-set-quotients`](foundation.exponents-set-quotients.md) diff --git a/src/foundation/repetitions-of-values.lagda.md b/src/foundation/repetitions-of-values.lagda.md index cbecce73b5..c8a9f50fe1 100644 --- a/src/foundation/repetitions-of-values.lagda.md +++ b/src/foundation/repetitions-of-values.lagda.md @@ -13,6 +13,7 @@ open import foundation.embeddings open import foundation.equivalences open import foundation.identity-types open import foundation.negated-equality +open import foundation.negation open import foundation.pairs-of-distinct-elements open import foundation.universe-levels @@ -21,14 +22,20 @@ open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.injective-maps +open import foundation-core.retractions +open import foundation-core.sections ```
## Idea -A repetition of values of a map `f : A → B` consists of a pair of distinct -points in `A` that get mapped to the same point in `B`. +A +{{#concept "repetition of values" Disambiguation="of a map of types" Agda=repetition-of-values}} +of a map `f : A → B` consists of a +[pair of distinct elements](foundation.pairs-of-distinct-elements.md) `x ≠ y` of +`A` that get mapped to the [same](foundation-core.identity-types.md) element in +`B`: `f x ＝ f y`. ## Definitions @@ -39,8 +46,7 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where - is-repetition-of-values : - (f : A → B) (p : pair-of-distinct-elements A) → UU l2 + is-repetition-of-values : (A → B) → pair-of-distinct-elements A → UU l2 is-repetition-of-values f p = f (first-pair-of-distinct-elements p) ＝ f (second-pair-of-distinct-elements p) @@ -75,8 +81,7 @@ module _ pair-of-distinct-elements-repetition-of-values is-repetition-of-values-repetition-of-values : - is-repetition-of-values f - pair-of-distinct-elements-repetition-of-values + is-repetition-of-values f pair-of-distinct-elements-repetition-of-values is-repetition-of-values-repetition-of-values = pr2 r ``` @@ -84,33 +89,58 @@ module _ ```agda is-repeated-value : - {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (a : A) → UU (l1 ⊔ l2) -is-repeated-value {l1} {l2} {A} {B} f a = + {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → A → UU (l1 ⊔ l2) +is-repeated-value {A = A} f a = Σ (Σ A (λ x → a ≠ x)) (λ x → f a ＝ f (pr1 x)) ``` ## Properties +### Maps with repetitions of values are not injective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + is-not-injective-repetition-of-values : + repetition-of-values f → ¬ (is-injective f) + is-not-injective-repetition-of-values r H = + distinction-repetition-of-values f r + ( H (is-repetition-of-values-repetition-of-values f r)) +``` + ### Repetitions of values of composite maps ```agda -repetition-of-values-comp : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C) - {f : A → B} → repetition-of-values f → repetition-of-values (g ∘ f) -repetition-of-values-comp g ((x , y , s) , t) = - ((x , y , s) , ap g t) - -repetition-of-values-left-factor : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {g : B → C} - {f : A → B} → is-emb f → repetition-of-values (g ∘ f) → repetition-of-values g -repetition-of-values-left-factor {g = g} {f} H ((a , b , K) , p) = - ((f a , f b , λ q → K (is-injective-is-emb H q)) , p) - -repetition-of-values-right-factor : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {g : B → C} - {f : A → B} → is-emb g → repetition-of-values (g ∘ f) → repetition-of-values f -repetition-of-values-right-factor {g = g} {f} H ((a , b , K) , p) = - ((a , b , K) , is-injective-is-emb H p) +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {g : B → C} {f : A → B} + where + + repetition-of-values-comp : + repetition-of-values f → repetition-of-values (g ∘ f) + repetition-of-values-comp ((x , y , s) , t) = + ((x , y , s) , ap g t) + + repetition-of-values-left-factor' : + is-injective f → repetition-of-values (g ∘ f) → repetition-of-values g + repetition-of-values-left-factor' H ((a , b , K) , p) = + ((f a , f b , λ q → K (H q)) , p) + + repetition-of-values-left-factor : + is-emb f → repetition-of-values (g ∘ f) → repetition-of-values g + repetition-of-values-left-factor H = + repetition-of-values-left-factor' (is-injective-is-emb H) + + repetition-of-values-right-factor' : + is-injective g → repetition-of-values (g ∘ f) → repetition-of-values f + repetition-of-values-right-factor' H ((a , b , K) , p) = ((a , b , K) , H p) + + repetition-of-values-right-factor : + is-emb g → repetition-of-values (g ∘ f) → repetition-of-values f + repetition-of-values-right-factor H = + repetition-of-values-right-factor' (is-injective-is-emb H) ``` ### The type of repetitions of values is invariant under equivalences @@ -150,17 +180,24 @@ module _ map-inv-equiv-repetition-of-values = map-inv-equiv equiv-repetition-of-values is-section-map-inv-equiv-repetition-of-values : - ( map-equiv-repetition-of-values ∘ map-inv-equiv-repetition-of-values) ~ id + is-section + ( map-equiv-repetition-of-values) + ( map-inv-equiv-repetition-of-values) is-section-map-inv-equiv-repetition-of-values = is-section-map-inv-equiv equiv-repetition-of-values is-retraction-map-inv-equiv-repetition-of-values : - ( map-inv-equiv-repetition-of-values ∘ map-equiv-repetition-of-values) ~ id + is-retraction + ( map-equiv-repetition-of-values) + ( map-inv-equiv-repetition-of-values) is-retraction-map-inv-equiv-repetition-of-values = is-retraction-map-inv-equiv equiv-repetition-of-values ``` -### Embeddings of repetitions values +### Embeddings of repetitions of values + +Given an embedding of arrows `f ↪ g`, then the type of repetitions of values of +`f` embeds into the type of repetitions of values of `g`. ```agda module _ @@ -192,3 +229,7 @@ module _ is-emb-map-emb-repetition-of-values : is-emb map-emb-repetition-of-values is-emb-map-emb-repetition-of-values = is-emb-map-emb emb-repetition-of-values ``` + +## See also + +- [Noninjective maps](foundation.noninjective-maps.md) diff --git a/src/foundation/set-presented-types.lagda.md b/src/foundation/set-presented-types.lagda.md index 658f0388f7..1c683dcbdb 100644 --- a/src/foundation/set-presented-types.lagda.md +++ b/src/foundation/set-presented-types.lagda.md @@ -7,7 +7,9 @@ module foundation.set-presented-types where
Imports ```agda +open import foundation.1-types open import foundation.action-on-identifications-functions +open import foundation.connected-maps open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.embeddings @@ -23,39 +25,92 @@ open import foundation.images open import foundation.injective-maps open import foundation.propositional-truncations open import foundation.set-truncations +open import foundation.sets open import foundation.subtypes open import foundation.surjective-maps +open import foundation.truncation-levels open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.propositions -open import foundation-core.sets ```
## Idea -A type `A` is said to be -{{#concept "set presented" Agda=has-set-presentation-Prop}} if there -[exists](foundation.existential-quantification.md) a map `f : X → A` from a -[set](foundation-core.sets.md) `X` such that the composite -`X → A → type-trunc-Set A` is an [equivalence](foundation.equivalences.md). +A type `A` is said to be {{#concept "set presented" Agda=has-set-presentation}} +if there [exists](foundation.existential-quantification.md) a map `f : X → A` +from a [set](foundation-core.sets.md) `X` such that the composite +`η ∘ f : X → A → ║A║₀` is an [equivalence](foundation.equivalences.md). ## Definitions -### Set presentations of types +### The underlying structure of a set presentation + +```agda +is-set-presentation-map : + {l1 l2 : Level} {A : UU l1} (X : Set l2) → (type-Set X → A) → UU (l1 ⊔ l2) +is-set-presentation-map X f = is-equiv (unit-trunc-Set ∘ f) + +set-presentation-structure : {l1 l2 : Level} → UU l1 → Set l2 → UU (l1 ⊔ l2) +set-presentation-structure A X = Σ (type-Set X → A) (is-set-presentation-map X) + +module _ + {l1 l2 : Level} {A : UU l1} (X : Set l2) (f : set-presentation-structure A X) + where + + map-set-presentation-structure : type-Set X → A + map-set-presentation-structure = pr1 f + + is-set-presentation-map-map-set-presentation-structure : + is-set-presentation-map X map-set-presentation-structure + is-set-presentation-map-map-set-presentation-structure = pr2 f +``` + +### The predicate on a set of being a set presentation of a type + +```agda +module _ + {l1 l2 : Level} (A : UU l1) (X : Set l2) + where + + is-set-presentation-Prop : Prop (l1 ⊔ l2) + is-set-presentation-Prop = trunc-Prop (set-presentation-structure A X) + + is-set-presentation : UU (l1 ⊔ l2) + is-set-presentation = type-Prop is-set-presentation-Prop + + is-prop-is-set-presentation : is-prop is-set-presentation + is-prop-is-set-presentation = is-prop-type-Prop is-set-presentation-Prop +``` + +### The type of set presentations of a type at a universe level + +```agda +module _ + {l1 : Level} (l2 : Level) (A : UU l1) + where + + set-presentation : UU (l1 ⊔ lsuc l2) + set-presentation = Σ (Set l2) (is-set-presentation A) + + is-1-type-set-presentation : is-1-type set-presentation + is-1-type-set-presentation = + is-1-type-type-subtype (is-set-presentation-Prop A) is-1-type-Set +``` + +### The predicate of having a set presentation at a universe level ```agda module _ - {l1 l2 : Level} (A : Set l1) (B : UU l2) + {l1 : Level} (l2 : Level) (A : UU l1) where - has-set-presentation-Prop : Prop (l1 ⊔ l2) - has-set-presentation-Prop = - ∃ (type-Set A → B) (λ f → is-equiv-Prop (unit-trunc-Set ∘ f)) + has-set-presentation-Prop : Prop (l1 ⊔ lsuc l2) + has-set-presentation-Prop = trunc-Prop (set-presentation l2 A) - has-set-presentation : UU (l1 ⊔ l2) + has-set-presentation : UU (l1 ⊔ lsuc l2) has-set-presentation = type-Prop has-set-presentation-Prop is-prop-has-set-presentation : is-prop has-set-presentation @@ -66,31 +121,31 @@ module _ ### Types set presented by coproducts are coproducts -Given a type `B` that is set presented by a coproduct +Given a type `A` that is set presented by a coproduct ```text - B + A ∧ \ f / \ η / ~ ∨ - (A1 + A2) -----> ║B║₀, + (X1 + X2) -----> ║A║₀, ``` -then `B` computes as the coproduct of the images of the restrictions of `f` -along the left and right inclusion of the coproduct `A1 + A2` +then `A` computes as the coproduct of the images of the restrictions of `f` +along the left and right inclusion of the coproduct `X1 + X2` ```text - B ≃ im (f ∘ inl) + im (f ∘ inr). + A ≃ im (f ∘ inl) + im (f ∘ inr). ``` ```agda module _ - {l1 l2 l3 : Level} {A1 : UU l1} {A2 : UU l2} {B : UU l3} - (f : A1 + A2 → B) (e : (A1 + A2) ≃ ║ B ║₀) + {l1 l2 l3 : Level} {X1 : UU l1} {X2 : UU l2} {A : UU l3} + (f : X1 + X2 → A) (e : (X1 + X2) ≃ ║ A ║₀) (H : unit-trunc-Set ∘ f ~ map-equiv e) where - map-is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) → B + map-is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) → A map-is-coproduct-codomain = rec-coproduct pr1 pr1 triangle-is-coproduct-codomain : @@ -137,10 +192,10 @@ module _ ( a)) , ( triangle-is-coproduct-codomain a ∙ inv p))) where - a : A1 + A2 + a : X1 + X2 a = map-inv-equiv e (unit-trunc-Set b) - is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) ≃ B + is-coproduct-codomain : (im (f ∘ inl) + im (f ∘ inr)) ≃ A pr1 is-coproduct-codomain = map-is-coproduct-codomain pr2 is-coproduct-codomain = is-equiv-is-emb-is-surjective diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index f6fc1ffb05..213be213e7 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -15,6 +15,7 @@ open import foundation.diagonal-maps-of-types open import foundation.embeddings open import foundation.equality-cartesian-product-types open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-propositional-truncation open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction open import foundation.identity-types @@ -265,6 +266,9 @@ module _ is-surjective-id : is-surjective (id {A = A}) is-surjective-id a = unit-trunc-Prop (a , refl) + + id-surjection : A ↠ A + id-surjection = (id , is-surjective-id) ``` ### Maps which are homotopic to surjective maps are surjective @@ -532,7 +536,7 @@ module _ abstract is-surjective-right-map-triangle : - (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) → + (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h) → is-surjective f → is-surjective g is-surjective-right-map-triangle f g h H is-surj-f x = apply-universal-property-trunc-Prop @@ -644,7 +648,7 @@ equiv-Surjection : Surjection l2 A → Surjection l3 A → UU (l1 ⊔ l2 ⊔ l3) equiv-Surjection f g = Σ ( type-Surjection f ≃ type-Surjection g) - ( λ e → (map-equiv e ∘ map-Surjection f) ~ map-Surjection g) + ( λ e → map-equiv e ∘ map-Surjection f ~ map-Surjection g) module _ {l1 l2 : Level} {A : UU l1} (f : Surjection l2 A) @@ -850,9 +854,7 @@ module _ is-inhabited-is-surjective : {f : A → B} → is-surjective f → is-inhabited B → is-inhabited A is-inhabited-is-surjective F = - rec-trunc-Prop - ( is-inhabited-Prop A) - ( rec-trunc-Prop (is-inhabited-Prop A) (unit-trunc-Prop ∘ pr1) ∘ F) + rec-trunc-Prop (is-inhabited-Prop A) (map-trunc-Prop pr1 ∘ F) is-inhabited-surjection : A ↠ B → is-inhabited B → is-inhabited A @@ -862,8 +864,8 @@ module _ ### The type of surjections `A ↠ B` is equivalent to the type of families `P` of inhabited types over `B` equipped with an equivalence `A ≃ Σ B P` -This remains to be shown. -[#735](https://github.com/UniMath/agda-unimath/issues/735) +> This remains to be shown. +> [#735](https://github.com/UniMath/agda-unimath/issues/735) ## See also diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md index d1246282e0..34a0415d7f 100644 --- a/src/foundation/unit-type.lagda.md +++ b/src/foundation/unit-type.lagda.md @@ -243,3 +243,12 @@ module _ retraction-point : retraction (point x) retraction-point = terminal-map A , refl-htpy ``` + +### Contractibility of dependent sums over the unit type + +```agda +abstract + is-contr-Σ-unit : + {l : Level} {B : unit → UU l} → is-contr (B star) → is-contr (Σ unit B) + is-contr-Σ-unit = is-contr-Σ is-contr-unit star +``` diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md index f7e47b899e..571015a471 100644 --- a/src/set-theory.lagda.md +++ b/src/set-theory.lagda.md @@ -28,7 +28,7 @@ this sense. Indeed, that `is-small l` is a predicate is equivalent to the connection between set theory and univalent type theory that is not directly compatible with the preconception that "set theory is a study of set-level mathematics". Namely, the universe of sets need not itself be a set-level -structure. In fact, with univalence it is a +structure. In fact, with univalence it is a proper [1-type](foundation-core.1-types.md). In this module, we consider ideas historically related to the study of set diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index 60423d0894..e071a5c220 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -78,6 +78,23 @@ module _ is-prop-is-acyclic-map f = is-prop-type-Prop (is-acyclic-map-Prop f) ``` +### The type of acyclic maps + +```agda +acyclic-map : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +acyclic-map A B = Σ (A → B) (is-acyclic-map) + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : acyclic-map A B) + where + + map-acyclic-map : A → B + map-acyclic-map = pr1 f + + is-acyclic-acyclic-map : is-acyclic-map map-acyclic-map + is-acyclic-acyclic-map = pr2 f +``` + ## Properties ### A map is acyclic if and only if it is an [epimorphism](foundation.epimorphisms.md) @@ -290,20 +307,29 @@ corresponding facts about [epimorphisms](foundation.epimorphisms.md). ```agda module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} - (g : B → C) (f : A → B) where is-acyclic-map-comp : + {g : B → C} {f : A → B} → is-acyclic-map g → is-acyclic-map f → is-acyclic-map (g ∘ f) - is-acyclic-map-comp ag af = + is-acyclic-map-comp {g} {f} ag af = is-acyclic-map-is-epimorphism (g ∘ f) ( is-epimorphism-comp g f ( is-epimorphism-is-acyclic-map g ag) ( is-epimorphism-is-acyclic-map f af)) + is-acyclic-map-comp-acyclic-map : + (g : acyclic-map B C) (f : acyclic-map A B) → + is-acyclic-map (map-acyclic-map g ∘ map-acyclic-map f) + is-acyclic-map-comp-acyclic-map (g , ag) (f , af) = is-acyclic-map-comp ag af + + comp-acyclic-map : acyclic-map B C → acyclic-map A B → acyclic-map A C + comp-acyclic-map (g , ag) (f , af) = (g ∘ f , is-acyclic-map-comp ag af) + is-acyclic-map-left-factor : + {g : B → C} {f : A → B} → is-acyclic-map (g ∘ f) → is-acyclic-map f → is-acyclic-map g - is-acyclic-map-left-factor ac af = + is-acyclic-map-left-factor {g} {f} ac af = is-acyclic-map-is-epimorphism g ( is-epimorphism-left-factor g f ( is-epimorphism-is-acyclic-map (g ∘ f) ac) @@ -476,8 +502,6 @@ module _ is-acyclic-is-acyclic-map-terminal-map ( Σ A B) ( is-acyclic-map-comp - ( terminal-map A) - ( pr1) ( is-acyclic-map-terminal-map-is-acyclic A ac-A) ( λ a → is-acyclic-equiv (equiv-fiber-pr1 B a) (ac-B a))) ``` @@ -495,8 +519,6 @@ module _ is-acyclic-is-acyclic-map-terminal-map ( A × B) ( is-acyclic-map-comp - ( terminal-map B) - ( pr2) ( is-acyclic-map-terminal-map-is-acyclic B ac-B) ( is-acyclic-map-horizontal-map-cone-is-pullback ( terminal-map A) @@ -523,8 +545,6 @@ module _ ( λ a → is-acyclic-is-acyclic-map-terminal-map A ( is-acyclic-map-left-factor - ( terminal-map A) - ( point a) ( is-acyclic-map-terminal-map-is-acyclic unit is-acyclic-unit) ( λ b → is-acyclic-equiv (compute-fiber-point a b) (l-ac a b)))) ``` diff --git a/src/synthetic-homotopy-theory/acyclic-types.lagda.md b/src/synthetic-homotopy-theory/acyclic-types.lagda.md index 35473b70bf..cb83beef9d 100644 --- a/src/synthetic-homotopy-theory/acyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-types.lagda.md @@ -78,6 +78,10 @@ is-acyclic-unit : is-acyclic unit is-acyclic-unit = is-acyclic-is-contr unit is-contr-unit ``` +### Acyclic types are inhabited + +> TODO + ## See also - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md) diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md index 96025ac714..bc2bc48e35 100644 --- a/src/univalent-combinatorics.lagda.md +++ b/src/univalent-combinatorics.lagda.md @@ -37,7 +37,6 @@ open import univalent-combinatorics.coproduct-types public open import univalent-combinatorics.counting public open import univalent-combinatorics.counting-decidable-subtypes public open import univalent-combinatorics.counting-dependent-pair-types public -open import univalent-combinatorics.counting-fibers-of-maps public open import univalent-combinatorics.counting-maybe public open import univalent-combinatorics.cubes public open import univalent-combinatorics.cycle-partitions public @@ -50,11 +49,13 @@ open import univalent-combinatorics.decidable-equivalence-relations public open import univalent-combinatorics.decidable-propositions public open import univalent-combinatorics.decidable-subtypes public open import univalent-combinatorics.dedekind-finite-sets public +open import univalent-combinatorics.dedekind-finite-types public open import univalent-combinatorics.dependent-function-types public open import univalent-combinatorics.dependent-pair-types public open import univalent-combinatorics.discrete-sigma-decompositions public open import univalent-combinatorics.distributivity-of-set-truncation-over-finite-products public open import univalent-combinatorics.double-counting public +open import univalent-combinatorics.dual-dedekind-finite-types public open import univalent-combinatorics.embeddings public open import univalent-combinatorics.embeddings-standard-finite-types public open import univalent-combinatorics.equality-finite-types public @@ -65,7 +66,6 @@ open import univalent-combinatorics.equivalences-standard-finite-types public open import univalent-combinatorics.ferrers-diagrams public open import univalent-combinatorics.fibers-of-maps public open import univalent-combinatorics.finite-choice public -open import univalent-combinatorics.finite-presentations public open import univalent-combinatorics.finite-types public open import univalent-combinatorics.finitely-many-connected-components public open import univalent-combinatorics.finitely-presented-types public @@ -106,6 +106,10 @@ open import univalent-combinatorics.standard-finite-trees public open import univalent-combinatorics.standard-finite-types public open import univalent-combinatorics.steiner-systems public open import univalent-combinatorics.steiner-triple-systems public +open import univalent-combinatorics.subcounting public +open import univalent-combinatorics.subfinite-indexing public +open import univalent-combinatorics.subfinite-types public +open import univalent-combinatorics.subfinitely-indexed-types public open import univalent-combinatorics.sums-of-natural-numbers public open import univalent-combinatorics.surjective-maps public open import univalent-combinatorics.symmetric-difference public diff --git a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md index 2dc4eea133..6b06dd1332 100644 --- a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md @@ -17,6 +17,7 @@ open import foundation.decidable-embeddings open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.embeddings +open import foundation.empty-types open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-types @@ -46,67 +47,51 @@ open import univalent-combinatorics.standard-finite-types ```agda abstract - count-decidable-subtype' : - {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) → - (k : ℕ) (e : Fin k ≃ X) → count (type-decidable-subtype P) - count-decidable-subtype' P zero-ℕ e = - count-is-empty - ( is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl ∘ pr1) - count-decidable-subtype' P (succ-ℕ k) e - with is-decidable-decidable-subtype P (map-equiv e (inr star)) + count-decidable-subtype-Fin : + {l : Level} (k : ℕ) → + (P : decidable-subtype l (Fin k)) → count (type-decidable-subtype P) + count-decidable-subtype-Fin 0 P = count-is-empty pr1 + count-decidable-subtype-Fin (succ-ℕ k) P + with is-decidable-decidable-subtype P (inr star) ... | inl p = - count-equiv - ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv)) - ( count-equiv' - ( right-distributive-Σ-coproduct - ( Fin k) - ( unit) - ( λ x → is-in-decidable-subtype P (map-equiv e x))) - ( pair - ( succ-ℕ - ( number-of-elements-count - ( count-decidable-subtype' - ( λ x → P (map-equiv e (inl x))) - ( k) - ( id-equiv)))) - ( equiv-coproduct - ( equiv-count - ( count-decidable-subtype' - ( λ x → P (map-equiv e (inl x))) - ( k) - ( id-equiv))) - ( equiv-is-contr - ( is-contr-unit) - ( is-contr-Σ - ( is-contr-unit) - ( star) - ( is-proof-irrelevant-is-prop - ( is-prop-is-in-decidable-subtype P - ( map-equiv e (inr star))) - ( p))))))) + count-equiv' + ( right-distributive-Σ-coproduct + ( Fin k) + ( unit) + ( is-in-decidable-subtype P)) + ( pair + ( succ-ℕ + ( number-of-elements-count (count-decidable-subtype-Fin k (P ∘ inl)))) + ( equiv-coproduct + ( equiv-count (count-decidable-subtype-Fin k (P ∘ inl))) + ( equiv-is-contr + ( is-contr-unit) + ( is-contr-Σ-unit + ( is-proof-irrelevant-is-in-decidable-subtype P (inr star) p))))) ... | inr f = - count-equiv - ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv)) + count-equiv' + ( right-distributive-Σ-coproduct + ( Fin k) + ( unit) + ( is-in-decidable-subtype P)) ( count-equiv' - ( right-distributive-Σ-coproduct - ( Fin k) - ( unit) - ( λ x → is-in-decidable-subtype P (map-equiv e x))) - ( count-equiv' - ( right-unit-law-coproduct-is-empty - ( Σ ( Fin k) - ( λ x → is-in-decidable-subtype P (map-equiv e (inl x)))) - ( Σ ( unit) - ( λ x → is-in-decidable-subtype P (map-equiv e (inr x)))) - ( λ where (star , p) → f p)) - ( count-decidable-subtype' - ( λ x → P (map-equiv e (inl x))) - ( k) - ( id-equiv)))) + ( right-unit-law-coproduct-is-empty + ( Σ (Fin k) (is-in-decidable-subtype P ∘ inl)) + ( Σ unit (is-in-decidable-subtype P ∘ inr)) + ( λ (* , p) → f p)) + ( count-decidable-subtype-Fin k (P ∘ inl))) + +count-decidable-subtype' : + {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) → + (k : ℕ) (e : Fin k ≃ X) → count (type-decidable-subtype P) +count-decidable-subtype' P k e = + count-equiv + ( equiv-Σ-equiv-base (is-in-decidable-subtype P) e) + ( count-decidable-subtype-Fin k (P ∘ map-equiv e)) count-decidable-subtype : {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) → - (count X) → count (type-decidable-subtype P) + count X → count (type-decidable-subtype P) count-decidable-subtype P e = count-decidable-subtype' P ( number-of-elements-count e) diff --git a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md index ce45d38d86..398a1fe35d 100644 --- a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md @@ -60,25 +60,21 @@ i.e., if the elements in the complement of `B` can be counted. ### `Σ A B` can be counted if `A` can be counted and if each `B x` can be counted ```agda +count-Σ-Fin : + {l : Level} (k : ℕ) {B : Fin k → UU l} → + ((x : Fin k) → count (B x)) → count (Σ (Fin k) B) +count-Σ-Fin 0 f = count-is-empty pr1 +count-Σ-Fin (succ-ℕ k) {B} f = + count-equiv' + ( ( equiv-coproduct id-equiv (left-unit-law-Σ (B ∘ inr))) ∘e + ( right-distributive-Σ-coproduct (Fin k) unit B)) + ( count-coproduct (count-Σ-Fin k (f ∘ inl)) (f (inr star))) + count-Σ' : - {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → - (k : ℕ) (e : Fin k ≃ A) → ((x : A) → count (B x)) → count (Σ A B) -count-Σ' zero-ℕ e f = - count-is-empty - ( λ x → - is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl (pr1 x)) -count-Σ' {l1} {l2} {A} {B} (succ-ℕ k) e f = - count-equiv - ( ( equiv-Σ-equiv-base B e) ∘e - ( ( inv-equiv - ( right-distributive-Σ-coproduct (Fin k) unit (B ∘ map-equiv e))) ∘e - ( equiv-coproduct - ( id-equiv) - ( inv-equiv - ( left-unit-law-Σ (B ∘ (map-equiv e ∘ inr))))))) - ( count-coproduct - ( count-Σ' k id-equiv (λ x → f (map-equiv e (inl x)))) - ( f (map-equiv e (inr star)))) + {l1 l2 : Level} (k : ℕ) {A : UU l1} {B : A → UU l2} → + (e : Fin k ≃ A) → ((x : A) → count (B x)) → count (Σ A B) +count-Σ' k {B = B} e f = + count-equiv (equiv-Σ-equiv-base B e) (count-Σ-Fin k (f ∘ map-equiv e)) abstract equiv-count-Σ' : diff --git a/src/univalent-combinatorics/counting-fibers-of-maps.lagda.md b/src/univalent-combinatorics/counting-fibers-of-maps.lagda.md deleted file mode 100644 index 7bf347e7c7..0000000000 --- a/src/univalent-combinatorics/counting-fibers-of-maps.lagda.md +++ /dev/null @@ -1,13 +0,0 @@ -# Counting the elements of the fiber of a map - -```agda -module univalent-combinatorics.counting-fibers-of-maps where -``` - -
Imports - -```agda - -``` - -
diff --git a/src/univalent-combinatorics/counting.lagda.md b/src/univalent-combinatorics/counting.lagda.md index b9c4fa6d19..3b9e471efe 100644 --- a/src/univalent-combinatorics/counting.lagda.md +++ b/src/univalent-combinatorics/counting.lagda.md @@ -113,38 +113,38 @@ module _ pr2 (count-equiv' e f) = equiv-count-equiv' e f count-is-equiv : {f : X → Y} → is-equiv f → count X → count Y - count-is-equiv H = count-equiv (pair _ H) + count-is-equiv H = count-equiv (_ , H) count-is-equiv' : {f : X → Y} → is-equiv f → count Y → count X - count-is-equiv' H = count-equiv' (pair _ H) + count-is-equiv' H = count-equiv' (_ , H) ``` -### A type as 0 elements if and only if it is empty +### A type has 0 elements if and only if it is empty ```agda abstract is-empty-is-zero-number-of-elements-count : {l : Level} {X : UU l} (e : count X) → is-zero-ℕ (number-of-elements-count e) → is-empty X - is-empty-is-zero-number-of-elements-count (pair .zero-ℕ e) refl x = + is-empty-is-zero-number-of-elements-count (.0 , e) refl x = map-inv-equiv e x abstract is-zero-number-of-elements-count-is-empty : {l : Level} {X : UU l} (e : count X) → is-empty X → is-zero-ℕ (number-of-elements-count e) - is-zero-number-of-elements-count-is-empty (pair zero-ℕ e) H = refl - is-zero-number-of-elements-count-is-empty (pair (succ-ℕ k) e) H = + is-zero-number-of-elements-count-is-empty (0 , e) H = refl + is-zero-number-of-elements-count-is-empty (succ-ℕ k , e) H = ex-falso (H (map-equiv e (zero-Fin k))) count-is-empty : {l : Level} {X : UU l} → is-empty X → count X -pr1 (count-is-empty H) = zero-ℕ -pr2 (count-is-empty H) = inv-equiv (pair H (is-equiv-is-empty' H)) +pr1 (count-is-empty H) = 0 +pr2 (count-is-empty H) = inv-equiv (H , is-equiv-is-empty' H) count-empty : count empty -count-empty = count-Fin zero-ℕ +count-empty = count-Fin 0 ``` ### A type has 1 element if and only if it is contractible @@ -159,18 +159,18 @@ abstract is-contr-is-one-number-of-elements-count : {l : Level} {X : UU l} (e : count X) → is-one-ℕ (number-of-elements-count e) → is-contr X - is-contr-is-one-number-of-elements-count (pair .(succ-ℕ zero-ℕ) e) refl = + is-contr-is-one-number-of-elements-count (.1 , e) refl = is-contr-equiv' (Fin 1) e is-contr-Fin-1 abstract is-one-number-of-elements-count-is-contr : {l : Level} {X : UU l} (e : count X) → is-contr X → is-one-ℕ (number-of-elements-count e) - is-one-number-of-elements-count-is-contr (pair zero-ℕ e) H = + is-one-number-of-elements-count-is-contr (0 , e) H = ex-falso (map-inv-equiv e (center H)) - is-one-number-of-elements-count-is-contr (pair (succ-ℕ zero-ℕ) e) H = + is-one-number-of-elements-count-is-contr (1 , e) H = refl - is-one-number-of-elements-count-is-contr (pair (succ-ℕ (succ-ℕ k)) e) H = + is-one-number-of-elements-count-is-contr (succ-ℕ (succ-ℕ k) , e) H = ex-falso ( Eq-Fin-eq (succ-ℕ (succ-ℕ k)) ( is-injective-equiv e @@ -187,18 +187,18 @@ count-unit = count-is-contr is-contr-unit ```agda has-decidable-equality-count : {l : Level} {X : UU l} → count X → has-decidable-equality X -has-decidable-equality-count (pair k e) = +has-decidable-equality-count (k , e) = has-decidable-equality-equiv' e (has-decidable-equality-Fin k) ``` -### This with a count are either inhabited or empty +### Types with a count are either inhabited or empty ```agda is-inhabited-or-empty-count : {l1 : Level} {A : UU l1} → count A → is-inhabited-or-empty A -is-inhabited-or-empty-count (pair zero-ℕ e) = - inr (is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl) -is-inhabited-or-empty-count (pair (succ-ℕ k) e) = +is-inhabited-or-empty-count (0 , e) = + inr (is-empty-is-zero-number-of-elements-count (0 , e) refl) +is-inhabited-or-empty-count (succ-ℕ k , e) = inl (unit-trunc-Prop (map-equiv e (zero-Fin k))) ``` @@ -207,11 +207,11 @@ is-inhabited-or-empty-count (pair (succ-ℕ k) e) = ```agda count-type-trunc-Prop : {l1 : Level} {A : UU l1} → count A → count (type-trunc-Prop A) -count-type-trunc-Prop (pair zero-ℕ e) = +count-type-trunc-Prop (0 , e) = count-is-empty ( is-empty-type-trunc-Prop - ( is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl)) -count-type-trunc-Prop (pair (succ-ℕ k) e) = + ( is-empty-is-zero-number-of-elements-count (0 , e) refl)) +count-type-trunc-Prop (succ-ℕ k , e) = count-is-contr ( is-proof-irrelevant-is-prop ( is-prop-type-trunc-Prop) diff --git a/src/univalent-combinatorics/decidable-subtypes.lagda.md b/src/univalent-combinatorics/decidable-subtypes.lagda.md index d7b83a688c..bb3efd1f1f 100644 --- a/src/univalent-combinatorics/decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/decidable-subtypes.lagda.md @@ -225,3 +225,7 @@ is-decidable-subtype-is-finite-has-decidable-eq S dec-A fin-S a = ## References {{#bibliography}} + +## See also + +- [Counting the elements of decidable subtypes](univalent-combinatorics.counting-decidable-subtypes.md) diff --git a/src/univalent-combinatorics/dedekind-finite-sets.lagda.md b/src/univalent-combinatorics/dedekind-finite-sets.lagda.md index f3d73ff2db..563c045e91 100644 --- a/src/univalent-combinatorics/dedekind-finite-sets.lagda.md +++ b/src/univalent-combinatorics/dedekind-finite-sets.lagda.md @@ -10,9 +10,13 @@ module univalent-combinatorics.dedekind-finite-sets where open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies open import foundation.propositions open import foundation.sets open import foundation.universe-levels + +open import univalent-combinatorics.dedekind-finite-types ``` @@ -22,21 +26,25 @@ open import foundation.universe-levels {{#concept "Dedekind finite sets" Agda=set-Dedekind-Finite-Set}} are [sets](foundation-core.sets.md) `X` with the [property](foundation-core.propositions.md) that every -[embedding](foundation-core.embeddings.md) `X ↪ X` is an +self-[embedding](foundation-core.embeddings.md) `X ↪ X` is an [equivalence](foundation-core.equivalences.md). -## Definition +## Definitions + +### The predicate of being a Dedekind finite set ```agda is-dedekind-finite-set-Prop : {l : Level} → Set l → Prop l is-dedekind-finite-set-Prop X = - Π-Prop - ( type-Set X → type-Set X) - ( λ f → function-Prop (is-emb f) (is-equiv-Prop f)) + is-dedekind-finite-Prop (type-Set X) is-dedekind-finite-set : {l : Level} → Set l → UU l is-dedekind-finite-set X = type-Prop (is-dedekind-finite-set-Prop X) +``` +### The subuniverse of Dedekind finite sets + +```agda Dedekind-Finite-Set : (l : Level) → UU (lsuc l) Dedekind-Finite-Set l = Σ (Set l) is-dedekind-finite-set diff --git a/src/univalent-combinatorics/dedekind-finite-types.lagda.md b/src/univalent-combinatorics/dedekind-finite-types.lagda.md new file mode 100644 index 0000000000..55bc731ea1 --- /dev/null +++ b/src/univalent-combinatorics/dedekind-finite-types.lagda.md @@ -0,0 +1,167 @@ +# Dedekind finite types + +```agda +module univalent-combinatorics.dedekind-finite-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.homotopies +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.split-surjective-maps +open import foundation.surjective-maps +open import foundation.universe-levels +``` + +
+ +## Idea + +{{#concept "Dedekind finite types" Agda=Dedekind-Finite-Type Agda=is-dedekind-finite}} +are types `X` with the [property](foundation-core.propositions.md) that every +self-[embedding](foundation-core.embeddings.md) `X ↪ X` is an +[equivalence](foundation-core.equivalences.md). + +## Definitions + +### The predicate of being a Dedekind finite type + +```agda +is-dedekind-finite-Prop : {l : Level} → UU l → Prop l +is-dedekind-finite-Prop X = + Π-Prop + ( X → X) + ( λ f → function-Prop (is-emb f) (is-equiv-Prop f)) + +is-dedekind-finite : {l : Level} → UU l → UU l +is-dedekind-finite X = type-Prop (is-dedekind-finite-Prop X) +``` + +### The subuniverse of Dedekind finite types + +```agda +Dedekind-Finite-Type : (l : Level) → UU (lsuc l) +Dedekind-Finite-Type l = Σ (UU l) is-dedekind-finite + +module _ + {l : Level} (X : Dedekind-Finite-Type l) + where + + type-Dedekind-Finite-Type : UU l + type-Dedekind-Finite-Type = pr1 X + + is-dedekind-finite-Dedekind-Finite-Type : + is-dedekind-finite type-Dedekind-Finite-Type + is-dedekind-finite-Dedekind-Finite-Type = pr2 X +``` + +## Properties + +### If two Dedekind finite types mutually embed, they are equivalent + +This can be understood as a constructive +[Cantor–Schröder–Bernstein theorem](foundation.cantor-schroder-bernstein-escardo.md) +for Dedekind finite types. + +**Proof.** Given embeddings `f : X ↪ Y` and `g : Y ↪ X`, we have a commuting +diagram + +```text + g ∘ f + X ------> X + | ∧ | + f | g / | f + | / | + ∨ / ∨ + Y ------> Y. + f ∘ g +``` + +The top and bottom rows are equivalences by Dedekind finiteness, so by the +6-for-2 property of equivalences every edge in this diagram is an equivalence. ∎ + +```agda +module _ + {l1 l2 : Level} + (X : Dedekind-Finite-Type l1) (Y : Dedekind-Finite-Type l2) + (f : type-Dedekind-Finite-Type X ↪ type-Dedekind-Finite-Type Y) + (g : type-Dedekind-Finite-Type Y ↪ type-Dedekind-Finite-Type X) + where + + is-equiv-map-cantor-schröder-bernstein-Dedekind-Finite-Type : + is-equiv (map-emb f) + is-equiv-map-cantor-schröder-bernstein-Dedekind-Finite-Type = + is-equiv-left-is-equiv-top-is-equiv-bottom-square + ( map-emb f) + ( map-emb f) + ( map-emb g) + ( refl-htpy) + ( refl-htpy) + ( is-dedekind-finite-Dedekind-Finite-Type X + ( map-emb g ∘ map-emb f) + ( is-emb-map-comp-emb g f)) + ( is-dedekind-finite-Dedekind-Finite-Type Y + ( map-emb f ∘ map-emb g) + ( is-emb-map-comp-emb f g)) + + cantor-schröder-bernstein-Dedekind-Finite-Type : + type-Dedekind-Finite-Type X ≃ type-Dedekind-Finite-Type Y + cantor-schröder-bernstein-Dedekind-Finite-Type = + ( map-emb f , is-equiv-map-cantor-schröder-bernstein-Dedekind-Finite-Type) +``` + +### If all elements are merely equal, then the type is Dedekind finite + +```agda +is-dedekind-finite-all-elements-merely-equal : + {l : Level} {X : UU l} → ((x y : X) → ║ x ＝ y ║₋₁) → is-dedekind-finite X +is-dedekind-finite-all-elements-merely-equal H f = + is-equiv-is-emb-is-surjective (λ x → map-trunc-Prop (x ,_) (H (f x) x)) +``` + +### Propositions are Dedekind finite + +```agda +is-dedekind-finite-is-prop : + {l : Level} {X : UU l} → is-prop X → is-dedekind-finite X +is-dedekind-finite-is-prop H f is-emb-f = + is-equiv-is-split-surjective-is-injective f + ( is-injective-is-emb is-emb-f) + ( λ x → (x , eq-is-prop H)) +``` + +## Comments + +It seems to be an open problem whether Dedekind finite types are closed under +coproducts or products. {{#cite Sto87}} + +## See also + +- [Dual Dedekind finite types](univalent-combinatorics.dual-dedekind-finite-types.md) +- [Finite types](univalent-combinatorics.finite-types.md) +- [Kuratowski finite sets](univalent-combinatorics.kuratowski-finite-sets.md) +- [Subfinite types](univalent-combinatorics.subfinite-types.md) +- [Subfinitely indexed types](univalent-combinatorics.subfinitely-indexed-types.md) + +## References + +{{#bibliography}} {{#reference Sto87}} + +## External links + +- [`Fin.Dedekind`](https://www.cs.bham.ac.uk/~mhe/TypeTopology/Fin.Dedekind.html) + at TypeTopology +- [finite object#Dedekind finiteness](https://ncatlab.org/nlab/show/finite+object#dedekind_finiteness) +- [finite set](https://ncatlab.org/nlab/show/finite+set) at $n$Lab +- [Dedekind-infinite set](https://en.wikipedia.org/wiki/Dedekind-infinite_set) + at Wikipedia diff --git a/src/univalent-combinatorics/dual-dedekind-finite-types.lagda.md b/src/univalent-combinatorics/dual-dedekind-finite-types.lagda.md new file mode 100644 index 0000000000..697b8d2f31 --- /dev/null +++ b/src/univalent-combinatorics/dual-dedekind-finite-types.lagda.md @@ -0,0 +1,154 @@ +# Dual Dedekind finite types + +```agda +module univalent-combinatorics.dual-dedekind-finite-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.homotopies +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.split-surjective-maps +open import foundation.surjective-maps +open import foundation.universe-levels + +open import synthetic-homotopy-theory.acyclic-maps +``` + +
+ +## Idea + +{{#concept "Dual Dedekind finite types" Agda=is-dual-dedekind-finite Agda=Dual-Dedekind-Finite-Type}} +are types `X` with the [property](foundation-core.propositions.md) that every +[acyclic](synthetic-homotopy-theory.acyclic-maps.md) endomap `X ↠ X` is an +[equivalence](foundation-core.equivalences.md). + +Recall that a +[Dedekind finite type](univalent-combinatorics.dedekind-finite-types.md) is a +type such that every self-[embedding](foundation-core.embeddings.md) is an +equivalence. The dual Dedekind finiteness condition is formally dual to the +Dedekind finiteness condition, since acyclic maps are precisely the +[epimorphisms](foundation.epimorphisms.md) in the +[∞-category of types](foundation.wild-category-of-types.md), while embeddings +are precisely the [monomorphisms](foundation.monomorphisms.md). + +## Definitions + +### The predicate of being a dual Dedekind finite type + +```agda +is-dual-dedekind-finite-Prop : {l : Level} → UU l → Prop l +is-dual-dedekind-finite-Prop X = + Π-Prop + ( X → X) + ( λ f → function-Prop (is-acyclic-map f) (is-equiv-Prop f)) + +is-dual-dedekind-finite : {l : Level} → UU l → UU l +is-dual-dedekind-finite X = type-Prop (is-dual-dedekind-finite-Prop X) + +is-prop-is-dual-dedekind-finite : + {l : Level} {X : UU l} → is-prop (is-dual-dedekind-finite X) +is-prop-is-dual-dedekind-finite {X = X} = + is-prop-type-Prop (is-dual-dedekind-finite-Prop X) +``` + +### The subuniverse of dual Dedekind finite types + +```agda +Dual-Dedekind-Finite-Type : (l : Level) → UU (lsuc l) +Dual-Dedekind-Finite-Type l = Σ (UU l) is-dual-dedekind-finite + +module _ + {l : Level} (X : Dual-Dedekind-Finite-Type l) + where + + type-Dual-Dedekind-Finite-Type : UU l + type-Dual-Dedekind-Finite-Type = pr1 X + + is-dual-dedekind-finite-Dual-Dedekind-Finite-Type : + is-dual-dedekind-finite type-Dual-Dedekind-Finite-Type + is-dual-dedekind-finite-Dual-Dedekind-Finite-Type = pr2 X +``` + +## Properties + +### If two dual Dedekind finite types mutually project, they are equivalent + +This can be understood as a constructive dual +[Cantor–Schröder–Bernstein theorem](foundation.cantor-schroder-bernstein-escardo.md) +for dual Dedekind finite types. + +**Proof.** Given epimorphisms `f : X ↠ Y` and `g : Y ↠ X`, we have a commuting +diagram + +```text + g ∘ f + X ------> X + | ∧ | + f | g / | f + | / | + ∨ / ∨ + Y ------> Y. + f ∘ g +``` + +The top and bottom rows are equivalences by dual Dedekind finiteness, so by the +6-for-2 property of equivalences every edge in this diagram is an equivalence. ∎ + +```agda +module _ + {l1 l2 : Level} + (X : Dual-Dedekind-Finite-Type l1) + (Y : Dual-Dedekind-Finite-Type l2) + (f : + acyclic-map + ( type-Dual-Dedekind-Finite-Type X) + ( type-Dual-Dedekind-Finite-Type Y)) + (g : + acyclic-map + ( type-Dual-Dedekind-Finite-Type Y) + ( type-Dual-Dedekind-Finite-Type X)) + where + + is-equiv-map-cantor-schröder-bernstein-Dual-Dedekind-Finite-Type : + is-equiv (map-acyclic-map f) + is-equiv-map-cantor-schröder-bernstein-Dual-Dedekind-Finite-Type = + is-equiv-left-is-equiv-top-is-equiv-bottom-square + ( map-acyclic-map f) + ( map-acyclic-map f) + ( map-acyclic-map g) + ( refl-htpy) + ( refl-htpy) + ( is-dual-dedekind-finite-Dual-Dedekind-Finite-Type X + ( map-acyclic-map g ∘ map-acyclic-map f) + ( is-acyclic-map-comp-acyclic-map g f)) + ( is-dual-dedekind-finite-Dual-Dedekind-Finite-Type Y + ( map-acyclic-map f ∘ map-acyclic-map g) + ( is-acyclic-map-comp-acyclic-map f g)) + + cantor-schröder-bernstein-Dual-Dedekind-Finite-Type : + type-Dual-Dedekind-Finite-Type X ≃ type-Dual-Dedekind-Finite-Type Y + cantor-schröder-bernstein-Dual-Dedekind-Finite-Type = + ( map-acyclic-map f , + is-equiv-map-cantor-schröder-bernstein-Dual-Dedekind-Finite-Type) +``` + +## See also + +- [Dedekind finite types](univalent-combinatorics.dedekind-finite-types.md) + +## External links + +- [Dedekind-infinite set](https://en.wikipedia.org/wiki/Dedekind-infinite_set) + at Wikipedia diff --git a/src/univalent-combinatorics/finite-choice.lagda.md b/src/univalent-combinatorics/finite-choice.lagda.md index 9446a425cb..43f0971a20 100644 --- a/src/univalent-combinatorics/finite-choice.lagda.md +++ b/src/univalent-combinatorics/finite-choice.lagda.md @@ -14,6 +14,7 @@ open import foundation.coproduct-types open import foundation.decidable-embeddings open import foundation.dependent-pair-types open import foundation.dependent-universal-property-equivalences +open import foundation.double-negation open import foundation.empty-types open import foundation.equivalences open import foundation.fiber-inclusions @@ -23,6 +24,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-propositional-truncation open import foundation.hilberts-epsilon-operators open import foundation.identity-types +open import foundation.inhabited-types open import foundation.propositional-truncations open import foundation.sets open import foundation.unit-type @@ -40,17 +42,20 @@ open import univalent-combinatorics.standard-finite-types ## Idea -Propositional truncations distributes over finite products. +[Propositional truncations](foundation.propositional-truncations.md) distributes +over finite products. ## Theorems +### Finite choice + ```agda abstract finite-choice-Fin : {l1 : Level} (k : ℕ) {Y : Fin k → UU l1} → - ((x : Fin k) → type-trunc-Prop (Y x)) → type-trunc-Prop ((x : Fin k) → Y x) - finite-choice-Fin {l1} zero-ℕ {Y} H = unit-trunc-Prop ind-empty - finite-choice-Fin {l1} (succ-ℕ k) {Y} H = + ((x : Fin k) → is-inhabited (Y x)) → is-inhabited ((x : Fin k) → Y x) + finite-choice-Fin 0 H = unit-trunc-Prop ind-empty + finite-choice-Fin (succ-ℕ k) {Y} H = map-inv-equiv-trunc-Prop ( equiv-dependent-universal-property-coproduct Y) ( map-inv-distributive-trunc-product-Prop @@ -60,35 +65,39 @@ abstract ( equiv-dependent-universal-property-unit (Y ∘ inr)) ( H (inr star))))) -abstract - finite-choice-count : - {l1 l2 : Level} {X : UU l1} {Y : X → UU l2} → count X → - ((x : X) → type-trunc-Prop (Y x)) → type-trunc-Prop ((x : X) → Y x) - finite-choice-count {l1} {l2} {X} {Y} (pair k e) H = - map-inv-equiv-trunc-Prop - ( equiv-precomp-Π e Y) - ( finite-choice-Fin k (λ x → H (map-equiv e x))) - -abstract - finite-choice : - {l1 l2 : Level} {X : UU l1} {Y : X → UU l2} → is-finite X → - ((x : X) → type-trunc-Prop (Y x)) → type-trunc-Prop ((x : X) → Y x) - finite-choice {l1} {l2} {X} {Y} is-finite-X H = - apply-universal-property-trunc-Prop is-finite-X - ( trunc-Prop ((x : X) → Y x)) - ( λ e → finite-choice-count e H) +module _ + {l1 l2 : Level} {X : UU l1} {Y : X → UU l2} + where + + abstract + finite-choice-count : + count X → + ((x : X) → is-inhabited (Y x)) → is-inhabited ((x : X) → Y x) + finite-choice-count (k , e) H = + map-inv-equiv-trunc-Prop + ( equiv-precomp-Π e Y) + ( finite-choice-Fin k (H ∘ map-equiv e)) + + abstract + finite-choice : + is-finite X → + ((x : X) → is-inhabited (Y x)) → is-inhabited ((x : X) → Y x) + finite-choice is-finite-X H = + apply-universal-property-trunc-Prop is-finite-X + ( trunc-Prop ((x : X) → Y x)) + ( λ e → finite-choice-count e H) ``` ```agda abstract ε-operator-count : {l : Level} {A : UU l} → count A → ε-operator-Hilbert A - ε-operator-count (pair zero-ℕ e) t = + ε-operator-count (0 , e) t = ex-falso ( is-empty-type-trunc-Prop - ( is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl) + ( is-empty-is-zero-number-of-elements-count (0 , e) refl) ( t)) - ε-operator-count (pair (succ-ℕ k) e) t = map-equiv e (zero-Fin k) + ε-operator-count (succ-ℕ k , e) t = map-equiv e (zero-Fin k) abstract ε-operator-decidable-subtype-count : @@ -99,7 +108,7 @@ abstract ( equiv-Σ-equiv-base (is-in-decidable-subtype P) (equiv-count e)) ( ε-operator-decidable-subtype-Fin ( number-of-elements-count e) - ( λ x → P (map-equiv-count e x))) + ( P ∘ map-equiv-count e)) ``` ```agda @@ -118,25 +127,69 @@ abstract ``` ```agda -abstract - choice-count-Σ-is-finite-fiber : - {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → - is-set A → count (Σ A B) → ((x : A) → is-finite (B x)) → - ((x : A) → type-trunc-Prop (B x)) → (x : A) → B x - choice-count-Σ-is-finite-fiber {l1} {l2} {A} {B} K e g H x = - ε-operator-count - ( count-domain-emb-is-finite-domain-emb e - ( fiber-inclusion-emb (pair A K) B x) - ( g x)) - ( H x) +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + abstract + choice-count-Σ-is-finite-fiber : + is-set A → count (Σ A B) → ((x : A) → is-finite (B x)) → + ((x : A) → is-inhabited (B x)) → (x : A) → B x + choice-count-Σ-is-finite-fiber K e g H x = + ε-operator-count + ( count-domain-emb-is-finite-domain-emb e + ( fiber-inclusion-emb (A , K) B x) + ( g x)) + ( H x) + + abstract + choice-is-finite-Σ-is-finite-fiber : + is-set A → is-finite (Σ A B) → ((x : A) → is-finite (B x)) → + ((x : A) → is-inhabited (B x)) → is-inhabited ((x : A) → B x) + choice-is-finite-Σ-is-finite-fiber K f g H = + apply-universal-property-trunc-Prop f + ( trunc-Prop ((x : A) → B x)) + ( λ e → unit-trunc-Prop (choice-count-Σ-is-finite-fiber K e g H)) +``` + +### Finite choice with respect to double negation +```agda abstract - choice-is-finite-Σ-is-finite-fiber : - {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → - is-set A → is-finite (Σ A B) → ((x : A) → is-finite (B x)) → - ((x : A) → type-trunc-Prop (B x)) → type-trunc-Prop ((x : A) → B x) - choice-is-finite-Σ-is-finite-fiber {l1} {l2} {A} {B} K f g H = - apply-universal-property-trunc-Prop f - ( trunc-Prop ((x : A) → B x)) - ( λ e → unit-trunc-Prop (choice-count-Σ-is-finite-fiber K e g H)) + finite-double-negation-choice-Fin : + {l1 : Level} (k : ℕ) {Y : Fin k → UU l1} → + ((x : Fin k) → ¬¬ (Y x)) → ¬¬ ((x : Fin k) → Y x) + finite-double-negation-choice-Fin 0 H = intro-double-negation ind-empty + finite-double-negation-choice-Fin (succ-ℕ k) {Y} H = + map-double-negation + ( λ p → ind-coproduct Y (pr1 p) (pr2 p)) + ( map-inv-distributive-double-negation-product + ( finite-double-negation-choice-Fin k (H ∘ inl) , + map-double-negation ind-unit (H (inr star)))) + +module _ + {l1 l2 : Level} {X : UU l1} {Y : X → UU l2} + where + + abstract + finite-double-negation-choice-count : + count X → ((x : X) → ¬¬ (Y x)) → ¬¬ ((x : X) → Y x) + finite-double-negation-choice-count (k , e) H = + map-double-negation + ( map-inv-equiv (equiv-precomp-Π e Y)) + ( finite-double-negation-choice-Fin k (H ∘ map-equiv e)) + + abstract + finite-double-negation-choice-double-negation-count : + ¬¬ count X → ((x : X) → ¬¬ (Y x)) → ¬¬ ((x : X) → Y x) + finite-double-negation-choice-double-negation-count nnc H nf = + nnc (λ c → finite-double-negation-choice-count c H nf) + + abstract + finite-double-negation-choice : + is-finite X → ((x : X) → ¬¬ (Y x)) → ¬¬ ((x : X) → Y x) + finite-double-negation-choice is-finite-X H = + apply-universal-property-trunc-Prop is-finite-X + ( double-negation-type-Prop ((x : X) → Y x)) + ( λ e → finite-double-negation-choice-count e H) ``` diff --git a/src/univalent-combinatorics/finite-presentations.lagda.md b/src/univalent-combinatorics/finite-presentations.lagda.md deleted file mode 100644 index a072941ed2..0000000000 --- a/src/univalent-combinatorics/finite-presentations.lagda.md +++ /dev/null @@ -1,24 +0,0 @@ -# Finite presentations of types - -```agda -module univalent-combinatorics.finite-presentations where -``` - -
Imports - -```agda - -``` - -
- -## Idea - -Finitely presented types are types A equipped with a map f : Fin k → A such that -the composite - -```text - Fin k → A → type-trunc-Set A -``` - -is an equivalence. diff --git a/src/univalent-combinatorics/finitely-presented-types.lagda.md b/src/univalent-combinatorics/finitely-presented-types.lagda.md index 6cc22a250a..7ac1ef35ab 100644 --- a/src/univalent-combinatorics/finitely-presented-types.lagda.md +++ b/src/univalent-combinatorics/finitely-presented-types.lagda.md @@ -30,20 +30,20 @@ open import univalent-combinatorics.standard-finite-types ## Idea -A type is said to be finitely presented if it is presented by a standard finite -type. +A type is {{#concept "finitely presented" Agda=is-finitely-presented}} if it is +[presented](foundation.set-presented-types.md) by a +[standard finite type](univalent-combinatorics.standard-finite-types.md). -## Definition +## Definitions ### To have a presentation of cardinality `k` ```agda -has-presentation-of-cardinality-Prop : - {l1 : Level} (k : ℕ) (A : UU l1) → Prop l1 +has-presentation-of-cardinality-Prop : {l : Level} → ℕ → UU l → Prop l has-presentation-of-cardinality-Prop k A = - has-set-presentation-Prop (Fin-Set k) A + is-set-presentation-Prop A (Fin-Set k) -has-presentation-of-cardinality : {l1 : Level} (k : ℕ) (A : UU l1) → UU l1 +has-presentation-of-cardinality : {l : Level} → ℕ → UU l → UU l has-presentation-of-cardinality k A = type-Prop (has-presentation-of-cardinality-Prop k A) ``` @@ -51,7 +51,7 @@ has-presentation-of-cardinality k A = ### Finitely presented types ```agda -is-finitely-presented : {l1 : Level} → UU l1 → UU l1 +is-finitely-presented : {l : Level} → UU l → UU l is-finitely-presented A = Σ ℕ (λ k → has-presentation-of-cardinality k A) ``` @@ -62,7 +62,8 @@ is-finitely-presented A = ```agda has-presentation-of-cardinality-has-cardinality-connected-components : - {l : Level} (k : ℕ) {A : UU l} → has-cardinality-connected-components k A → + {l : Level} (k : ℕ) {A : UU l} → + has-cardinality-connected-components k A → has-presentation-of-cardinality k A has-presentation-of-cardinality-has-cardinality-connected-components k {A} H = apply-universal-property-trunc-Prop H @@ -97,26 +98,31 @@ has-cardinality-connected-components-has-presentation-of-cardinality k {A} H = ### To be finitely presented is a property +In other words, the cardinalty of a finite presentation is unique. + ```agda -all-elements-equal-is-finitely-presented : - {l1 : Level} {A : UU l1} → all-elements-equal (is-finitely-presented A) -all-elements-equal-is-finitely-presented {l1} {A} (pair k K) (pair l L) = - eq-type-subtype - ( λ n → has-set-presentation-Prop (Fin-Set n) A) - ( eq-cardinality - ( has-cardinality-connected-components-has-presentation-of-cardinality - ( k) - ( K)) - ( has-cardinality-connected-components-has-presentation-of-cardinality - ( l) - ( L))) - -is-prop-is-finitely-presented : - {l1 : Level} {A : UU l1} → is-prop (is-finitely-presented A) -is-prop-is-finitely-presented = - is-prop-all-elements-equal all-elements-equal-is-finitely-presented +module _ + {l : Level} {A : UU l} + where + + all-elements-equal-is-finitely-presented : + all-elements-equal (is-finitely-presented A) + all-elements-equal-is-finitely-presented (k , K) (l , L) = + eq-type-subtype + ( λ n → is-set-presentation-Prop A (Fin-Set n)) + ( eq-cardinality + ( has-cardinality-connected-components-has-presentation-of-cardinality + ( k) + ( K)) + ( has-cardinality-connected-components-has-presentation-of-cardinality + ( l) + ( L))) + + is-prop-is-finitely-presented : is-prop (is-finitely-presented A) + is-prop-is-finitely-presented = + is-prop-all-elements-equal all-elements-equal-is-finitely-presented is-finitely-presented-Prop : {l : Level} (A : UU l) → Prop l -pr1 (is-finitely-presented-Prop A) = is-finitely-presented A -pr2 (is-finitely-presented-Prop A) = is-prop-is-finitely-presented +is-finitely-presented-Prop A = + ( is-finitely-presented A , is-prop-is-finitely-presented) ``` diff --git a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md index 7de999ba15..f5308fe47b 100644 --- a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md +++ b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md @@ -31,7 +31,7 @@ open import univalent-combinatorics.standard-finite-types A {{#concept "Kuratowski finite set" agda=Kuratowski-Finite-Set}} is a [set](foundation-core.sets.md) `X` for which there exists a [surjection](foundation.surjective-maps.md) into `X` from a standard finite -type. In other words, the Kuratowski finite set are the +type. In other words, a Kuratowski finite set is a [set-quotient](foundation.set-quotients.md) of a [standard finite type](univalent-combinatorics.standard-finite-types.md). @@ -97,6 +97,10 @@ has-decidable-equality-is-finite-type-Kuratowski-Finite-Set X = - [Finite types](univalent-combinatorics.finite-types.md) - [Dedekind finite sets](univalent-combinatorics.dedekind-finite-sets.md) +- In + [`univalent-combinatorics.surjective-maps`](univalent-combinatorics.surjective-maps.md) + it is shown that if a Kuratowski finite set has decidable equality then it is + finite. ## External links diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md index 78df169e8b..3c54d86fa2 100644 --- a/src/univalent-combinatorics/pigeonhole-principle.lagda.md +++ b/src/univalent-combinatorics/pigeonhole-principle.lagda.md @@ -21,6 +21,7 @@ open import foundation.identity-types open import foundation.injective-maps open import foundation.negated-equality open import foundation.negation +open import foundation.noninjective-maps open import foundation.pairs-of-distinct-elements open import foundation.propositional-truncations open import foundation.propositions @@ -40,9 +41,11 @@ open import univalent-combinatorics.standard-finite-types ## Idea -If `f : X → Y` is an injective map between finite types `X` and `Y` with `k` and -`l` elements, then `k ≤ l`. Conversely, if `l < k`, then no map `f : X → Y` is -injective. +If `f : X → Y` is an [injective map](foundation-core.injective-maps.md) between +[finite types](univalent-combinatorics.finite-types.md) `X` and `Y` with `k` and +`l` elements, then `k ≤ l`. Conversely, if `l < k`, then every map `f : X → Y` +[repeats a value](foundation.repetitions-of-values.md), and hence is +[noninjective](foundation.noninjective-maps.md). ## Theorems @@ -53,14 +56,14 @@ injective. ```agda leq-emb-Fin : (k l : ℕ) → Fin k ↪ Fin l → k ≤-ℕ l -leq-emb-Fin zero-ℕ zero-ℕ f = refl-leq-ℕ zero-ℕ -leq-emb-Fin (succ-ℕ k) zero-ℕ f = ex-falso (map-emb f (inr star)) -leq-emb-Fin zero-ℕ (succ-ℕ l) f = leq-zero-ℕ (succ-ℕ l) +leq-emb-Fin 0 0 f = refl-leq-ℕ 0 +leq-emb-Fin (succ-ℕ k) 0 f = map-emb f (inr star) +leq-emb-Fin 0 (succ-ℕ l) f = leq-zero-ℕ (succ-ℕ l) leq-emb-Fin (succ-ℕ k) (succ-ℕ l) f = leq-emb-Fin k l (reduce-emb-Fin k l f) leq-is-emb-Fin : (k l : ℕ) {f : Fin k → Fin l} → is-emb f → k ≤-ℕ l -leq-is-emb-Fin k l {f = f} H = leq-emb-Fin k l (pair f H) +leq-is-emb-Fin k l {f = f} H = leq-emb-Fin k l (f , H) ``` #### Given an injective map `Fin k → Fin l`, it follows that `k ≤ l` @@ -76,7 +79,7 @@ leq-is-injective-Fin k l H = ```agda is-not-emb-le-Fin : - (k l : ℕ) (f : Fin k → Fin l) → le-ℕ l k → ¬ (is-emb f) + (k l : ℕ) (f : Fin k → Fin l) → l <-ℕ k → ¬ (is-emb f) is-not-emb-le-Fin k l f p = map-neg (leq-is-emb-Fin k l) (contradiction-le-ℕ l k p) ``` @@ -85,7 +88,7 @@ is-not-emb-le-Fin k l f p = ```agda is-not-injective-le-Fin : - (k l : ℕ) (f : Fin k → Fin l) → le-ℕ l k → is-not-injective f + (k l : ℕ) (f : Fin k → Fin l) → l <-ℕ k → is-not-injective f is-not-injective-le-Fin k l f p = map-neg (is-emb-is-injective (is-set-Fin l)) (is-not-emb-le-Fin k l f p) ``` @@ -114,7 +117,7 @@ no-embedding-ℕ-Fin k e = ```agda module _ - (k l : ℕ) (f : Fin k → Fin l) (p : le-ℕ l k) + (k l : ℕ) (f : Fin k → Fin l) (p : l <-ℕ k) where repetition-of-values-le-Fin : repetition-of-values f @@ -150,10 +153,18 @@ module _ is-repetition-of-values-repetition-of-values f repetition-of-values-le-Fin + is-noninjective-le-Fin : is-noninjective f + is-noninjective-le-Fin = unit-trunc-Prop repetition-of-values-le-Fin + repetition-of-values-Fin-succ-to-Fin : (k : ℕ) (f : Fin (succ-ℕ k) → Fin k) → repetition-of-values f repetition-of-values-Fin-succ-to-Fin k f = repetition-of-values-le-Fin (succ-ℕ k) k f (succ-le-ℕ k) + +is-noninjective-Fin-succ-to-Fin : + (k : ℕ) (f : Fin (succ-ℕ k) → Fin k) → is-noninjective f +is-noninjective-Fin-succ-to-Fin k f = + unit-trunc-Prop (repetition-of-values-Fin-succ-to-Fin k f) ``` ### The pigeonhole principle for types equipped with a counting @@ -179,8 +190,8 @@ module _ leq-is-emb-count : {f : A → B} → is-emb f → - (number-of-elements-count eA) ≤-ℕ (number-of-elements-count eB) - leq-is-emb-count {f} H = leq-emb-count (pair f H) + number-of-elements-count eA ≤-ℕ number-of-elements-count eB + leq-is-emb-count {f} H = leq-emb-count (f , H) ``` #### If `f : A → B` is an injective map between types equipped with a counting, then the number of elements of `A` is less than the number of elements of `B` @@ -188,7 +199,7 @@ module _ ```agda leq-is-injective-count : {f : A → B} → is-injective f → - (number-of-elements-count eA) ≤-ℕ (number-of-elements-count eB) + number-of-elements-count eA ≤-ℕ number-of-elements-count eB leq-is-injective-count H = leq-is-emb-count (is-emb-is-injective (is-set-count eB) H) ``` @@ -198,7 +209,7 @@ module _ ```agda is-not-emb-le-count : (f : A → B) → - le-ℕ (number-of-elements-count eB) (number-of-elements-count eA) → + number-of-elements-count eB <-ℕ number-of-elements-count eA → ¬ (is-emb f) is-not-emb-le-count f p H = is-not-emb-le-Fin @@ -211,7 +222,7 @@ module _ h : Fin (number-of-elements-count eA) ↪ Fin (number-of-elements-count eB) h = comp-emb ( emb-equiv (inv-equiv-count eB)) - ( comp-emb (pair f H) (emb-equiv (equiv-count eA))) + ( comp-emb (f , H) (emb-equiv (equiv-count eA))) ``` #### There is no injective map `A → B` between types equipped with a counting if the number of elements of `B` is strictly less than the number of elements of `A` @@ -219,7 +230,7 @@ module _ ```agda is-not-injective-le-count : (f : A → B) → - le-ℕ (number-of-elements-count eB) (number-of-elements-count eA) → + number-of-elements-count eB <-ℕ number-of-elements-count eA → is-not-injective f is-not-injective-le-count f p H = is-not-emb-le-count f p (is-emb-is-injective (is-set-count eB) H) @@ -229,11 +240,11 @@ module _ ```agda no-embedding-ℕ-count : - {l : Level} {A : UU l} (e : count A) → ¬ (ℕ ↪ A) + {l : Level} {A : UU l} → count A → ¬ (ℕ ↪ A) no-embedding-ℕ-count e f = no-embedding-ℕ-Fin - ( number-of-elements-count e) - ( comp-emb (emb-equiv (inv-equiv-count e)) f) + ( number-of-elements-count e) + ( comp-emb (emb-equiv (inv-equiv-count e)) f) ``` #### For any map `f : A → B` between types equipped with a counting, if `|A| < |B|` then we construct a pair of distinct elements of `A` on which `f` assumes the same value @@ -242,13 +253,13 @@ no-embedding-ℕ-count e f = module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (eA : count A) (eB : count B) (f : A → B) - (p : le-ℕ (number-of-elements-count eB) (number-of-elements-count eA)) + (p : number-of-elements-count eB <-ℕ number-of-elements-count eA) where repetition-of-values-le-count : repetition-of-values f repetition-of-values-le-count = map-equiv-repetition-of-values - ( (map-inv-equiv-count eB ∘ f) ∘ (map-equiv-count eA)) + ( map-inv-equiv-count eB ∘ f ∘ map-equiv-count eA) ( f) ( equiv-count eA) ( equiv-count eB) @@ -301,27 +312,26 @@ module _ ```agda leq-emb-is-finite : (A ↪ B) → - (number-of-elements-is-finite H) ≤-ℕ (number-of-elements-is-finite K) + number-of-elements-is-finite H ≤-ℕ number-of-elements-is-finite K leq-emb-is-finite f = - apply-universal-property-trunc-Prop H P - ( λ eA → - apply-universal-property-trunc-Prop K P - ( λ eB → - concatenate-eq-leq-eq-ℕ - ( inv (compute-number-of-elements-is-finite eA H)) - ( leq-emb-count eA eB f) - ( compute-number-of-elements-is-finite eB K))) - where - P : Prop lzero - P = leq-ℕ-Prop - ( number-of-elements-is-finite H) - ( number-of-elements-is-finite K) + let + open + do-syntax-trunc-Prop + ( leq-ℕ-Prop + ( number-of-elements-is-finite H) + ( number-of-elements-is-finite K)) + in do + eA ← H + eB ← K + concatenate-eq-leq-eq-ℕ + ( inv (compute-number-of-elements-is-finite eA H)) + ( leq-emb-count eA eB f) + ( compute-number-of-elements-is-finite eB K) leq-is-emb-is-finite : {f : A → B} → is-emb f → - (number-of-elements-is-finite H) ≤-ℕ (number-of-elements-is-finite K) - leq-is-emb-is-finite {f} H = - leq-emb-is-finite (pair f H) + number-of-elements-is-finite H ≤-ℕ number-of-elements-is-finite K + leq-is-emb-is-finite {f} H = leq-emb-is-finite (f , H) ``` #### If `A → B` is an injective map between finite types, then `|A| ≤ |B|` @@ -329,7 +339,7 @@ module _ ```agda leq-is-injective-is-finite : {f : A → B} → is-injective f → - (number-of-elements-is-finite H) ≤-ℕ (number-of-elements-is-finite K) + number-of-elements-is-finite H ≤-ℕ number-of-elements-is-finite K leq-is-injective-is-finite I = leq-is-emb-is-finite (is-emb-is-injective (is-set-is-finite K) I) ``` @@ -339,18 +349,19 @@ module _ ```agda is-not-emb-le-is-finite : (f : A → B) → - le-ℕ (number-of-elements-is-finite K) (number-of-elements-is-finite H) → + number-of-elements-is-finite K <-ℕ number-of-elements-is-finite H → ¬ (is-emb f) is-not-emb-le-is-finite f p E = - apply-universal-property-trunc-Prop H empty-Prop - ( λ e → - apply-universal-property-trunc-Prop K empty-Prop - ( λ d → is-not-emb-le-count e d f - ( concatenate-eq-le-eq-ℕ - ( compute-number-of-elements-is-finite d K) - ( p) - ( inv (compute-number-of-elements-is-finite e H))) - ( E))) + let open do-syntax-trunc-Prop empty-Prop + in do + e ← H + d ← K + is-not-emb-le-count e d f + ( concatenate-eq-le-eq-ℕ + ( compute-number-of-elements-is-finite d K) + ( p) + ( inv (compute-number-of-elements-is-finite e H))) + ( E) ``` #### There are no injective maps between finite types `A` and `B` such that `|B| < |A|` @@ -358,7 +369,7 @@ module _ ```agda is-not-injective-le-is-finite : (f : A → B) → - le-ℕ (number-of-elements-is-finite K) (number-of-elements-is-finite H) → + number-of-elements-is-finite K <-ℕ number-of-elements-is-finite H → is-not-injective f is-not-injective-le-is-finite f p I = is-not-emb-le-is-finite f p (is-emb-is-injective (is-set-is-finite K) I) @@ -373,3 +384,7 @@ no-embedding-ℕ-is-finite H f = apply-universal-property-trunc-Prop H empty-Prop ( λ e → no-embedding-ℕ-count e f) ``` + +## See also + +- [Sequences of elements in finite types](univalent-combinatorics.sequences-finite-types.md) diff --git a/src/univalent-combinatorics/quotients-finite-types.lagda.md b/src/univalent-combinatorics/quotients-finite-types.lagda.md index 0566bd152d..e61734b8bf 100644 --- a/src/univalent-combinatorics/quotients-finite-types.lagda.md +++ b/src/univalent-combinatorics/quotients-finite-types.lagda.md @@ -20,8 +20,10 @@ open import univalent-combinatorics.image-of-maps ## Idea -The quotient of a finite type by a decidable equivalence relation is again a -finite type. In this file we set up some infrastructure for such quotients. +The quotient of a [finite type](univalent-combinatorics.finite-types.md) by a +[decidable equivalence relation](foundation.decidable-equivalence-relations.md) +is again a finite type. In this file we set up some infrastructure for such +quotients. ## Definition diff --git a/src/univalent-combinatorics/repetitions-of-values.lagda.md b/src/univalent-combinatorics/repetitions-of-values.lagda.md index f051b846bd..c116d72022 100644 --- a/src/univalent-combinatorics/repetitions-of-values.lagda.md +++ b/src/univalent-combinatorics/repetitions-of-values.lagda.md @@ -18,9 +18,15 @@ open import foundation.identity-types open import foundation.injective-maps open import foundation.negated-equality open import foundation.negation +open import foundation.noninjective-maps +open import foundation.pairs-of-distinct-elements open import foundation.sets +open import univalent-combinatorics.counting +open import univalent-combinatorics.counting-decidable-subtypes +open import univalent-combinatorics.counting-dependent-pair-types open import univalent-combinatorics.decidable-dependent-function-types +open import univalent-combinatorics.decidable-dependent-pair-types open import univalent-combinatorics.decidable-propositions open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.equality-standard-finite-types @@ -31,15 +37,16 @@ open import univalent-combinatorics.standard-finite-types ## Idea -A **repetition of values** of a function `f : A → B` consists of a pair -`a a' : A` such that `a ≠ a'` and `f a ＝ f a'`. +A {{#concept "repetition of values" Disambiguation="of a map of types"}} of a +map `f : A → B` consists of a +[pair of distinct elements](foundation.pairs-of-distinct-elements.md) `x ≠ y` of +`A` that get mapped to the [same](foundation-core.identity-types.md) element in +`B`: `f x ＝ f y`. ## Properties ### If `f : Fin k → Fin l` is not injective, then it has a repetition of values -b - ```agda repetition-of-values-is-not-injective-Fin : (k l : ℕ) (f : Fin k → Fin l) → @@ -83,80 +90,45 @@ repetition-of-values-is-not-injective-Fin k l f N = ( K) ``` -### On the standard finite sets, `is-repetition-of-values f x` is decidable - -```text -is-decidable-is-repetition-of-values-Fin : - {k l : ℕ} (f : Fin k → Fin l) (x : Fin k) → - is-decidable (is-repetition-of-values f x) -is-decidable-is-repetition-of-values-Fin f x = - is-decidable-Σ-Fin - ( λ y → - is-decidable-product - ( is-decidable-neg (has-decidable-equality-Fin x y)) - ( has-decidable-equality-Fin (f x) (f y))) +> We could modify this construction to provide proof that `i < j` rather than +> `i ≠ j`. + +### On the standard finite sets, we can count the number of pairs of distinct elements + +```agda +count-pair-of-distinct-elements-Fin : + (k : ℕ) → count (pair-of-distinct-elements (Fin k)) +count-pair-of-distinct-elements-Fin k = + count-Σ-Fin k + ( λ x → + count-decidable-subtype-Fin k + ( λ y → neg-Decidable-Prop (decidable-Eq-Fin k x y))) ``` ### On the standard finite sets, `is-repeated-value f x` is decidable -```text +```agda is-decidable-is-repeated-value-Fin : (k l : ℕ) (f : Fin k → Fin l) (x : Fin k) → is-decidable (is-repeated-value f x) is-decidable-is-repeated-value-Fin k l f x = - is-decidable-Σ-Fin k - ( λ y → - is-decidable-product - ( is-decidable-neg (has-decidable-equality-Fin k x y)) - ( has-decidable-equality-Fin l (f x) (f y))) + is-decidable-Σ-count + ( count-decidable-subtype-Fin k + ( λ y → neg-Decidable-Prop (decidable-Eq-Fin k x y))) + ( λ (y , p) → has-decidable-equality-Fin l (f x) (f y)) ``` -### The predicate that `f` maps two different elements to the same value - -This remains to be defined. -[#748](https://github.com/UniMath/agda-unimath/issues/748) - ### On the standard finite sets, `has-repetition-of-values f` is decidable -```text +```agda is-decidable-has-repetition-of-values-Fin : - (k l : ℕ) (f : Fin k → Fin l) → is-decidable (has-repetition-of-values f) + (k l : ℕ) (f : Fin k → Fin l) → is-decidable (repetition-of-values f) is-decidable-has-repetition-of-values-Fin k l f = - is-decidable-Σ-Fin k (is-decidable-is-repetition-of-values-Fin k l f) + is-decidable-Σ-count + ( count-pair-of-distinct-elements-Fin k) + ( λ (x , y , _) → has-decidable-equality-Fin l (f x) (f y)) ``` -### If `f` is not injective, then it has a `repetition-of-values` - -```text -is-injective-map-Fin-0-Fin : - {k : ℕ} (f : Fin zero-ℕ → Fin k) → is-injective f -is-injective-map-Fin-0-Fin f {()} - -is-injective-map-Fin-1-Fin : {k : ℕ} (f : Fin 1 → Fin k) → is-injective f -is-injective-map-Fin-1-Fin f {inr star} {inr star} p = refl - -has-repetition-of-values-is-not-injective-Fin : - (k l : ℕ) (f : Fin l → Fin k) → - is-not-injective f → has-repetition-of-values f -has-repetition-of-values-is-not-injective-Fin k zero-ℕ f H = - ex-falso (H (is-injective-map-Fin-0-Fin {k} f)) -has-repetition-of-values-is-not-injective-Fin k (succ-ℕ l) f H with - is-decidable-is-repetition-of-values-Fin (succ-ℕ l) k f (inr star) -... | inl r = pair (inr star) r -... | inr g = - α (has-repetition-of-values-is-not-injective-Fin k l (f ∘ inl) K) - where - K : is-not-injective (f ∘ inl) - K I = H (λ {x} {y} → J x y) - where - J : (x y : Fin (succ-ℕ l)) → Id (f x) (f y) → Id x y - J (inl x) (inl y) p = ap inl (I p) - J (inl x) (inr star) p = - ex-falso (g (triple (inl x) (Eq-Fin-eq (succ-ℕ l)) (inv p))) - J (inr star) (inl y) p = - ex-falso (g (triple (inl y) (Eq-Fin-eq (succ-ℕ l)) p)) - J (inr star) (inr star) p = refl - α : has-repetition-of-values (f ∘ inl) → has-repetition-of-values f - α (pair x (pair y (pair h q))) = - pair (inl x) (pair (inl y) (pair (λ r → h (is-injective-inl r)) q)) -``` +## See also + +- [The pigeonhole principle](univalent-combinatorics.pigeonhole-principle.md) diff --git a/src/univalent-combinatorics/sequences-finite-types.lagda.md b/src/univalent-combinatorics/sequences-finite-types.lagda.md index e9cd8106af..5c6f8ce478 100644 --- a/src/univalent-combinatorics/sequences-finite-types.lagda.md +++ b/src/univalent-combinatorics/sequences-finite-types.lagda.md @@ -44,57 +44,56 @@ sequence of elements in a finite type. ## Properties ```agda -repetition-of-values-sequence-Fin : - (k : ℕ) (f : ℕ → Fin k) → repetition-of-values f -repetition-of-values-sequence-Fin k f = - repetition-of-values-left-factor - ( is-emb-nat-Fin (succ-ℕ k)) - ( repetition-of-values-Fin-succ-to-Fin k (f ∘ nat-Fin (succ-ℕ k))) - -pair-of-distinct-elements-repetition-of-values-sequence-Fin : - (k : ℕ) (f : sequence (Fin k)) → pair-of-distinct-elements ℕ -pair-of-distinct-elements-repetition-of-values-sequence-Fin k f = - pair-of-distinct-elements-repetition-of-values f - ( repetition-of-values-sequence-Fin k f) - -first-repetition-of-values-sequence-Fin : - (k : ℕ) (f : sequence (Fin k)) → ℕ -first-repetition-of-values-sequence-Fin k f = - first-repetition-of-values f (repetition-of-values-sequence-Fin k f) - -second-repetition-of-values-sequence-Fin : - (k : ℕ) (f : sequence (Fin k)) → ℕ -second-repetition-of-values-sequence-Fin k f = - second-repetition-of-values f (repetition-of-values-sequence-Fin k f) - -distinction-repetition-of-values-sequence-Fin : - (k : ℕ) (f : sequence (Fin k)) → - first-repetition-of-values-sequence-Fin k f ≠ - second-repetition-of-values-sequence-Fin k f -distinction-repetition-of-values-sequence-Fin k f = - distinction-repetition-of-values f (repetition-of-values-sequence-Fin k f) - -is-repetition-pair-of-distinct-elements-repetition-of-values-sequence-Fin : - (k : ℕ) (f : sequence (Fin k)) → - is-repetition-of-values f - ( pair-of-distinct-elements-repetition-of-values-sequence-Fin k f) -is-repetition-pair-of-distinct-elements-repetition-of-values-sequence-Fin k f = - is-repetition-of-values-repetition-of-values f - ( repetition-of-values-sequence-Fin k f) - -le-first-repetition-of-values-sequence-Fin : - (k : ℕ) (f : sequence (Fin k)) → - le-ℕ (first-repetition-of-values-sequence-Fin k f) (succ-ℕ k) -le-first-repetition-of-values-sequence-Fin k f = - strict-upper-bound-nat-Fin - ( succ-ℕ k) - ( first-repetition-of-values - ( f ∘ nat-Fin (succ-ℕ k)) - ( repetition-of-values-le-Fin - ( succ-ℕ k) - ( k) +module _ + (k : ℕ) (f : ℕ → Fin k) + where + + repetition-of-values-sequence-Fin : + repetition-of-values f + repetition-of-values-sequence-Fin = + repetition-of-values-left-factor + ( is-emb-nat-Fin (succ-ℕ k)) + ( repetition-of-values-Fin-succ-to-Fin k (f ∘ nat-Fin (succ-ℕ k))) + + pair-of-distinct-elements-repetition-of-values-sequence-Fin : + pair-of-distinct-elements ℕ + pair-of-distinct-elements-repetition-of-values-sequence-Fin = + pair-of-distinct-elements-repetition-of-values f + repetition-of-values-sequence-Fin + + first-repetition-of-values-sequence-Fin : ℕ + first-repetition-of-values-sequence-Fin = + first-repetition-of-values f repetition-of-values-sequence-Fin + + second-repetition-of-values-sequence-Fin : ℕ + second-repetition-of-values-sequence-Fin = + second-repetition-of-values f repetition-of-values-sequence-Fin + + distinction-repetition-of-values-sequence-Fin : + first-repetition-of-values-sequence-Fin ≠ + second-repetition-of-values-sequence-Fin + distinction-repetition-of-values-sequence-Fin = + distinction-repetition-of-values f repetition-of-values-sequence-Fin + + is-repetition-pair-of-distinct-elements-repetition-of-values-sequence-Fin : + is-repetition-of-values f + pair-of-distinct-elements-repetition-of-values-sequence-Fin + is-repetition-pair-of-distinct-elements-repetition-of-values-sequence-Fin = + is-repetition-of-values-repetition-of-values f + repetition-of-values-sequence-Fin + + le-first-repetition-of-values-sequence-Fin : + first-repetition-of-values-sequence-Fin <-ℕ (succ-ℕ k) + le-first-repetition-of-values-sequence-Fin = + strict-upper-bound-nat-Fin + ( succ-ℕ k) + ( first-repetition-of-values ( f ∘ nat-Fin (succ-ℕ k)) - ( succ-le-ℕ k))) + ( repetition-of-values-le-Fin + ( succ-ℕ k) + ( k) + ( f ∘ nat-Fin (succ-ℕ k)) + ( succ-le-ℕ k))) ``` ### Ordered repetitions of values of maps out of the natural numbers diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index 31d90d106c..c9dfc158bc 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -32,6 +32,7 @@ open import foundation.negated-equality open import foundation.negation open import foundation.noncontractible-types open import foundation.preunivalent-type-families +open import foundation.propositions open import foundation.raising-universe-levels open import foundation.retractions open import foundation.sets @@ -147,7 +148,7 @@ map-equiv-Fin-1 : Fin 1 → unit map-equiv-Fin-1 (inr x) = x map-inv-equiv-Fin-1 : unit → Fin 1 -map-inv-equiv-Fin-1 x = inr x +map-inv-equiv-Fin-1 = inr is-section-map-inv-equiv-Fin-1 : ( map-equiv-Fin-1 ∘ map-inv-equiv-Fin-1) ~ id @@ -171,6 +172,12 @@ pr2 equiv-Fin-1 = is-equiv-map-equiv-Fin-1 is-contr-Fin-1 : is-contr (Fin 1) is-contr-Fin-1 = is-contr-equiv unit equiv-Fin-1 is-contr-unit +is-prop-Fin-1 : is-prop (Fin 1) +is-prop-Fin-1 = is-prop-is-contr is-contr-Fin-1 + +Fin-1-Prop : Prop lzero +Fin-1-Prop = (Fin 1 , is-prop-Fin-1) + is-not-contractible-Fin : (k : ℕ) → is-not-one-ℕ k → is-not-contractible (Fin k) is-not-contractible-Fin zero-ℕ f = is-not-contractible-empty diff --git a/src/univalent-combinatorics/subcounting.lagda.md b/src/univalent-combinatorics/subcounting.lagda.md new file mode 100644 index 0000000000..5eedd1dae4 --- /dev/null +++ b/src/univalent-combinatorics/subcounting.lagda.md @@ -0,0 +1,149 @@ +# Subcounting + +```agda +module univalent-combinatorics.subcounting where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.contractible-types +open import foundation.coproduct-types +open import foundation.decidable-equality +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.discrete-types +open import foundation.embeddings +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.homotopies +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.unit-type +open import foundation.universe-levels + +open import univalent-combinatorics.counting +open import univalent-combinatorics.equality-standard-finite-types +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A {{#concept "subcounting" Agda=subcount}} of a type `X` is an +[embedding](foundation-core.embeddings.md) of `X` into a +[standard finite type](univalent-combinatorics.standard-finite-types.md). + +## Definitions + +```agda +subcount : {l : Level} → UU l → UU l +subcount X = Σ ℕ (λ k → X ↪ Fin k) + +module _ + {l : Level} {X : UU l} (e : subcount X) + where + + bound-number-of-elements-subcount : ℕ + bound-number-of-elements-subcount = pr1 e + + emb-subcount : X ↪ Fin bound-number-of-elements-subcount + emb-subcount = pr2 e + + map-subcount : X → Fin bound-number-of-elements-subcount + map-subcount = map-emb emb-subcount + + is-emb-map-subcount : is-emb map-subcount + is-emb-map-subcount = is-emb-map-emb emb-subcount + + is-injective-map-subcount : is-injective map-subcount + is-injective-map-subcount = is-injective-emb emb-subcount + + is-set-has-subcount : is-set X + is-set-has-subcount = + is-set-emb emb-subcount (is-set-Fin bound-number-of-elements-subcount) + + has-decidable-equality-has-subcount : has-decidable-equality X + has-decidable-equality-has-subcount = + has-decidable-equality-emb emb-subcount + ( has-decidable-equality-Fin bound-number-of-elements-subcount) +``` + +## Properties + +### The elements of the standard finite types can be subcounted + +```agda +subcount-Fin : (k : ℕ) → subcount (Fin k) +pr1 (subcount-Fin k) = k +pr2 (subcount-Fin k) = id-emb +``` + +### A counting is a subcounting + +```agda +subcount-count : {l : Level} {X : UU l} → count X → subcount X +subcount-count (n , e) = (n , emb-equiv (inv-equiv e)) +``` + +### Types equipped with subcountings are closed under subtypes + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {Y : UU l2} + where + + abstract + emb-subcount-emb : + (Y ↪ X) → (f : subcount X) → Y ↪ Fin (bound-number-of-elements-subcount f) + emb-subcount-emb e f = comp-emb (emb-subcount f) e + + subcount-emb : (Y ↪ X) → subcount X → subcount Y + pr1 (subcount-emb e f) = bound-number-of-elements-subcount f + pr2 (subcount-emb e f) = emb-subcount-emb e f + + subcount-is-emb : {f : Y → X} → is-emb f → subcount X → subcount Y + subcount-is-emb H = subcount-emb (_ , H) +``` + +### A type has sub-0 elements if and only if it is empty + +```agda +abstract + is-empty-is-zero-bound-number-of-elements-subcount : + {l : Level} {X : UU l} (e : subcount X) → + is-zero-ℕ (bound-number-of-elements-subcount e) → is-empty X + is-empty-is-zero-bound-number-of-elements-subcount (.0 , e) refl = map-emb e +``` + +### If the elements of a type can be subcounted, then the elements of its propositional truncation can be subcounted + +**Proof.** Given a subcounting `X ↪ Fin k`, then, by the functorial action of +propositional truncations, we have an embedding `║X║₋₁ ↪ ║Fin k║₋₁`. By +induction, if `k ≐ 0` then `║Fin k║₋₁ ≃ 0 ≃ Fin 0` and so `║X║₋₁ ↪ Fin 0` is a +subcounting. Otherwise, if `k ≐ j + 1`, then `║Fin k║₋₁ ≃ 1 ≃ Fin 1` and again +`║X║₋₁ ↪ Fin 1` is a subcounting. + +```agda +module _ + {l : Level} {X : UU l} + where + + subcount-trunc-Prop : subcount X → subcount ║ X ║₋₁ + subcount-trunc-Prop (0 , f , is-emb-f) = + ( 0 , + rec-trunc-Prop empty-Prop id ∘ map-trunc-Prop f , + is-emb-is-prop is-prop-type-trunc-Prop is-prop-empty) + subcount-trunc-Prop (succ-ℕ k , f , is-emb-f) = + ( 1 , + rec-trunc-Prop Fin-1-Prop (λ _ → inr star) ∘ map-trunc-Prop f , + is-emb-is-prop is-prop-type-trunc-Prop is-prop-Fin-1) +``` diff --git a/src/univalent-combinatorics/subfinite-indexing.lagda.md b/src/univalent-combinatorics/subfinite-indexing.lagda.md new file mode 100644 index 0000000000..61f7195f03 --- /dev/null +++ b/src/univalent-combinatorics/subfinite-indexing.lagda.md @@ -0,0 +1,442 @@ +# Subfinite indexing + +```agda +module univalent-combinatorics.subfinite-indexing where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.distance-natural-numbers +open import elementary-number-theory.maximum-natural-numbers +open import elementary-number-theory.minimum-natural-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.contractible-types +open import foundation.coproduct-types +open import foundation.decidable-equality +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.discrete-types +open import foundation.embeddings +open import foundation.empty-types +open import foundation.equivalences +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.homotopies +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.iterating-functions +open import foundation.noninjective-maps +open import foundation.propositional-maps +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.repetitions-of-values +open import foundation.retracts-of-types +open import foundation.sets +open import foundation.split-surjective-maps +open import foundation.subtypes +open import foundation.surjective-maps +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels + +open import univalent-combinatorics.counting +open import univalent-combinatorics.equality-standard-finite-types +open import univalent-combinatorics.finite-choice +open import univalent-combinatorics.pigeonhole-principle +open import univalent-combinatorics.standard-finite-types +open import univalent-combinatorics.subcounting +open import univalent-combinatorics.subfinite-types +``` + +
+ +## Idea + +A {{#concept "subfinite indexing" Agda=subfinite-indexing}} of a type `X` is the +data of a type `D` [equipped](foundation.structure.md) with a +[subcounting](univalent-combinatorics.subcounting.md) `D ↪ Fin n` and a +[surjection](foundation.surjective-maps.md) `D ↠ X`. + +## Definitions + +```agda +subfinite-indexing : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +subfinite-indexing l2 X = Σ (UU l2) (λ D → (subcount D) × (D ↠ X)) + +module _ + {l1 l2 : Level} {X : UU l1} (e : subfinite-indexing l2 X) + where + + indexing-type-subfinite-indexing : UU l2 + indexing-type-subfinite-indexing = pr1 e + + subcount-indexing-type-subfinite-indexing : + subcount indexing-type-subfinite-indexing + subcount-indexing-type-subfinite-indexing = pr1 (pr2 e) + + is-set-indexing-type-subfinite-indexing : + is-set indexing-type-subfinite-indexing + is-set-indexing-type-subfinite-indexing = + is-set-has-subcount subcount-indexing-type-subfinite-indexing + + indexing-set-subfinite-indexing : Set l2 + indexing-set-subfinite-indexing = + ( indexing-type-subfinite-indexing , + is-set-indexing-type-subfinite-indexing) + + bound-number-of-elements-subfinite-indexing : ℕ + bound-number-of-elements-subfinite-indexing = + bound-number-of-elements-subcount subcount-indexing-type-subfinite-indexing + + emb-subfinite-indexing : + indexing-type-subfinite-indexing ↪ + Fin bound-number-of-elements-subfinite-indexing + emb-subfinite-indexing = + emb-subcount subcount-indexing-type-subfinite-indexing + + map-emb-subfinite-indexing : + indexing-type-subfinite-indexing → + Fin bound-number-of-elements-subfinite-indexing + map-emb-subfinite-indexing = + map-subcount subcount-indexing-type-subfinite-indexing + + is-emb-map-emb-subfinite-indexing : + is-emb map-emb-subfinite-indexing + is-emb-map-emb-subfinite-indexing = + is-emb-map-subcount subcount-indexing-type-subfinite-indexing + + is-injective-map-emb-subfinite-indexing : + is-injective map-emb-subfinite-indexing + is-injective-map-emb-subfinite-indexing = + is-injective-map-subcount subcount-indexing-type-subfinite-indexing + + projection-subfinite-indexing : + indexing-type-subfinite-indexing ↠ X + projection-subfinite-indexing = pr2 (pr2 e) + + map-projection-subfinite-indexing : + indexing-type-subfinite-indexing → X + map-projection-subfinite-indexing = + map-surjection projection-subfinite-indexing + + is-surjective-map-projection-subfinite-indexing : + is-surjective map-projection-subfinite-indexing + is-surjective-map-projection-subfinite-indexing = + is-surjective-map-surjection projection-subfinite-indexing +``` + +## Properties + +### Types with subcountings have subfinite indexings + +```agda +subfinite-indexing-subcount : + {l : Level} {X : UU l} → subcount X → subfinite-indexing l X +subfinite-indexing-subcount {X = X} e = (X , e , id-surjection) +``` + +### Types equipped with subfinite indexings are closed under surjections + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} + where + + subfinite-indexing-surjection : + X ↠ Y → subfinite-indexing l3 X → subfinite-indexing l3 Y + subfinite-indexing-surjection s (D , e , t) = (D , e , comp-surjection s t) +``` + +### Types equipped with subfinite indexings are closed under retracts + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} + where + + subfinite-indexing-retract-of : + Y retract-of X → subfinite-indexing l3 X → subfinite-indexing l3 Y + subfinite-indexing-retract-of R = + subfinite-indexing-surjection + ( map-retraction-retract R , + is-surjective-has-section (section-retract R)) +``` + +### Types equipped with subfinite indexings are closed under equivalences + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} + where + + subfinite-indexing-equiv : + Y ≃ X → subfinite-indexing l3 X → subfinite-indexing l3 Y + subfinite-indexing-equiv e = + subfinite-indexing-retract-of (retract-equiv e) + + subfinite-indexing-equiv' : + X ≃ Y → subfinite-indexing l3 X → subfinite-indexing l3 Y + subfinite-indexing-equiv' e = + subfinite-indexing-retract-of (retract-inv-equiv e) +``` + +### Types equipped with subfinite indexings are closed under subtypes + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} (P : subtype l2 X) + (f : subfinite-indexing l3 X) + where + + indexing-subtype-subfinite-indexing-subtype : + subtype l2 (indexing-type-subfinite-indexing f) + indexing-subtype-subfinite-indexing-subtype d = + P (map-projection-subfinite-indexing f d) + + indexing-type-subfinite-indexing-subtype : UU (l2 ⊔ l3) + indexing-type-subfinite-indexing-subtype = + type-subtype indexing-subtype-subfinite-indexing-subtype + + bound-number-of-elements-subfinite-indexing-subtype : ℕ + bound-number-of-elements-subfinite-indexing-subtype = + bound-number-of-elements-subfinite-indexing f + + emb-subfinite-indexing-subtype : + indexing-type-subfinite-indexing-subtype ↪ + Fin bound-number-of-elements-subfinite-indexing-subtype + emb-subfinite-indexing-subtype = + comp-emb + ( emb-subfinite-indexing f) + ( emb-subtype indexing-subtype-subfinite-indexing-subtype) + + subcount-subfinite-indexing-subtype : + subcount indexing-type-subfinite-indexing-subtype + subcount-subfinite-indexing-subtype = + ( bound-number-of-elements-subfinite-indexing-subtype , + emb-subfinite-indexing-subtype) + + map-projection-subfinite-indexing-subtype : + indexing-type-subfinite-indexing-subtype → type-subtype P + map-projection-subfinite-indexing-subtype (d , p) = + (map-projection-subfinite-indexing f d , p) + + abstract + is-surjective-map-projection-subfinite-indexing-subtype : + is-surjective map-projection-subfinite-indexing-subtype + is-surjective-map-projection-subfinite-indexing-subtype (x , p) = + map-trunc-Prop + ( λ where (y , refl) → ((y , p) , refl)) + ( is-surjective-map-projection-subfinite-indexing f x) + + projection-subfinite-indexing-subtype : + indexing-type-subfinite-indexing-subtype ↠ type-subtype P + projection-subfinite-indexing-subtype = + ( map-projection-subfinite-indexing-subtype , + is-surjective-map-projection-subfinite-indexing-subtype) + + subfinite-indexing-subtype : subfinite-indexing (l2 ⊔ l3) (type-subtype P) + subfinite-indexing-subtype = + ( indexing-type-subfinite-indexing-subtype , + subcount-subfinite-indexing-subtype , + projection-subfinite-indexing-subtype) +``` + +### Types equipped with subfinite indexings are closed under embeddings + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (e : Y ↪ X) + (f : subfinite-indexing l3 X) + where + + subfinite-indexing-emb : subfinite-indexing (l1 ⊔ l2 ⊔ l3) Y + subfinite-indexing-emb = + subfinite-indexing-equiv' + ( equiv-total-fiber (map-emb e)) + ( subfinite-indexing-subtype (fiber-emb-Prop e) f) +``` + +### A type is subfinitely indexed if and only if it is a subtype of a finitely indexed type + +**Proof.** Given a subfinite indexing on `X`, we may form the +[pushout](synthetic-homotopy-theory.pushouts.md) + +```text + D ╰──────→ Fin n + │ │ + │ │ + ↡ ⌜ ↓ + X ─────────→ D'. +``` + +Since surjective maps are the left class of an orthogonal factorization system +they are stable under cobase change, so the right vertical map is surjective. +And by Proposition 2.2.6 of {{#cite ABFJ20}} the pushout of an embedding is an +embedding, so the bottom horizontal map is an embedding. + +Conversely, given a subtype of a finitely indexed type, we may form the +[pullback](foundation-core.pullbacks.md) + +```text + D' ──────→ Fin n + │ ⌟ │ + │ │ + ↓ ↡ + X ╰────────→ D. +``` + +Embeddings are closed under pullbacks since it is characterized as the right +class of an orthogonal factorization system, and since this orthogonal +factorization system is stable, so are the surjections. ■ + +> This remains to be formalized. + +### Types equipped with subfinite indexings are Dedekind finite + +We reproduce a proof given by +[Gro-Tsen](https://mathoverflow.net/users/17064/gro-tsen) in this MathOverflow +answer: . + +**Proof.** Let $X$ be a subfinitely indexed type, witnessed by $Fin n ↩ D ↠ X$ +where $h$ is the surjection. We wish to show $X$ is Dedekind finite, so let +$f : X ↪ X$ be an arbitrary self-embedding. To conclude $f$ is an equivalence it +suffices to prove $f$ is surjective, so assume given an arbitrary $x : X$ where +we want to show there exists $z : X$ such that $f(z) ＝ x$. + +The mapping $i ↦ fⁱ(x)$ defines a sequence of elements of $X$. By surjectivity +of $h$ each $fⁱ(x)$ merely has a representative in $D$, so by +[finite choice](univalent-combinatorics.finite-choice.md) there exists a +sequence $x₋ : D^{\operatorname{Fin}n}$ lifting $x,f(x),…,f^{n-1}(x)$. + +Now, the standard pigeonhole principle applies to $\operatorname{Fin}n$, so +there has to be $i < j$ in $\operatorname{Fin}n$ such that $xᵢ = xⱼ$, and in +particular $h(xᵢ) = h(xⱼ)$, i.e., $fⁱ(x) = fʲ(x)$. By injectivity of $f$ we can +cancel $i$ applications to obtain $x = f(f^{j-i-1}(x))$, and so $f^{j-i-1}(x)$ +is the desired preimage. ∎ + +```agda +module _ + {l1 l2 : Level} {X : UU l1} (c : subfinite-indexing l2 X) + where + + abstract + lemma-is-surjective-is-injective-endo-subfinite-indexing : + (f : X → X) → + is-injective f → + (x : X) → + ((i : Fin (succ-ℕ (bound-number-of-elements-subfinite-indexing c))) → + fiber + ( map-projection-subfinite-indexing c) + ( iterate + ( nat-Fin (succ-ℕ (bound-number-of-elements-subfinite-indexing c)) i) + ( f) + ( x))) → + fiber f x + lemma-is-surjective-is-injective-endo-subfinite-indexing + f is-injective-f x hy = + ( iterate k f x , compute-iterate-dist-f-x) + where abstract + y : + Fin (succ-ℕ (bound-number-of-elements-subfinite-indexing c)) → + indexing-type-subfinite-indexing c + y = pr1 ∘ hy + + r : repetition-of-values y + r = + inv-ap-repetition-of-values + ( is-injective-emb (emb-subfinite-indexing c)) + ( repetition-of-values-Fin-succ-to-Fin + ( bound-number-of-elements-subfinite-indexing c) + ( map-emb-subfinite-indexing c ∘ y)) + + i : ℕ + i = + nat-Fin + ( succ-ℕ (bound-number-of-elements-subfinite-indexing c)) + ( first-repetition-of-values y r) + + j : ℕ + j = + nat-Fin + ( succ-ℕ (bound-number-of-elements-subfinite-indexing c)) + ( second-repetition-of-values y r) + + k+1-nonzero : ℕ⁺ + k+1-nonzero = + ( dist-ℕ i j , + dist-neq-ℕ i j + ( distinction-repetition-of-values y r ∘ + is-injective-nat-Fin + ( succ-ℕ (bound-number-of-elements-subfinite-indexing c)))) + + k : ℕ + k = pred-ℕ⁺ k+1-nonzero + + compute-succ-k : succ-ℕ k ＝ dist-ℕ i j + compute-succ-k = ap pr1 (is-section-succ-nonzero-ℕ' k+1-nonzero) + + compute-iterate-f-x : iterate i f x ＝ iterate j f x + compute-iterate-f-x = + inv (pr2 (hy (first-repetition-of-values y r))) ∙ + ap + ( map-projection-subfinite-indexing c) + ( is-repetition-of-values-repetition-of-values y r) ∙ + pr2 (hy (second-repetition-of-values y r)) + + compute-iterate-min-max-f-x : + iterate (max-ℕ i j) f x ＝ iterate (min-ℕ i j) f x + compute-iterate-min-max-f-x = + eq-value-min-max-eq-value-sequence + ( λ u → iterate u f x) + ( i) + ( j) + ( compute-iterate-f-x) + + compute-iterate-dist-f-x : f (iterate k f x) ＝ x + compute-iterate-dist-f-x = + compute-iterate-offset f is-injective-f + ( min-ℕ i j) + ( k) + ( ( ap + ( λ u → iterate u f x) + ( ( inv (left-successor-law-add-ℕ k (min-ℕ i j))) ∙ + ( ap (_+ℕ min-ℕ i j) compute-succ-k) ∙ + ( eq-max-dist-min-ℕ i j))) ∙ + ( compute-iterate-min-max-f-x)) + + abstract + is-surjective-is-injective-endo-subfinite-indexing : + (f : X → X) → is-injective f → is-surjective f + is-surjective-is-injective-endo-subfinite-indexing f F x = + map-trunc-Prop + ( lemma-is-surjective-is-injective-endo-subfinite-indexing f F x) + ( finite-choice-Fin + ( succ-ℕ (bound-number-of-elements-subfinite-indexing c)) + ( λ i → + is-surjective-map-projection-subfinite-indexing c + ( iterate + ( nat-Fin + ( succ-ℕ (bound-number-of-elements-subfinite-indexing c)) + ( i)) + ( f) + ( x)))) + + is-dedekind-finite-subfinite-indexing : + (f : X → X) → is-emb f → is-equiv f + is-dedekind-finite-subfinite-indexing f is-emb-f = + is-equiv-is-emb-is-surjective + ( is-surjective-is-injective-endo-subfinite-indexing f + ( is-injective-is-emb is-emb-f)) + ( is-emb-f) +``` + +## References + +{{#bibliograhy}} diff --git a/src/univalent-combinatorics/subfinite-types.lagda.md b/src/univalent-combinatorics/subfinite-types.lagda.md new file mode 100644 index 0000000000..a1ca4f4bbd --- /dev/null +++ b/src/univalent-combinatorics/subfinite-types.lagda.md @@ -0,0 +1,298 @@ +# Subfinite types + +```agda +module univalent-combinatorics.subfinite-types where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.distance-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.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.strict-inequality-natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.decidable-equality +open import foundation.dependent-pair-types +open import foundation.discrete-types +open import foundation.embeddings +open import foundation.empty-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.iterating-functions +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.repetitions-of-values +open import foundation.sections +open import foundation.sets +open import foundation.split-surjective-maps +open import foundation.surjective-maps +open import foundation.universe-levels + +open import univalent-combinatorics.dedekind-finite-types +open import univalent-combinatorics.equality-finite-types +open import univalent-combinatorics.equality-standard-finite-types +open import univalent-combinatorics.finite-types +open import univalent-combinatorics.pigeonhole-principle +open import univalent-combinatorics.sequences-finite-types +open import univalent-combinatorics.standard-finite-types +open import univalent-combinatorics.subcounting +``` + +
+ +## Idea + +A type `X` is {{#concept "subfinite" Agda=is-subfinite Agda=Subfinite-Type}} if +there [exists](foundation.existential-quantification.md) an +[embedding](foundation-core.embeddings.md) into a +[standard finite type](univalent-combinatorics.standard-finite-types.md). + +## Definitions + +### The predicate of being subfinite + +```agda +is-subfinite-Prop : {l : Level} → UU l → Prop l +is-subfinite-Prop X = trunc-Prop (subcount X) + +is-subfinite : {l : Level} → UU l → UU l +is-subfinite X = type-Prop (is-subfinite-Prop X) + +is-prop-is-subfinite : {l : Level} {X : UU l} → is-prop (is-subfinite X) +is-prop-is-subfinite {X = X} = is-prop-type-Prop (is-subfinite-Prop X) +``` + +### The subuniverse of subfinite types + +```agda +Subfinite-Type : (l : Level) → UU (lsuc l) +Subfinite-Type l = Σ (UU l) (is-subfinite) + +module _ + {l : Level} (X : Subfinite-Type l) + where + + type-Subfinite-Type : UU l + type-Subfinite-Type = pr1 X + + is-subfinite-type-Subfinite-Type : is-subfinite type-Subfinite-Type + is-subfinite-type-Subfinite-Type = pr2 X +``` + +## Properties + +### Subfinite types are discrete + +```agda +module _ + {l : Level} (X : Subfinite-Type l) + where + + has-decidable-equality-type-Subfinite-Type : + has-decidable-equality (type-Subfinite-Type X) + has-decidable-equality-type-Subfinite-Type = + rec-trunc-Prop + ( has-decidable-equality-Prop (type-Subfinite-Type X)) + ( λ (k , f) → has-decidable-equality-emb f (has-decidable-equality-Fin k)) + ( is-subfinite-type-Subfinite-Type X) + + discrete-type-Subfinite-Type : Discrete-Type l + discrete-type-Subfinite-Type = + ( type-Subfinite-Type X , has-decidable-equality-type-Subfinite-Type) +``` + +### Subfinite types are sets + +```agda +module _ + {l : Level} (X : Subfinite-Type l) + where + + is-set-type-Subfinite-Type : is-set (type-Subfinite-Type X) + is-set-type-Subfinite-Type = + is-set-has-decidable-equality (has-decidable-equality-type-Subfinite-Type X) + + set-Subfinite-Type : Set l + set-Subfinite-Type = (type-Subfinite-Type X , is-set-type-Subfinite-Type) +``` + +### Subfinite types are Dedekind finite + +We reproduce a proof given by +[Gro-Tsen](https://mathoverflow.net/users/17064/gro-tsen) in this MathOverflow +answer: . + +**Proof.** Let $X$ be a subfinite type witnessed by $ι : X ↪ Fin n$, and let +$f : X ↪ X$ be an arbitrary self-embedding. It suffices to prove $f$ is +surjective, so assume given an $x : X$ where we want to show there exists +$z : X$ such that $f(z) ＝ x$. The mapping $i ↦ fⁱ(x)$ defines an $ℕ$-indexed +sequence of elements of $X$. Since the +[standard pigeonhole principle](univalent-combinatorics.pigeonhole-principle.md) +applies to $\operatorname{Fin}n$ there has to be $i < j$ in +$\operatorname{Fin}n$ such that $ι(fⁱ(x)) = ι(fʲ(x))$. Since $ι$ is an embedding +we in particular have $fⁱ(x) = fʲ(x)$ . By injectivity of $f$ we can cancel $i$ +applications on both sides of the equation to obtain $x = f(f^{j-i-1}(x))$, and +so $f^{j-i-1}(x)$ is our desired preimage of $x$. ∎ + +```agda +module _ + {l : Level} {X : UU l} + where + + eq-value-min-max-eq-value-sequence : + (f : ℕ → X) (i j : ℕ) → f i ＝ f j → f (max-ℕ i j) ＝ f (min-ℕ i j) + eq-value-min-max-eq-value-sequence f i j p = + rec-coproduct + ( λ i≤j → + ap f (leq-right-max-ℕ i j i≤j) ∙ + inv p ∙ + ap f (inv (leq-left-min-ℕ i j i≤j))) + ( λ j≤i → + ap f (leq-left-max-ℕ i j j≤i) ∙ + p ∙ + ap f (inv (leq-right-min-ℕ i j j≤i))) + ( linear-leq-ℕ i j) + + compute-iterate-offset : + (f : X → X) {x : X} → is-injective f → (i d : ℕ) → + iterate (succ-ℕ (d +ℕ i)) f x ＝ iterate i f x → + f (iterate d f x) ＝ x + compute-iterate-offset f is-injective-f zero-ℕ d p = p + compute-iterate-offset f is-injective-f (succ-ℕ i) d p = + compute-iterate-offset f is-injective-f i d (is-injective-f p) + +module _ + {l : Level} {X : UU l} (c : subcount X) + where + + is-split-surjective-is-injective-endo-subcount : + (f : X → X) → is-injective f → is-split-surjective f + is-split-surjective-is-injective-endo-subcount f is-injective-f x = + ( iterate k f x , compute-iterate-dist-f-x) + where + + y : ℕ → Fin (bound-number-of-elements-subcount c) + y i = map-subcount c (iterate i f x) + + r : repetition-of-values y + r = + repetition-of-values-sequence-Fin (bound-number-of-elements-subcount c) y + + i : ℕ + i = first-repetition-of-values y r + + j : ℕ + j = second-repetition-of-values y r + + k+1-nonzero : ℕ⁺ + k+1-nonzero = + ( dist-ℕ i j , dist-neq-ℕ i j (distinction-repetition-of-values y r)) + + k : ℕ + k = pred-ℕ⁺ k+1-nonzero + + compute-succ-k : succ-ℕ k ＝ dist-ℕ i j + compute-succ-k = ap pr1 (is-section-succ-nonzero-ℕ' k+1-nonzero) + + compute-iterate-f-x : iterate i f x ＝ iterate j f x + compute-iterate-f-x = + is-injective-map-subcount c + ( is-repetition-of-values-repetition-of-values y r) + + compute-iterate-min-max-f-x : + iterate (max-ℕ i j) f x ＝ iterate (min-ℕ i j) f x + compute-iterate-min-max-f-x = + eq-value-min-max-eq-value-sequence + (λ u → iterate u f x) + ( i) + ( j) + ( compute-iterate-f-x) + + compute-iterate-dist-f-x : f (iterate k f x) ＝ x + compute-iterate-dist-f-x = + compute-iterate-offset f is-injective-f + ( min-ℕ i j) + ( k) + ( ( ap + ( λ u → iterate u f x) + ( ( inv (left-successor-law-add-ℕ k (min-ℕ i j))) ∙ + ( ap (_+ℕ min-ℕ i j) compute-succ-k) ∙ + ( eq-max-dist-min-ℕ i j))) ∙ + ( compute-iterate-min-max-f-x)) + + is-dedekind-finite-subcount' : + (f : X → X) → is-injective f → is-equiv f + is-dedekind-finite-subcount' f is-injective-f = + is-equiv-is-split-surjective-is-injective f + ( is-injective-f) + ( is-split-surjective-is-injective-endo-subcount f is-injective-f) + + is-dedekind-finite-subcount : + (f : X → X) → is-emb f → is-equiv f + is-dedekind-finite-subcount f is-emb-f = + is-dedekind-finite-subcount' f (is-injective-is-emb is-emb-f) + +module _ + {l : Level} (X : Subfinite-Type l) + where + + is-dedekind-finite-type-Subfinite-Type' : + (f : type-Subfinite-Type X → type-Subfinite-Type X) → + is-injective f → is-equiv f + is-dedekind-finite-type-Subfinite-Type' f is-injective-f = + rec-trunc-Prop + ( is-equiv-Prop f) + ( λ j → is-dedekind-finite-subcount' j f is-injective-f) + ( is-subfinite-type-Subfinite-Type X) + + is-dedekind-finite-type-Subfinite-Type : + is-dedekind-finite (type-Subfinite-Type X) + is-dedekind-finite-type-Subfinite-Type f is-emb-f = + is-dedekind-finite-type-Subfinite-Type' f (is-injective-is-emb is-emb-f) + + dedekind-finite-type-Subfinite-Type : Dedekind-Finite-Type l + dedekind-finite-type-Subfinite-Type = + ( type-Subfinite-Type X , is-dedekind-finite-type-Subfinite-Type) +``` + +### The Cantor–Schröder–Bernstein theorem for subfinite types + +If two subfinite types `X` and `Y` mutually embed, `X ↪ Y` and `Y ↪ X`, then +`X ≃ Y`. + +```agda +module _ + {l1 l2 : Level} (X : Subfinite-Type l1) (Y : Subfinite-Type l2) + where + + cantor-schröder-bernstein-Subfinite-Type : + (type-Subfinite-Type X ↪ type-Subfinite-Type Y) → + (type-Subfinite-Type Y ↪ type-Subfinite-Type X) → + type-Subfinite-Type X ≃ type-Subfinite-Type Y + cantor-schröder-bernstein-Subfinite-Type = + cantor-schröder-bernstein-Dedekind-Finite-Type + ( dedekind-finite-type-Subfinite-Type X) + ( dedekind-finite-type-Subfinite-Type Y) +``` + +## External links + +- [Finiteness in Sheaf Topoi](https://grossack.site/2024/08/19/finiteness-in-sheaf-topoi), + blog post by Chris Grossack +- [`Fin.Kuratowski`](https://www.cs.bham.ac.uk/~mhe/TypeTopology/Fin.Kuratowski.html) + at TypeTopology +- [finite set](https://ncatlab.org/nlab/show/finite+set) at $n$Lab +- [finite object](https://ncatlab.org/nlab/show/finite+object) at $n$Lab +- [Finite set](https://en.wikipedia.org/wiki/Finite_set) at Wikipedia diff --git a/src/univalent-combinatorics/subfinitely-indexed-types.lagda.md b/src/univalent-combinatorics/subfinitely-indexed-types.lagda.md new file mode 100644 index 0000000000..665b866119 --- /dev/null +++ b/src/univalent-combinatorics/subfinitely-indexed-types.lagda.md @@ -0,0 +1,158 @@ +# Subfinitely indexed types + +```agda +module univalent-combinatorics.subfinitely-indexed-types where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.decidable-equality +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.functoriality-propositional-truncation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.surjective-maps +open import foundation.universe-levels + +open import univalent-combinatorics.dedekind-finite-types +open import univalent-combinatorics.equality-finite-types +open import univalent-combinatorics.finite-types +open import univalent-combinatorics.image-of-maps +open import univalent-combinatorics.standard-finite-types +open import univalent-combinatorics.subfinite-indexing +open import univalent-combinatorics.subfinite-types +``` + +
+ +## Idea + +A type `X` is +{{#concept "subfinitely indexed" agda=is-subfinitely-indexed agda=Subfinitely-Indexed-Type}}, +or **Kuratowski subfinite**, if there +[exists](foundation.existential-quantification.md) a +[surjection](foundation.surjective-maps.md) onto `X` from a +[subfinite type](univalent-combinatorics.subfinite-types.md). + +## Definitions + +### The predicate of being subfinitely indexed + +```agda +is-subfinitely-indexed-Prop : + {l1 : Level} (l2 : Level) → UU l1 → Prop (l1 ⊔ lsuc l2) +is-subfinitely-indexed-Prop l2 X = + exists-structure-Prop (Subfinite-Type l2) (λ N → type-Subfinite-Type N ↠ X) + +is-subfinitely-indexed : + {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +is-subfinitely-indexed l2 X = type-Prop (is-subfinitely-indexed-Prop l2 X) + +is-prop-is-subfinitely-indexed : + {l1 l2 : Level} {X : UU l1} → is-prop (is-subfinitely-indexed l2 X) +is-prop-is-subfinitely-indexed {l2 = l2} {X} = + is-prop-type-Prop (is-subfinitely-indexed-Prop l2 X) +``` + +### The subuniverse of subfinitely indexed types + +```agda +Subfinitely-Indexed-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Subfinitely-Indexed-Type l1 l2 = Σ (UU l1) (is-subfinitely-indexed l2) + +module _ + {l1 l2 : Level} (X : Subfinitely-Indexed-Type l1 l2) + where + + type-Subfinitely-Indexed-Type : UU l1 + type-Subfinitely-Indexed-Type = pr1 X + + is-subfinitely-indexed-Subfinitely-Indexed-Type : + is-subfinitely-indexed l2 type-Subfinitely-Indexed-Type + is-subfinitely-indexed-Subfinitely-Indexed-Type = pr2 X +``` + +## Properties + +### Types with subfinite indexings are subfinitely indexed + +```agda +module _ + {l1 l2 : Level} {X : UU l1} + where + + abstract + is-subfinitely-indexed-has-subfinite-indexing : + subfinite-indexing l2 X → is-subfinitely-indexed l2 X + is-subfinitely-indexed-has-subfinite-indexing (D , e , h) = + unit-trunc-Prop ((D , unit-trunc-Prop e) , h) + + abstract + is-inhabited-subfinite-indexing-is-subfinitely-indexed : + is-subfinitely-indexed l2 X → ║ subfinite-indexing l2 X ║₋₁ + is-inhabited-subfinite-indexing-is-subfinitely-indexed = + rec-trunc-Prop + ( trunc-Prop (subfinite-indexing l2 X)) + ( λ ((D , |e|) , h) → map-trunc-Prop (λ e → (D , e , h)) |e|) +``` + +### Subfinitely indexed types are Dedekind finite + +```agda +module _ + {l1 l2 : Level} (X : Subfinitely-Indexed-Type l1 l2) + where + + is-dedekind-finite-type-Subfinitely-Indexed-Type : + is-dedekind-finite (type-Subfinitely-Indexed-Type X) + is-dedekind-finite-type-Subfinitely-Indexed-Type f is-emb-f = + rec-trunc-Prop + ( is-equiv-Prop f) + ( λ c → is-dedekind-finite-subfinite-indexing c f is-emb-f) + ( is-inhabited-subfinite-indexing-is-subfinitely-indexed + ( is-subfinitely-indexed-Subfinitely-Indexed-Type X)) + + dedekind-finite-type-Subfinitely-Indexed-Type : Dedekind-Finite-Type l1 + dedekind-finite-type-Subfinitely-Indexed-Type = + ( type-Subfinitely-Indexed-Type X , + is-dedekind-finite-type-Subfinitely-Indexed-Type) +``` + +### The Cantor–Schröder–Bernstein theorem for subfinitely indexed types + +If two subfinitely indexed types `X` and `Y` mutually embed, `X ↪ Y` and +`Y ↪ X`, then `X ≃ Y`. + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Subfinitely-Indexed-Type l1 l2) + (Y : Subfinitely-Indexed-Type l3 l4) + where + + cantor-schröder-bernstein-Subfinitely-Indexed-Type : + (type-Subfinitely-Indexed-Type X ↪ type-Subfinitely-Indexed-Type Y) → + (type-Subfinitely-Indexed-Type Y ↪ type-Subfinitely-Indexed-Type X) → + type-Subfinitely-Indexed-Type X ≃ type-Subfinitely-Indexed-Type Y + cantor-schröder-bernstein-Subfinitely-Indexed-Type = + cantor-schröder-bernstein-Dedekind-Finite-Type + ( dedekind-finite-type-Subfinitely-Indexed-Type X) + ( dedekind-finite-type-Subfinitely-Indexed-Type Y) +``` + +## External links + +- [Finiteness in Sheaf Topoi](https://grossack.site/2024/08/19/finiteness-in-sheaf-topoi), + blog post by Chris Grossack +- [`Fin.Kuratowski`](https://www.cs.bham.ac.uk/~mhe/TypeTopology/Fin.Kuratowski.html) + at TypeTopology +- [finite set](https://ncatlab.org/nlab/show/finite+set) at $n$Lab +- [finite object](https://ncatlab.org/nlab/show/finite+object) at $n$Lab +- [Finite set](https://en.wikipedia.org/wiki/Finite_set) at Wikipedia diff --git a/src/univalent-combinatorics/surjective-maps.lagda.md b/src/univalent-combinatorics/surjective-maps.lagda.md index 2ebd5851c5..d21747be79 100644 --- a/src/univalent-combinatorics/surjective-maps.lagda.md +++ b/src/univalent-combinatorics/surjective-maps.lagda.md @@ -63,8 +63,7 @@ module _ where count-surjection-has-decidable-equality : - (n : ℕ) → (has-decidable-equality X) → (Fin n ↠ X) → - count (X) + (n : ℕ) → (has-decidable-equality X) → (Fin n ↠ X) → count X count-surjection-has-decidable-equality n dec-X f = count-decidable-emb ( ( map-equiv