From 9f38f3bfc2d9c3606a46af402da6a7d74a8c1208 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Thu, 28 Aug 2025 17:55:31 -0600 Subject: [PATCH 01/35] it's working with an unsolved meta currently. need to fill that hole and it's done --- src/foundation/connected-types.lagda.md | 10 +++++++ .../acyclic-types.lagda.md | 14 +++++++++- .../suspensions-of-types.lagda.md | 26 +++++++++++++++++++ 3 files changed, 49 insertions(+), 1 deletion(-) diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md index 06cf448eef..fad35eea72 100644 --- a/src/foundation/connected-types.lagda.md +++ b/src/foundation/connected-types.lagda.md @@ -271,3 +271,13 @@ module _ ( λ where refl → refl) ( center (K a x))))) ``` + +In particular, inhabited types are `-1`-connected; their identity types are +`-2`-connected, as all types are. + +```agda +is-neg-one-connected-is-inhabited : + {l : Level} (A : UU l) → is-inhabited A → is-connected neg-one-𝕋 A +is-neg-one-connected-is-inhabited A a = + is-connected-succ-is-connected-eq a (λ x y → is-neg-two-connected (x ＝ y)) +``` diff --git a/src/synthetic-homotopy-theory/acyclic-types.lagda.md b/src/synthetic-homotopy-theory/acyclic-types.lagda.md index cb83beef9d..d68f28fd66 100644 --- a/src/synthetic-homotopy-theory/acyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-types.lagda.md @@ -8,11 +8,14 @@ module synthetic-homotopy-theory.acyclic-types where ```agda open import foundation.contractible-types +open import foundation.0-connected-types open import foundation.equivalences +open import foundation.inhabited-types open import foundation.propositions open import foundation.retracts-of-types open import foundation.unit-type open import foundation.universe-levels +open import foundation.propositional-truncations open import synthetic-homotopy-theory.functoriality-suspensions open import synthetic-homotopy-theory.suspensions-of-types @@ -80,7 +83,16 @@ is-acyclic-unit = is-acyclic-is-contr unit is-contr-unit ### Acyclic types are inhabited -> TODO +Proof: `Σ X` is 0-connected if and only if `X` is inhabited, and contractible +types are of course 0-connected. + +```agda +is-inhabited-is-acyclic : {l : Level} (A : UU l) → is-acyclic A → is-inhabited A +is-inhabited-is-acyclic A ac = + is-inhabited-suspension-is-0-connected + ( A) + ( is-0-connected-is-contr (suspension A) ac) +``` ## See also diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index b0d6084cbc..1fb10558ba 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -1,6 +1,8 @@ # Suspensions of types ```agda +{-# OPTIONS --allow-unsolved-metas #-} + module synthetic-homotopy-theory.suspensions-of-types where ``` @@ -9,6 +11,8 @@ module synthetic-homotopy-theory.suspensions-of-types where ```agda open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions +open import foundation.0-connected-types +open import foundation.inhabited-types open import foundation.booleans open import foundation.commuting-squares-of-identifications open import foundation.connected-types @@ -21,6 +25,7 @@ open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-extensionality +open import foundation.set-truncations open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types @@ -644,3 +649,24 @@ module _ ( Y)) ( is-equiv-id)) ``` + +### `Σ X` is 0-connected if and only if `X` is inhabited + +Note that `Σ empty = bool` is not 0-connected. + +The forward direction is the subtle one. When `Σ X` is 0-connected, then in +particular we merely have `p ∈ north-suspension ＝ south-suspension`; such +identifications are generated by `X`. + +```agda +suspension-is-0-connected-is-inhabited : + {l : Level} (X : UU l) → is-inhabited X → is-0-connected (suspension X) +suspension-is-0-connected-is-inhabited X x = + is-connected-succ-suspension-is-connected + ( is-neg-one-connected-is-inhabited X x) + +is-inhabited-suspension-is-0-connected : + {l : Level} (X : UU l) → is-0-connected (suspension X) → is-inhabited X +is-inhabited-suspension-is-0-connected X (sx , p) = + {! !} +``` From 2a9af3387bece3cadabc1fa29f368daed9b993c8 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Thu, 28 Aug 2025 18:45:34 -0600 Subject: [PATCH 02/35] this is growing --- src/foundation/connected-types.lagda.md | 4 + .../acyclic-types.lagda.md | 4 +- .../suspensions-of-types.lagda.md | 86 +++++++++++++++++-- 3 files changed, 87 insertions(+), 7 deletions(-) diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md index fad35eea72..0cc9114604 100644 --- a/src/foundation/connected-types.lagda.md +++ b/src/foundation/connected-types.lagda.md @@ -280,4 +280,8 @@ is-neg-one-connected-is-inhabited : {l : Level} (A : UU l) → is-inhabited A → is-connected neg-one-𝕋 A is-neg-one-connected-is-inhabited A a = is-connected-succ-is-connected-eq a (λ x y → is-neg-two-connected (x ＝ y)) + +is-inhabited-is-neg-one-connected : + {l : Level} (A : UU l) → is-connected neg-one-𝕋 A → is-inhabited A +is-inhabited-is-neg-one-connected A (a , _) = a ``` diff --git a/src/synthetic-homotopy-theory/acyclic-types.lagda.md b/src/synthetic-homotopy-theory/acyclic-types.lagda.md index d68f28fd66..ad94fffefb 100644 --- a/src/synthetic-homotopy-theory/acyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-types.lagda.md @@ -7,15 +7,15 @@ module synthetic-homotopy-theory.acyclic-types where
Imports ```agda -open import foundation.contractible-types open import foundation.0-connected-types +open import foundation.contractible-types open import foundation.equivalences open import foundation.inhabited-types +open import foundation.propositional-truncations open import foundation.propositions open import foundation.retracts-of-types open import foundation.unit-type open import foundation.universe-levels -open import foundation.propositional-truncations open import synthetic-homotopy-theory.functoriality-suspensions open import synthetic-homotopy-theory.suspensions-of-types diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 1fb10558ba..2884a3445d 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -1,18 +1,17 @@ # Suspensions of types ```agda -{-# OPTIONS --allow-unsolved-metas #-} - module synthetic-homotopy-theory.suspensions-of-types where ```
Imports ```agda +open import elementary-number-theory.natural-numbers + +open import foundation.0-connected-types open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions -open import foundation.0-connected-types -open import foundation.inhabited-types open import foundation.booleans open import foundation.commuting-squares-of-identifications open import foundation.connected-types @@ -25,17 +24,18 @@ open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-extensionality -open import foundation.set-truncations open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types +open import foundation.inhabited-types open import foundation.path-algebra open import foundation.propositional-truncations open import foundation.propositions open import foundation.retractions open import foundation.sections +open import foundation.set-truncations open import foundation.surjective-maps open import foundation.torsorial-type-families open import foundation.transport-along-identifications @@ -46,6 +46,10 @@ open import foundation.unit-type open import foundation.universe-levels open import foundation.whiskering-homotopies-composition +open import foundation-core.coproduct-types +open import foundation-core.empty-types +open import foundation-core.sets + open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-suspension-structures @@ -54,6 +58,8 @@ open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.suspension-structures open import synthetic-homotopy-theory.universal-property-pushouts open import synthetic-homotopy-theory.universal-property-suspensions + +open import univalent-combinatorics.finite-types ```
@@ -557,6 +563,30 @@ module _ is-surjective-map-surjection-bool-suspension ``` +### The suspension of an empty type is the booleans + +```agda +module _ + {l : Level} (X : UU l) (emp : is-empty X) + where + + is-equiv-map-surjection-bool-suspension : + is-equiv map-surjection-bool-suspension + pr1 (pr1 is-equiv-map-surjection-bool-suspension) = + cogap-suspension (true , (false , ex-falso ∘ emp)) + pr2 (pr1 is-equiv-map-surjection-bool-suspension) x = {! !} + pr1 (pr2 is-equiv-map-surjection-bool-suspension) = + cogap-suspension (true , (false , ex-falso ∘ emp)) + pr2 (pr2 is-equiv-map-surjection-bool-suspension) true = {! !} + pr2 (pr2 is-equiv-map-surjection-bool-suspension) false = {! !} + + equiv-map-surjection-bool-suspension : + bool ≃ suspension X + pr1 equiv-map-surjection-bool-suspension = map-surjection-bool-suspension + pr2 equiv-map-surjection-bool-suspension = + is-equiv-map-surjection-bool-suspension +``` + ### The suspension of a contractible type is contractible ```agda @@ -670,3 +700,49 @@ is-inhabited-suspension-is-0-connected : is-inhabited-suspension-is-0-connected X (sx , p) = {! !} ``` + +In fact, the following are logically equivalent: + +- `X` is empty or inhabited +- `trunc-Set (Σ X)` is [finite](univalent-combinatorics.finite-types.md) + +Proof: + +(->): When `X` is empty, its suspension is the set `Fin 2`. When `X` is +inhabited, its suspension is 0-connected, and 0-truncated 0-connected types are +contractible and hence are `Fin 1`. + +(<-): Such a cardinality can only be 1 or 2. When it's 1, i.e. when +`trunc-Set (Σ X)` is 0-connected, then it follows that `Σ X` is also +0-connected, therefore that `X` is inhabited. When it's 2, i.e. when there are +no identifications `north = south` in `Σ X`, then `X` had to have been empty. + +```agda +module _ + {l : Level} (X : UU l) + where + + is-finite-suspension-is-inhabited-or-empty : + is-empty X + is-inhabited X → is-finite (type-trunc-Set (suspension X)) + is-finite-suspension-is-inhabited-or-empty (inl x) = + is-finite-equiv + ( equiv-unit-trunc-set + ( suspension X , + is-set-equiv + ( bool) + ( inv-equiv + ( equiv-map-surjection-bool-suspension X x)) + ( is-set-bool)) ∘e + equiv-map-surjection-bool-suspension X x) + ( is-finite-bool) + is-finite-suspension-is-inhabited-or-empty (inr x) = + is-finite-is-contr {! !} + + is-inhabited-or-empty-is-finite-suspension : + is-finite (type-trunc-Set (suspension X)) → is-empty X + is-inhabited X + is-inhabited-or-empty-is-finite-suspension p with number-of-elements-is-finite p + ... | 0 = ex-falso {! !} + ... | 1 = inr {! !} + ... | 2 = inl {! !} + ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! !} +``` From 716cf96168fec73ff21bf3c35230a036ecfbbdea Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 00:42:08 -0600 Subject: [PATCH 03/35] workinonit --- src/foundation/set-truncations.lagda.md | 15 ++ src/foundation/surjective-maps.lagda.md | 13 ++ .../suspensions-of-types.lagda.md | 166 +++++++++++++++--- .../finitely-enumerable-types.lagda.md | 22 +++ 4 files changed, 189 insertions(+), 27 deletions(-) diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md index 154cc2d2b5..774c72c400 100644 --- a/src/foundation/set-truncations.lagda.md +++ b/src/foundation/set-truncations.lagda.md @@ -567,3 +567,18 @@ module _ triangle-distributive-trunc-product-Set = pr2 (center distributive-trunc-product-Set) ``` + +### `X` is empty iff its set truncation is empty + +```agda +module _ + {l : Level} {X : UU l} + where + + is-empty-set-truncation-is-empty : is-empty (type-trunc-Set X) → is-empty X + is-empty-set-truncation-is-empty p x = p (unit-trunc-Set x) + + set-truncation-is-empty-is-empty : is-empty X → is-empty (type-trunc-Set X) + set-truncation-is-empty-is-empty p x = + apply-universal-property-trunc-Set empty-Set x p +``` diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index f5878a0f62..136f23d5e5 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -34,6 +34,7 @@ open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.constant-maps open import foundation-core.contractible-maps +open import foundation-core.empty-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.function-types @@ -873,6 +874,18 @@ module _ is-inhabited-is-surjective (is-surjective-map-surjection f) ``` +### When `X` is empty and `X` surjects onto `Y`, then `Y` is empty + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (emp-A : is-empty A) + where + + is-empty-surjection-empty : A ↠ B → is-empty B + is-empty-surjection-empty (f , p) b = + rec-trunc-Prop empty-Prop (λ (a , q) → emp-A a) (p b) +``` + ### 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. diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 2884a3445d..393f7b723f 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -20,6 +20,8 @@ open import foundation.contractible-types open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.diagonal-maps-of-types +open import foundation.double-negation +open import foundation.empty-types open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.fibers-of-maps @@ -30,7 +32,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.inhabited-types -open import foundation.path-algebra +open import foundation.mere-equivalences open import foundation.propositional-truncations open import foundation.propositions open import foundation.retractions @@ -38,6 +40,7 @@ open import foundation.sections open import foundation.set-truncations open import foundation.surjective-maps open import foundation.torsorial-type-families +open import foundation.transport-along-equivalences open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels @@ -47,9 +50,11 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.coproduct-types -open import foundation-core.empty-types +open import foundation-core.negation open import foundation-core.sets +open import logic.propositionally-decidable-types + open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-suspension-structures @@ -59,7 +64,11 @@ open import synthetic-homotopy-theory.suspension-structures open import synthetic-homotopy-theory.universal-property-pushouts open import synthetic-homotopy-theory.universal-property-suspensions +open import univalent-combinatorics.2-element-types +open import univalent-combinatorics.counting open import univalent-combinatorics.finite-types +open import univalent-combinatorics.finitely-enumerable-types +open import univalent-combinatorics.standard-finite-types ```
@@ -103,6 +112,10 @@ meridian-suspension : meridian-suspension {X = X} = glue-pushout (terminal-map X) (terminal-map X) +is-inhabited-suspension : + {l : Level} (X : UU l) → is-inhabited (suspension X) +is-inhabited-suspension X = unit-trunc-Prop north-suspension + suspension-structure-suspension : {l : Level} (X : UU l) → suspension-structure X (suspension X) pr1 (suspension-structure-suspension X) = north-suspension @@ -563,6 +576,19 @@ module _ is-surjective-map-surjection-bool-suspension ``` +This provides a +[finite enumeration](univalent-combinatorics.finitely-enumerable-types.md) of +`Σ X`. + +```agda + finite-enumeration-suspension : finite-enumeration (suspension X) + pr1 finite-enumeration-suspension = 2 + pr2 finite-enumeration-suspension = + comp-surjection + ( surjection-bool-suspension) + ( surjection-equiv equiv-bool-Fin-2) +``` + ### The suspension of an empty type is the booleans ```agda @@ -570,15 +596,70 @@ module _ {l : Level} (X : UU l) (emp : is-empty X) where + suspension-structure-empty-bool : suspension-structure X bool + pr1 suspension-structure-empty-bool = true + pr1 (pr2 suspension-structure-empty-bool) = false + pr2 (pr2 suspension-structure-empty-bool) = ex-falso ∘ emp + + inv-map-surjection-bool-suspension : suspension X → bool + inv-map-surjection-bool-suspension = + cogap-suspension suspension-structure-empty-bool + + compute-true-suspension-empty-bool : + inv-map-surjection-bool-suspension north-suspension ＝ true + compute-true-suspension-empty-bool = + compute-north-cogap-suspension suspension-structure-empty-bool + + compute-false-suspension-empty-bool : + inv-map-surjection-bool-suspension south-suspension ＝ false + compute-false-suspension-empty-bool = + compute-south-cogap-suspension suspension-structure-empty-bool + + compute-north-suspension-empty-bool : + (map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension) + north-suspension + ＝ north-suspension + compute-north-suspension-empty-bool = + ap map-surjection-bool-suspension compute-true-suspension-empty-bool + + compute-south-suspension-empty-bool : + (map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension) + south-suspension + ＝ south-suspension + compute-south-suspension-empty-bool = + ap map-surjection-bool-suspension compute-false-suspension-empty-bool + + dependent-suspension-sutructure-surjection-bool-suspension : + dependent-suspension-structure + (λ z → + (map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension) + (z) + ＝ z) + (suspension-structure-suspension X) + pr1 dependent-suspension-sutructure-surjection-bool-suspension = + compute-north-suspension-empty-bool + pr1 (pr2 dependent-suspension-sutructure-surjection-bool-suspension) = + compute-south-suspension-empty-bool + pr2 (pr2 dependent-suspension-sutructure-surjection-bool-suspension) x = + ex-falso (emp x) + is-equiv-map-surjection-bool-suspension : is-equiv map-surjection-bool-suspension pr1 (pr1 is-equiv-map-surjection-bool-suspension) = - cogap-suspension (true , (false , ex-falso ∘ emp)) - pr2 (pr1 is-equiv-map-surjection-bool-suspension) x = {! !} + inv-map-surjection-bool-suspension + pr2 (pr1 is-equiv-map-surjection-bool-suspension) = + dependent-cogap-suspension + ( λ z → + ( map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension) + ( z) + ＝ z) + ( dependent-suspension-sutructure-surjection-bool-suspension) pr1 (pr2 is-equiv-map-surjection-bool-suspension) = - cogap-suspension (true , (false , ex-falso ∘ emp)) - pr2 (pr2 is-equiv-map-surjection-bool-suspension) true = {! !} - pr2 (pr2 is-equiv-map-surjection-bool-suspension) false = {! !} + inv-map-surjection-bool-suspension + pr2 (pr2 is-equiv-map-surjection-bool-suspension) true = + compute-true-suspension-empty-bool + pr2 (pr2 is-equiv-map-surjection-bool-suspension) false = + compute-false-suspension-empty-bool equiv-map-surjection-bool-suspension : bool ≃ suspension X @@ -686,7 +767,7 @@ Note that `Σ empty = bool` is not 0-connected. The forward direction is the subtle one. When `Σ X` is 0-connected, then in particular we merely have `p ∈ north-suspension ＝ south-suspension`; such -identifications are generated by `X`. +identifications are inductively generated by `X`. ```agda suspension-is-0-connected-is-inhabited : @@ -697,13 +778,13 @@ suspension-is-0-connected-is-inhabited X x = is-inhabited-suspension-is-0-connected : {l : Level} (X : UU l) → is-0-connected (suspension X) → is-inhabited X -is-inhabited-suspension-is-0-connected X (sx , p) = - {! !} +is-inhabited-suspension-is-0-connected X p = + unit-trunc-Prop {! !} ``` In fact, the following are logically equivalent: -- `X` is empty or inhabited +- `X` is [inhabited or empty](logic.propositionally-decidable-types.md) - `trunc-Set (Σ X)` is [finite](univalent-combinatorics.finite-types.md) Proof: @@ -712,37 +793,68 @@ Proof: inhabited, its suspension is 0-connected, and 0-truncated 0-connected types are contractible and hence are `Fin 1`. -(<-): Such a cardinality can only be 1 or 2. When it's 1, i.e. when -`trunc-Set (Σ X)` is 0-connected, then it follows that `Σ X` is also -0-connected, therefore that `X` is inhabited. When it's 2, i.e. when there are -no identifications `north = south` in `Σ X`, then `X` had to have been empty. +(<-): Such a cardinality can only be 1 or 2 - suspensions are inhabited, say, by +`north-suspension`, and the cardinality of a type finitely enumerated by +`Fin 2 = bool` can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` +is 0-connected, then it follows that `Σ X` is also 0-connected, therefore that +`X` is inhabited. When it's 2, i.e. when there are no identifications +`north = south` in `Σ X`, then `X` had to have been empty. ```agda module _ {l : Level} (X : UU l) where + trunc-suspension-is-contractible-is-pointed : + X → is-contr (type-trunc-Set (suspension X)) + trunc-suspension-is-contractible-is-pointed x = + suspension-is-0-connected-is-inhabited X (unit-trunc-Prop x) + + trunc-suspension-is-contractible-is-inhabited : + is-inhabited X → is-contr (type-trunc-Set (suspension X)) + trunc-suspension-is-contractible-is-inhabited x = + rec-trunc-Prop + ( is-contr-Prop (type-trunc-Set (suspension X))) + ( trunc-suspension-is-contractible-is-pointed) + ( x) + is-finite-suspension-is-inhabited-or-empty : - is-empty X + is-inhabited X → is-finite (type-trunc-Set (suspension X)) + is-inhabited-or-empty X → is-finite (type-trunc-Set (suspension X)) is-finite-suspension-is-inhabited-or-empty (inl x) = + is-finite-is-contr (trunc-suspension-is-contractible-is-inhabited x) + is-finite-suspension-is-inhabited-or-empty (inr x) = is-finite-equiv ( equiv-unit-trunc-set ( suspension X , - is-set-equiv - ( bool) - ( inv-equiv - ( equiv-map-surjection-bool-suspension X x)) - ( is-set-bool)) ∘e + is-set-equiv + ( bool) + ( inv-equiv + ( equiv-map-surjection-bool-suspension X x)) + ( is-set-bool)) ∘e equiv-map-surjection-bool-suspension X x) ( is-finite-bool) - is-finite-suspension-is-inhabited-or-empty (inr x) = - is-finite-is-contr {! !} + + is-empty-trunc-suspension-has-two-elements : + has-two-elements (type-trunc-Set (suspension X)) → is-empty X + is-empty-trunc-suspension-has-two-elements p x = + intro-double-negation + ( ap unit-trunc-Set (meridian-suspension x)) + ( λ q → is-not-one-two-ℕ (eq-cardinality p (unit-trunc-Prop eq))) + where + eq : Fin 1 ≃ type-trunc-Set (suspension X) + pr1 eq (inr star) = unit-trunc-Set north-suspension + pr1 (pr1 (pr2 eq)) _ = inr star + pr2 (pr1 (pr2 eq)) _ = + eq-is-contr (trunc-suspension-is-contractible-is-pointed x) + pr1 (pr2 (pr2 eq)) _ = inr star + pr2 (pr2 (pr2 eq)) (inr star) = refl is-inhabited-or-empty-is-finite-suspension : - is-finite (type-trunc-Set (suspension X)) → is-empty X + is-inhabited X + is-finite (type-trunc-Set (suspension X)) → is-inhabited-or-empty X is-inhabited-or-empty-is-finite-suspension p with number-of-elements-is-finite p - ... | 0 = ex-falso {! !} - ... | 1 = inr {! !} - ... | 2 = inl {! !} + ... | 0 = + ex-falso (is-nonempty-is-inhabited (is-inhabited-suspension X) (is-empty-set-truncation-is-empty (is-empty-is-zero-number-of-elements-is-finite p {! !}))) + ... | 1 = inl (is-inhabited-suspension-is-0-connected X {! !}) + ... | 2 = inr (is-empty-trunc-suspension-has-two-elements {! !}) ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! !} ``` diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index bfb1910c4e..1367badbff 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -1,12 +1,15 @@ # Finitely enumerable types ```agda +{-# OPTIONS --allow-unsolved-metas #-} + module univalent-combinatorics.finitely-enumerable-types where ```
Imports ```agda +open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers @@ -36,6 +39,8 @@ open import foundation.type-arithmetic-coproduct-types open import foundation.unit-type open import foundation.universe-levels +open import foundation-core.empty-types + open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.counting @@ -71,6 +76,9 @@ module _ is-finitely-enumerable : UU l is-finitely-enumerable = type-Prop is-finitely-enumerable-prop + cardinality-finite-enumeration : finite-enumeration → ℕ + cardinality-finite-enumeration (n , _) = n + Finitely-Enumerable-Type : (l : Level) → UU (lsuc l) Finitely-Enumerable-Type l = type-subtype (is-finitely-enumerable-prop {l}) @@ -116,6 +124,20 @@ is-finite-is-finitely-enumerable-discrete D eX = ∃-surjection-has-decidable-equality-if-is-finite (D , eX) ``` +We can say more: the cardinality of `X` enumerated by `Fin n` is bounded above +by `n`. + +```agda +is-upper-bound-finite-enumeration : + {l : Level} (X : UU l) → + (eq : has-decidable-equality X) → + (f : finite-enumeration X) → + leq-ℕ + (number-of-elements-count (count-finite-enumeration-discrete eq f)) + (cardinality-finite-enumeration X f) +is-upper-bound-finite-enumeration X eq (n , f) = {! !} +``` + ### Finite types are finitely enumerable ```agda From fc1ab8d1a0979bbc045653af880d82f56d0b1101 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 00:43:20 -0600 Subject: [PATCH 04/35] edits --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 393f7b723f..ac8ff43b17 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -578,7 +578,7 @@ module _ This provides a [finite enumeration](univalent-combinatorics.finitely-enumerable-types.md) of -`Σ X`. +`Σ X` by the canonical equivalence `bool ≃ Fin 2`. ```agda finite-enumeration-suspension : finite-enumeration (suspension X) From adf81f06813d014973515809b59c7d700498c710 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 00:47:22 -0600 Subject: [PATCH 05/35] edits --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index ac8ff43b17..2c593c51ef 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -761,9 +761,9 @@ module _ ( is-equiv-id)) ``` -### `Σ X` is 0-connected if and only if `X` is inhabited +### `Σ X` is 0-connected iff `X` is inhabited -Note that `Σ empty = bool` is not 0-connected. +Note that `Σ empty = bool` is not `0`-connected. The forward direction is the subtle one. When `Σ X` is 0-connected, then in particular we merely have `p ∈ north-suspension ＝ south-suspension`; such @@ -798,7 +798,7 @@ contractible and hence are `Fin 1`. `Fin 2 = bool` can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` is 0-connected, then it follows that `Σ X` is also 0-connected, therefore that `X` is inhabited. When it's 2, i.e. when there are no identifications -`north = south` in `Σ X`, then `X` had to have been empty. +`north = south` in `Σ X`, then `X` better have been empty. ```agda module _ From d91172ded8b23e4338bcb78ae048f5589472d9c5 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 10:47:58 -0600 Subject: [PATCH 06/35] I'm not convinced acyclic types have anything to do with cyclic groups... --- tables/cyclic-types.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/tables/cyclic-types.md b/tables/cyclic-types.md index dda8b45bec..5aac89f85e 100644 --- a/tables/cyclic-types.md +++ b/tables/cyclic-types.md @@ -1,7 +1,5 @@ | Concept | File | | ------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------- | -| Acyclic maps | [`synthetic-homotopy-theory.acyclic-maps`](synthetic-homotopy-theory.acyclic-maps.md) | -| Acyclic types | [`synthetic-homotopy-theory.acyclic-types`](synthetic-homotopy-theory.acyclic-types.md) | | Acyclic undirected graphs | [`graph-theory.acyclic-undirected-graphs`](graph-theory.acyclic-undirected-graphs.md) | | Bracelets | [`univalent-combinatorics.bracelets`](univalent-combinatorics.bracelets.md) | | The category of cyclic rings | [`ring-theory.category-of-cyclic-rings`](ring-theory.category-of-cyclic-rings.md) | @@ -15,7 +13,6 @@ | Euler's totient function | [`elementary-number-theory.eulers-totient-function`](elementary-number-theory.eulers-totient-function.md) | | Finitely cyclic maps | [`elementary-number-theory.finitely-cyclic-maps`](elementary-number-theory.finitely-cyclic-maps.md) | | Generating elements of groups | [`group-theory.generating-elements-groups`](group-theory.generating-elements-groups.md) | -| Hatcher's acyclic type | [`synthetic-homotopy-theory.hatchers-acyclic-type`](synthetic-homotopy-theory.hatchers-acyclic-type.md) | | Homomorphisms of cyclic rings | [`ring-theory.homomorphisms-cyclic-rings`](ring-theory.homomorphisms-cyclic-rings.md) | | Infinite cyclic types | [`synthetic-homotopy-theory.infinite-cyclic-types`](synthetic-homotopy-theory.infinite-cyclic-types.md) | | Multiplicative units in the standard cyclic rings | [`elementary-number-theory.multiplicative-units-standard-cyclic-rings`](elementary-number-theory.multiplicative-units-standard-cyclic-rings.md) | From f9303eddfe039c5e37e70cc1138f69699d702069 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 10:48:36 -0600 Subject: [PATCH 07/35] workinonit --- src/foundation/connected-types.lagda.md | 3 +- .../suspensions-of-types.lagda.md | 40 +++++++++++++------ .../finitely-enumerable-types.lagda.md | 25 +++++++++--- 3 files changed, 49 insertions(+), 19 deletions(-) diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md index 0cc9114604..ce446bc478 100644 --- a/src/foundation/connected-types.lagda.md +++ b/src/foundation/connected-types.lagda.md @@ -273,7 +273,8 @@ module _ ``` In particular, inhabited types are `-1`-connected; their identity types are -`-2`-connected, as all types are. +`-2`-connected, as all types are. This characterizes the `-1`-connected types, +i.e. `X` is `-1`-connected iff it's inhabited. ```agda is-neg-one-connected-is-inhabited : diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 2c593c51ef..2814fc5e18 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -1,6 +1,8 @@ # Suspensions of types ```agda +{-# OPTIONS --lossy-unification #-} + module synthetic-homotopy-theory.suspensions-of-types where ``` @@ -28,6 +30,7 @@ open import foundation.fibers-of-maps open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-function-types +open import foundation.mere-equality open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types @@ -84,7 +87,7 @@ type `X` is the [pushout](synthetic-homotopy-theory.pushouts.md) of the ``` Suspensions play an important role in synthetic homotopy theory. For example, -they star in the freudenthal suspension theorem and give us a definition of +they star in the Freudenthal suspension theorem and give us a definition of [the spheres](synthetic-homotopy-theory.spheres.md). ## Definitions @@ -763,11 +766,11 @@ module _ ### `Σ X` is 0-connected iff `X` is inhabited -Note that `Σ empty = bool` is not `0`-connected. +Note that `Σ empty ＝ bool` is _not_ `0`-connected. The forward direction is the subtle one. When `Σ X` is 0-connected, then in -particular we merely have `p ∈ north-suspension ＝ south-suspension`; such -identifications are inductively generated by `X`. +particular we merely have `p ∈ north ＝ south`; such identifications are +inductively generated by `X`. ```agda suspension-is-0-connected-is-inhabited : @@ -778,8 +781,11 @@ suspension-is-0-connected-is-inhabited X x = is-inhabited-suspension-is-0-connected : {l : Level} (X : UU l) → is-0-connected (suspension X) → is-inhabited X -is-inhabited-suspension-is-0-connected X p = - unit-trunc-Prop {! !} +is-inhabited-suspension-is-0-connected X ΣX-conn = + rec-trunc-Prop (is-inhabited-Prop X) (λ h → {! !}) p + where + p : mere-eq (north-suspension {X = X}) (south-suspension {X = X}) + p = mere-eq-is-0-connected ΣX-conn north-suspension south-suspension ``` In fact, the following are logically equivalent: @@ -794,11 +800,11 @@ inhabited, its suspension is 0-connected, and 0-truncated 0-connected types are contractible and hence are `Fin 1`. (<-): Such a cardinality can only be 1 or 2 - suspensions are inhabited, say, by -`north-suspension`, and the cardinality of a type finitely enumerated by -`Fin 2 = bool` can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` -is 0-connected, then it follows that `Σ X` is also 0-connected, therefore that -`X` is inhabited. When it's 2, i.e. when there are no identifications -`north = south` in `Σ X`, then `X` better have been empty. +`north`, and the cardinality of a type finitely enumerated by `Fin 2 ＝ bool` +can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` is 0-connected +and hence contractible, well, this is the definition of 0-connectedness of +`Σ X`, and therefore `X` is inhabited. When it's 2, i.e. when there are no +identifications `north ＝ south` in `Σ X`, then `X` better have been empty. ```agda module _ @@ -853,8 +859,16 @@ module _ is-finite (type-trunc-Set (suspension X)) → is-inhabited-or-empty X is-inhabited-or-empty-is-finite-suspension p with number-of-elements-is-finite p ... | 0 = - ex-falso (is-nonempty-is-inhabited (is-inhabited-suspension X) (is-empty-set-truncation-is-empty (is-empty-is-zero-number-of-elements-is-finite p {! !}))) - ... | 1 = inl (is-inhabited-suspension-is-0-connected X {! !}) + ex-falso + ( is-nonempty-is-inhabited + ( is-inhabited-suspension X) + ( is-empty-set-truncation-is-empty + ( is-empty-is-zero-number-of-elements-is-finite p {! !}))) + ... | 1 = + inl + ( is-inhabited-suspension-is-0-connected + ( X) + ( is-contr-is-one-number-of-elements-is-finite p {! !})) ... | 2 = inr (is-empty-trunc-suspension-has-two-elements {! !}) ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! !} ``` diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index 1367badbff..8253a19870 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -1,7 +1,7 @@ # Finitely enumerable types ```agda -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --allow-unsolved-metas --lossy-unification #-} module univalent-combinatorics.finitely-enumerable-types where ``` @@ -9,7 +9,7 @@ module univalent-combinatorics.finitely-enumerable-types where
Imports ```agda -open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.strict-inequality-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers @@ -22,6 +22,7 @@ open import foundation.decidable-equality open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.equivalences +open import foundation.negation open import foundation.existential-quantification open import foundation.fibers-of-maps open import foundation.function-types @@ -132,10 +133,24 @@ is-upper-bound-finite-enumeration : {l : Level} (X : UU l) → (eq : has-decidable-equality X) → (f : finite-enumeration X) → - leq-ℕ - (number-of-elements-count (count-finite-enumeration-discrete eq f)) + ¬ le-ℕ (cardinality-finite-enumeration X f) -is-upper-bound-finite-enumeration X eq (n , f) = {! !} + (number-of-elements-count (count-finite-enumeration-discrete eq f)) +is-upper-bound-finite-enumeration X eq (0 , f) p = + tr (le-ℕ (cardinality-finite-enumeration X (0 , f))) h p + where + h : + number-of-elements-count (count-finite-enumeration-discrete eq (0 , f)) ＝ 0 + h = + eq-cardinality + ( {! !}) + ( unit-trunc-Prop + ( equiv-is-empty + ( λ ()) + ( is-empty-surjection-empty + ( λ ()) + ( f)))) +is-upper-bound-finite-enumeration X eq (succ-ℕ n , f) p = {! !} ``` ### Finite types are finitely enumerable From e77977a3d6981d24263120de2c009c056159fe14 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 10:50:09 -0600 Subject: [PATCH 08/35] pre-commit hygeine --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 2 +- .../finitely-enumerable-types.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 2814fc5e18..567ef147bd 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -30,11 +30,11 @@ open import foundation.fibers-of-maps open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-function-types -open import foundation.mere-equality open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.inhabited-types +open import foundation.mere-equality open import foundation.mere-equivalences open import foundation.propositional-truncations open import foundation.propositions diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index 8253a19870..41f70304ab 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -9,9 +9,9 @@ module univalent-combinatorics.finitely-enumerable-types where
Imports ```agda -open import elementary-number-theory.strict-inequality-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 open import foundation.action-on-identifications-functions open import foundation.booleans @@ -22,7 +22,6 @@ open import foundation.decidable-equality open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.equivalences -open import foundation.negation open import foundation.existential-quantification open import foundation.fibers-of-maps open import foundation.function-types @@ -30,6 +29,7 @@ open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-coproduct-types open import foundation.identity-types open import foundation.logical-equivalences +open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions open import foundation.raising-universe-levels From b24a60d2bdf1d4954f0493cbaf62e583054bed54 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 11:08:07 -0600 Subject: [PATCH 09/35] added link for mere equality --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 567ef147bd..5b3995d3bd 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -769,8 +769,8 @@ module _ Note that `Σ empty ＝ bool` is _not_ `0`-connected. The forward direction is the subtle one. When `Σ X` is 0-connected, then in -particular we merely have `p ∈ north ＝ south`; such identifications are -inductively generated by `X`. +particular we [merely](foundation.mere-equality.md) have `p ∈ north ＝ south`; +such identifications are inductively generated by `X`. ```agda suspension-is-0-connected-is-inhabited : From 6f2033144b31b5bea0562b71ac95894a8238edd6 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 11:16:48 -0600 Subject: [PATCH 10/35] fixed inference issue in bool equivalence --- .../suspensions-of-types.lagda.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 5b3995d3bd..8f174b78a4 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -619,15 +619,17 @@ module _ compute-south-cogap-suspension suspension-structure-empty-bool compute-north-suspension-empty-bool : - (map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension) - north-suspension + ( map-surjection-bool-suspension {X = X} ∘ + inv-map-surjection-bool-suspension) + north-suspension ＝ north-suspension compute-north-suspension-empty-bool = ap map-surjection-bool-suspension compute-true-suspension-empty-bool compute-south-suspension-empty-bool : - (map-surjection-bool-suspension ∘ inv-map-surjection-bool-suspension) - south-suspension + ( map-surjection-bool-suspension {X = X} ∘ + inv-map-surjection-bool-suspension) + south-suspension ＝ south-suspension compute-south-suspension-empty-bool = ap map-surjection-bool-suspension compute-false-suspension-empty-bool From c2709108db7b90a889393a68e174fb38a925d2f2 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 11:21:52 -0600 Subject: [PATCH 11/35] typo --- src/univalent-combinatorics/2-element-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md index b44650d1ca..5575e20b50 100644 --- a/src/univalent-combinatorics/2-element-types.lagda.md +++ b/src/univalent-combinatorics/2-element-types.lagda.md @@ -203,7 +203,7 @@ pr1 (extensionality-2-Element-Type X Y) = equiv-eq-2-Element-Type X Y pr2 (extensionality-2-Element-Type X Y) = is-equiv-equiv-eq-2-Element-Type X Y ``` -### Characterization the identifications of `Fin 2` with a `2`-element type `X` +### Characterizing the identifications of `Fin 2` with a `2`-element type `X` #### Evaluating an equivalence and an automorphism at `0 : Fin 2` From 0a174cf5e5b7c33ced86593bf26d13e54f0bd0f2 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 11:23:53 -0600 Subject: [PATCH 12/35] with abstraction is being finnicky, surprised refl doesn't work here --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 8f174b78a4..bf96764a64 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -865,12 +865,12 @@ module _ ( is-nonempty-is-inhabited ( is-inhabited-suspension X) ( is-empty-set-truncation-is-empty - ( is-empty-is-zero-number-of-elements-is-finite p {! !}))) + ( is-empty-is-zero-number-of-elements-is-finite p {! refl !}))) ... | 1 = inl ( is-inhabited-suspension-is-0-connected ( X) - ( is-contr-is-one-number-of-elements-is-finite p {! !})) + ( is-contr-is-one-number-of-elements-is-finite p {! refl !})) ... | 2 = inr (is-empty-trunc-suspension-has-two-elements {! !}) ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! !} ``` From 7a1d589709f940f1aaf55efb48633f8218944c0d Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 11:27:51 -0600 Subject: [PATCH 13/35] anonymized unused lambda variable --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index bf96764a64..2708b3e546 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -847,7 +847,7 @@ module _ is-empty-trunc-suspension-has-two-elements p x = intro-double-negation ( ap unit-trunc-Set (meridian-suspension x)) - ( λ q → is-not-one-two-ℕ (eq-cardinality p (unit-trunc-Prop eq))) + ( λ _ → is-not-one-two-ℕ (eq-cardinality p (unit-trunc-Prop eq))) where eq : Fin 1 ≃ type-trunc-Set (suspension X) pr1 eq (inr star) = unit-trunc-Set north-suspension From 4f972c914a7fe72ab64115a8ba5791c8695a4076 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 11:50:42 -0600 Subject: [PATCH 14/35] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- src/foundation/connected-types.lagda.md | 2 +- src/foundation/surjective-maps.lagda.md | 2 +- src/synthetic-homotopy-theory/acyclic-types.lagda.md | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md index ce446bc478..160d65fa7d 100644 --- a/src/foundation/connected-types.lagda.md +++ b/src/foundation/connected-types.lagda.md @@ -274,7 +274,7 @@ module _ In particular, inhabited types are `-1`-connected; their identity types are `-2`-connected, as all types are. This characterizes the `-1`-connected types, -i.e. `X` is `-1`-connected iff it's inhabited. +i.e., `X` is `-1`-connected iff it's inhabited. ```agda is-neg-one-connected-is-inhabited : diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 136f23d5e5..a797b01cee 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -874,7 +874,7 @@ module _ is-inhabited-is-surjective (is-surjective-map-surjection f) ``` -### When `X` is empty and `X` surjects onto `Y`, then `Y` is empty +### Empty types are closed under surjections ```agda module _ diff --git a/src/synthetic-homotopy-theory/acyclic-types.lagda.md b/src/synthetic-homotopy-theory/acyclic-types.lagda.md index ad94fffefb..15e3214912 100644 --- a/src/synthetic-homotopy-theory/acyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-types.lagda.md @@ -83,8 +83,8 @@ is-acyclic-unit = is-acyclic-is-contr unit is-contr-unit ### Acyclic types are inhabited -Proof: `Σ X` is 0-connected if and only if `X` is inhabited, and contractible -types are of course 0-connected. +**Proof.** `Σ X` is 0-connected if and only if `X` is inhabited, and contractible +types are of course 0-connected. ∎ ```agda is-inhabited-is-acyclic : {l : Level} (A : UU l) → is-acyclic A → is-inhabited A From 042ce863e4a31b6b5b348dfe97328c976a2d66c8 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 12:08:14 -0600 Subject: [PATCH 15/35] acyclic/epimorphic maps are surjective --- .../acyclic-maps.lagda.md | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index a37d589205..2e8e5a9c3c 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -22,6 +22,7 @@ open import foundation.epimorphisms open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-extensionality +open import foundation.surjective-maps open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types @@ -127,6 +128,29 @@ module _ ( ac b))) ``` +### Acyclic maps are surjective + +Hence, epimorphisms are surjective. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + abstract + is-surjective-is-acyclic-map : is-acyclic-map f → is-surjective f + is-surjective-is-acyclic-map ac x = + is-inhabited-is-acyclic + ( fiber f x) + ( ac x) + + is-surjective-is-epimorphism : is-epimorphism f → is-surjective f + is-surjective-is-epimorphism epi x = + is-inhabited-is-acyclic + ( fiber f x) + ( is-acyclic-map-is-epimorphism f epi x) +``` + ### A type is acyclic if and only if its terminal map is an acyclic map ```agda From 9e0028ea22aeb87fce6f02b245162cf7c8021641 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 12:08:31 -0600 Subject: [PATCH 16/35] allowed unsolved metas, for the time being --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 2708b3e546..0e9f2a0272 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -1,7 +1,7 @@ # Suspensions of types ```agda -{-# OPTIONS --lossy-unification #-} +{-# OPTIONS --lossy-unification --allow-unsolved-metas #-} module synthetic-homotopy-theory.suspensions-of-types where ``` From 6cdc190896b24a31fa591fb637f0b1783224974c Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 12:14:37 -0600 Subject: [PATCH 17/35] qed --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 0e9f2a0272..f91ebff6eb 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -806,7 +806,7 @@ contractible and hence are `Fin 1`. can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` is 0-connected and hence contractible, well, this is the definition of 0-connectedness of `Σ X`, and therefore `X` is inhabited. When it's 2, i.e. when there are no -identifications `north ＝ south` in `Σ X`, then `X` better have been empty. +identifications `north ＝ south` in `Σ X`, then `X` better have been empty. ∎ ```agda module _ From 11b496aa89e2365a9614096528cb363bdcc42e2a Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 12:17:28 -0600 Subject: [PATCH 18/35] formatting --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index f91ebff6eb..3737451ec1 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -795,7 +795,7 @@ In fact, the following are logically equivalent: - `X` is [inhabited or empty](logic.propositionally-decidable-types.md) - `trunc-Set (Σ X)` is [finite](univalent-combinatorics.finite-types.md) -Proof: +**Proof.** (->): When `X` is empty, its suspension is the set `Fin 2`. When `X` is inhabited, its suspension is 0-connected, and 0-truncated 0-connected types are From 13f94a0ba606d80552e55b0533ee9e71a6a30a07 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 14:02:45 -0600 Subject: [PATCH 19/35] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 4 ++++ .../finitely-enumerable-types.lagda.md | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 3737451ec1..fb59eb8d10 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -874,3 +874,7 @@ module _ ... | 2 = inr (is-empty-trunc-suspension-has-two-elements {! !}) ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! !} ``` + +## See also + +- [Suspensions of propositions](synthetic-homotopy-theory.suspensions-of-propositions.md) diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index 41f70304ab..10471fdf76 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -133,9 +133,9 @@ is-upper-bound-finite-enumeration : {l : Level} (X : UU l) → (eq : has-decidable-equality X) → (f : finite-enumeration X) → - ¬ le-ℕ - (cardinality-finite-enumeration X f) + leq-ℕ (number-of-elements-count (count-finite-enumeration-discrete eq f)) + (cardinality-finite-enumeration X f) is-upper-bound-finite-enumeration X eq (0 , f) p = tr (le-ℕ (cardinality-finite-enumeration X (0 , f))) h p where From 1d147b5eb68a50b9347cbb59db599124645348fc Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 14:03:28 -0600 Subject: [PATCH 20/35] suspensions almost commute with propositional truncations --- .../suspensions-of-propositions.lagda.md | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md index 35f8ab47d9..103329c4c2 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md @@ -19,6 +19,8 @@ open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.sets +open import foundation.set-truncations +open import foundation.propositional-truncations open import foundation.subsingleton-induction open import foundation.surjective-maps open import foundation.torsorial-type-families @@ -487,6 +489,28 @@ module _ ( surjection-equiv equiv-bool-Fin-2)) ``` +### Suspensions _almost_ commute with propositional truncations + +The problem is that empty types suspend to a two-element set. This is easily +fixed by adjusting the truncation level, and we do have that +`Σ (trunc-Prop X) = trunc-Set (Σ X)`. + +```agda +module _ + {l : Level} (X : UU l) + where + + suspension-structure-suspension-trunc-prop-trunc-set-suspension : + suspension-structure (type-trunc-Prop X) (type-trunc-Set (suspension X)) + pr1 suspension-structure-suspension-trunc-prop-trunc-set-suspension = {! !} + pr1 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) = {! !} + pr2 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) = {! !} + + suspension-trunc-prop-trunc-set-suspension : + suspension (type-trunc-Prop X) → type-trunc-Set (suspension X) + suspension-trunc-prop-trunc-set-suspension = cogap-suspension {! !} +``` + ## See also - Suspensions of propositions are used in the proof of From 1bfd42e7ba33768f26399b45f321fca1de4fd0f7 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 14:36:50 -0600 Subject: [PATCH 21/35] making progress in suspensions of propositions on the almost-commuting lemma --- .../suspensions-of-propositions.lagda.md | 89 ++++++++++++++++++- 1 file changed, 85 insertions(+), 4 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md index 103329c4c2..276debf2a9 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md @@ -9,6 +9,7 @@ module synthetic-homotopy-theory.suspensions-of-propositions where ```agda open import foundation.booleans open import foundation.contractible-types +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.existential-quantification @@ -502,13 +503,93 @@ module _ suspension-structure-suspension-trunc-prop-trunc-set-suspension : suspension-structure (type-trunc-Prop X) (type-trunc-Set (suspension X)) - pr1 suspension-structure-suspension-trunc-prop-trunc-set-suspension = {! !} - pr1 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) = {! !} - pr2 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) = {! !} + pr1 suspension-structure-suspension-trunc-prop-trunc-set-suspension = + unit-trunc-Set north-suspension + pr1 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) = + unit-trunc-Set south-suspension + pr2 (pr2 suspension-structure-suspension-trunc-prop-trunc-set-suspension) = + rec-trunc-Prop + ( Id-Prop + ( trunc-Set (suspension X)) + ( unit-trunc-Set north-suspension) + ( unit-trunc-Set south-suspension)) + ( λ x → ap unit-trunc-Set (meridian-suspension x)) suspension-trunc-prop-trunc-set-suspension : suspension (type-trunc-Prop X) → type-trunc-Set (suspension X) - suspension-trunc-prop-trunc-set-suspension = cogap-suspension {! !} + suspension-trunc-prop-trunc-set-suspension = + cogap-suspension + ( suspension-structure-suspension-trunc-prop-trunc-set-suspension) + + suspension-structure-trunc-set-suspension-suspension-trunc-prop : + suspension-structure X (suspension (type-trunc-Prop X)) + pr1 suspension-structure-trunc-set-suspension-suspension-trunc-prop = + north-suspension + pr1 (pr2 suspension-structure-trunc-set-suspension-suspension-trunc-prop) = + south-suspension + pr2 (pr2 suspension-structure-trunc-set-suspension-suspension-trunc-prop) x = + meridian-suspension (unit-trunc-Prop x) + + trunc-set-suspension-suspension-trunc-prop : + type-trunc-Set (suspension X) → suspension (type-trunc-Prop X) + trunc-set-suspension-suspension-trunc-prop = + map-universal-property-trunc-Set + ( suspension-set-Prop (trunc-Prop X)) + ( cogap-suspension + suspension-structure-trunc-set-suspension-suspension-trunc-prop) + + dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension : + dependent-suspension-structure + ( λ z → + ( trunc-set-suspension-suspension-trunc-prop ∘ + suspension-trunc-prop-trunc-set-suspension) + ( z) + ＝ z) + ( suspension-structure-suspension (type-trunc-Prop X)) + pr1 dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension = + ap trunc-set-suspension-suspension-trunc-prop {! !} ∙ {! !} + pr1 (pr2 dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension) = + ap trunc-set-suspension-suspension-trunc-prop {! !} ∙ {! !} + pr2 (pr2 dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension) x = + eq-is-prop {! is-set !} + + suspension-structure-eq-trunc-set-suspension : + (x : type-trunc-Set (suspension X)) → + suspension-structure + (X) + ((suspension-trunc-prop-trunc-set-suspension ∘ + trunc-set-suspension-suspension-trunc-prop) + x ＝ + x) + pr1 (suspension-structure-eq-trunc-set-suspension x) = {! !} + pr1 (pr2 (suspension-structure-eq-trunc-set-suspension x)) = {! !} + pr2 (pr2 (suspension-structure-eq-trunc-set-suspension x)) = {! !} + + is-equiv-suspension-trunc-prop-trunc-set-suspension : + is-equiv suspension-trunc-prop-trunc-set-suspension + pr1 (pr1 is-equiv-suspension-trunc-prop-trunc-set-suspension) = + trunc-set-suspension-suspension-trunc-prop + pr2 (pr1 is-equiv-suspension-trunc-prop-trunc-set-suspension) x = + apply-universal-property-trunc-Set + ( set-Prop + ( Id-Prop + ( trunc-Set (suspension X)) + ( ( suspension-trunc-prop-trunc-set-suspension ∘ + trunc-set-suspension-suspension-trunc-prop) + x) + ( x))) + ( x) + ( cogap-suspension (suspension-structure-eq-trunc-set-suspension x)) + pr1 (pr2 is-equiv-suspension-trunc-prop-trunc-set-suspension) = + trunc-set-suspension-suspension-trunc-prop + pr2 (pr2 is-equiv-suspension-trunc-prop-trunc-set-suspension) = + dependent-cogap-suspension + ( λ z → + ( trunc-set-suspension-suspension-trunc-prop ∘ + suspension-trunc-prop-trunc-set-suspension) + ( z) + ＝ z) + ( dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension) ``` ## See also From 4833e027f4d3df07b73bd6022218b75ad1b3b28a Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 15:03:41 -0600 Subject: [PATCH 22/35] there remain some computations to do by hand --- .../suspensions-of-propositions.lagda.md | 26 ++++++++++++++----- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md index 276debf2a9..9fa972b1f0 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md @@ -538,7 +538,7 @@ module _ ( cogap-suspension suspension-structure-trunc-set-suspension-suspension-trunc-prop) - dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension : + dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension : dependent-suspension-structure ( λ z → ( trunc-set-suspension-suspension-trunc-prop ∘ @@ -546,12 +546,18 @@ module _ ( z) ＝ z) ( suspension-structure-suspension (type-trunc-Prop X)) - pr1 dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension = + pr1 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension = ap trunc-set-suspension-suspension-trunc-prop {! !} ∙ {! !} - pr1 (pr2 dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension) = + pr1 (pr2 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension) = ap trunc-set-suspension-suspension-trunc-prop {! !} ∙ {! !} - pr2 (pr2 dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension) x = - eq-is-prop {! is-set !} + pr2 (pr2 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension) _ = + eq-is-prop + ( is-set-suspension-Prop + ( trunc-Prop X) + ( ( trunc-set-suspension-suspension-trunc-prop ∘ + suspension-trunc-prop-trunc-set-suspension) + ( south-suspension)) + ( south-suspension)) suspension-structure-eq-trunc-set-suspension : (x : type-trunc-Set (suspension X)) → @@ -563,7 +569,13 @@ module _ x) pr1 (suspension-structure-eq-trunc-set-suspension x) = {! !} pr1 (pr2 (suspension-structure-eq-trunc-set-suspension x)) = {! !} - pr2 (pr2 (suspension-structure-eq-trunc-set-suspension x)) = {! !} + pr2 (pr2 (suspension-structure-eq-trunc-set-suspension x)) _ = + eq-is-prop + ( is-set-type-trunc-Set + ( ( suspension-trunc-prop-trunc-set-suspension ∘ + trunc-set-suspension-suspension-trunc-prop) + ( x)) + ( x)) is-equiv-suspension-trunc-prop-trunc-set-suspension : is-equiv suspension-trunc-prop-trunc-set-suspension @@ -589,7 +601,7 @@ module _ suspension-trunc-prop-trunc-set-suspension) ( z) ＝ z) - ( dependent-suspension-structure-retraction-suspension-trunc-prop-trunc-set-suspension) + ( dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension) ``` ## See also From a42a827a38ea6f60f49300657716877c51591025 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 15:05:05 -0600 Subject: [PATCH 23/35] back to this version --- .../finitely-enumerable-types.lagda.md | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index 10471fdf76..3bf6c5bad0 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -11,7 +11,7 @@ module univalent-combinatorics.finitely-enumerable-types where ```agda open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers -open import elementary-number-theory.strict-inequality-natural-numbers +open import elementary-number-theory.inequality-natural-numbers open import foundation.action-on-identifications-functions open import foundation.booleans @@ -136,21 +136,7 @@ is-upper-bound-finite-enumeration : leq-ℕ (number-of-elements-count (count-finite-enumeration-discrete eq f)) (cardinality-finite-enumeration X f) -is-upper-bound-finite-enumeration X eq (0 , f) p = - tr (le-ℕ (cardinality-finite-enumeration X (0 , f))) h p - where - h : - number-of-elements-count (count-finite-enumeration-discrete eq (0 , f)) ＝ 0 - h = - eq-cardinality - ( {! !}) - ( unit-trunc-Prop - ( equiv-is-empty - ( λ ()) - ( is-empty-surjection-empty - ( λ ()) - ( f)))) -is-upper-bound-finite-enumeration X eq (succ-ℕ n , f) p = {! !} +is-upper-bound-finite-enumeration X eq f = {! !} ``` ### Finite types are finitely enumerable From e830721d9e925b83c02145a94d1195117d3b7cf3 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 15:09:26 -0600 Subject: [PATCH 24/35] citation needed --- src/univalent-combinatorics/finitely-enumerable-types.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index 3bf6c5bad0..c611533871 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -126,7 +126,8 @@ is-finite-is-finitely-enumerable-discrete D eX = ``` We can say more: the cardinality of `X` enumerated by `Fin n` is bounded above -by `n`. +by `n`. This is a dual +[pigeonhole principle](univalent-combinatorics.pigeonhole-principle.md). ```agda is-upper-bound-finite-enumeration : From 509a7c26a3ed5d1014c8582b2467b7826595b73e Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Fri, 29 Aug 2025 15:36:41 -0600 Subject: [PATCH 25/35] Update src/foundation/surjective-maps.lagda.md Co-authored-by: Fredrik Bakke --- src/foundation/surjective-maps.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index a797b01cee..134fc44e7e 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -881,8 +881,8 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (emp-A : is-empty A) where - is-empty-surjection-empty : A ↠ B → is-empty B - is-empty-surjection-empty (f , p) b = + is-empty-surjection : A ↠ B → is-empty B + is-empty-surjection (f , p) b = rec-trunc-Prop empty-Prop (λ (a , q) → emp-A a) (p b) ``` From 35fc0253b5c505ce06a3194c96d902683d7278e1 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 31 Aug 2025 19:08:36 -0600 Subject: [PATCH 26/35] typo --- src/univalent-combinatorics/finite-choice.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/univalent-combinatorics/finite-choice.lagda.md b/src/univalent-combinatorics/finite-choice.lagda.md index 43f0971a20..1713e5712f 100644 --- a/src/univalent-combinatorics/finite-choice.lagda.md +++ b/src/univalent-combinatorics/finite-choice.lagda.md @@ -42,7 +42,7 @@ open import univalent-combinatorics.standard-finite-types ## Idea -[Propositional truncations](foundation.propositional-truncations.md) distributes +[Propositional truncations](foundation.propositional-truncations.md) distribute over finite products. ## Theorems From c6675763362711b7855d4cebe91e32d41f9cb7b3 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 31 Aug 2025 20:50:34 -0600 Subject: [PATCH 27/35] a bit of section infrastructure --- src/foundation/sections.lagda.md | 45 ++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/src/foundation/sections.lagda.md b/src/foundation/sections.lagda.md index 0c9cd52162..e28ca21460 100644 --- a/src/foundation/sections.lagda.md +++ b/src/foundation/sections.lagda.md @@ -20,6 +20,7 @@ open import foundation.whiskering-homotopies-composition open import foundation-core.contractible-types open import foundation-core.equivalences +open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies @@ -187,4 +188,48 @@ is-injective-map-section-family : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (b : (x : A) → B x) → is-injective (map-section-family b) is-injective-map-section-family b = ap pr1 + +injection-map-section-family : + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (b : (x : A) → B x) → + injection A (Σ A B) +pr1 (injection-map-section-family b) = map-section-family b +pr2 (injection-map-section-family b) = is-injective-map-section-family b +``` + +### The space of sections of `f : A → B` is equivalent to the space of dependent maps `(b : B) → fiber f b` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + section-dependent-fiber : section f → (b : B) → fiber f b + pr1 (section-dependent-fiber (g , s) b) = g b + pr2 (section-dependent-fiber (g , s) b) = s b + + dependent-fiber-section : ((b : B) → fiber f b) → section f + pr1 (dependent-fiber-section g) b = pr1 (g b) + pr2 (dependent-fiber-section g) b = pr2 (g b) + + equiv-section-dependent-fiber : + section f ≃ ((b : B) → fiber f b) + pr1 equiv-section-dependent-fiber = section-dependent-fiber + pr1 (pr1 (pr2 equiv-section-dependent-fiber)) = dependent-fiber-section + pr2 (pr1 (pr2 equiv-section-dependent-fiber)) = refl-htpy + pr1 (pr2 (pr2 equiv-section-dependent-fiber)) = dependent-fiber-section + pr2 (pr2 (pr2 equiv-section-dependent-fiber)) = refl-htpy +``` + +### Sections are injective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + is-injective-is-section : (g : B → A) → is-section f g → is-injective g + is-injective-is-section g s {x} {y} eq = inv (s x) ∙ ap f eq ∙ s y + + injection-section : section f → injection B A + injection-section (g , s) = (g , is-injective-is-section g s) ``` From d0337dc232236d0632bdf336c9b13875417262cb Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 31 Aug 2025 20:50:53 -0600 Subject: [PATCH 28/35] from an injection to the leq --- src/univalent-combinatorics/pigeonhole-principle.lagda.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md index dc8a1e1e99..40cd35cf33 100644 --- a/src/univalent-combinatorics/pigeonhole-principle.lagda.md +++ b/src/univalent-combinatorics/pigeonhole-principle.lagda.md @@ -206,6 +206,11 @@ module _ 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) + + leq-injection-count : + (f : injection A B) → + number-of-elements-count eA ≤-ℕ number-of-elements-count eB + leq-injection-count (f , inj) = leq-is-injective-count inj ``` #### There is no embedding `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` From 6602fd84bfa63bb3d3dd246e3bded548dc196ee2 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 31 Aug 2025 20:51:06 -0600 Subject: [PATCH 29/35] running into issues with implicit/explicit functions... --- .../finitely-enumerable-types.lagda.md | 53 ++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index b99cc12b74..5c29dff5ea 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -20,6 +20,7 @@ open import foundation.conjunction open import foundation.coproduct-types open import foundation.decidable-equality open import foundation.dependent-pair-types +open import foundation.existential-quantification open import foundation.embeddings open import foundation.equality-cartesian-product-types open import foundation.equivalences @@ -33,8 +34,11 @@ open import foundation.identity-types open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations +open import foundation.injective-maps +open import foundation.inhabited-types open import foundation.propositions open import foundation.raising-universe-levels +open import foundation.sections open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.type-arithmetic-booleans @@ -51,7 +55,9 @@ open import univalent-combinatorics.counting-decidable-subtypes open import univalent-combinatorics.counting-dependent-pair-types open import univalent-combinatorics.dedekind-finite-types open import univalent-combinatorics.finite-types +open import univalent-combinatorics.finite-choice open import univalent-combinatorics.standard-finite-types +open import univalent-combinatorics.pigeonhole-principle open import univalent-combinatorics.subfinitely-enumerable-types open import univalent-combinatorics.surjective-maps ``` @@ -84,6 +90,18 @@ module _ cardinality-finite-enumeration : finite-enumeration → ℕ cardinality-finite-enumeration (n , _) = n + surjection-finite-enumeration : + (f : finite-enumeration) → Fin (cardinality-finite-enumeration f) ↠ X + surjection-finite-enumeration (n , f) = f + + map-finite-enumeration : + (f : finite-enumeration) → Fin (cardinality-finite-enumeration f) → X + map-finite-enumeration f = map-surjection (surjection-finite-enumeration f) + + is-surjective-finite-enumeration : + (f : finite-enumeration) → is-surjective (map-finite-enumeration f) + is-surjective-finite-enumeration (n , f) = is-surjective-map-surjection f + Finitely-Enumerable-Type : (l : Level) → UU (lsuc l) Finitely-Enumerable-Type l = type-subtype (is-finitely-enumerable-prop {l}) @@ -134,6 +152,31 @@ by `n`. This is a dual [pigeonhole principle](univalent-combinatorics.pigeonhole-principle.md). ```agda +has-section-has-decidable-equality-finite-enumeration : + {l : Level} (X : UU l) (eq : has-decidable-equality X) + (f : finite-enumeration X) → + is-inhabited ((x : X) → fiber (map-finite-enumeration X f) x) +has-section-has-decidable-equality-finite-enumeration X eq f = + finite-choice + ( is-finite-is-finitely-enumerable-discrete eq (unit-trunc-Prop f)) + ( is-surjective-finite-enumeration X f) + +has-injective-map-is-upper-bound-finite-enumeration : + {l : Level} (X : UU l) (eq : has-decidable-equality X) + (f : finite-enumeration X) → + exists + (X → Fin (cardinality-finite-enumeration X f)) + (is-injective-Prop (is-set-has-decidable-equality eq)) +has-injective-map-is-upper-bound-finite-enumeration X eq f = + rec-trunc-Prop + ( ∃ + ( X → Fin (cardinality-finite-enumeration X f)) + ( is-injective-Prop (is-set-has-decidable-equality eq))) + ( λ g → unit-trunc-Prop + ( ( λ x → inclusion-fiber (map-finite-enumeration X f) (g x)) , + ( {! is-injective-is-section !}))) + ( has-section-has-decidable-equality-finite-enumeration X eq f) + is-upper-bound-finite-enumeration : {l : Level} (X : UU l) → (eq : has-decidable-equality X) → @@ -141,7 +184,15 @@ is-upper-bound-finite-enumeration : leq-ℕ (number-of-elements-count (count-finite-enumeration-discrete eq f)) (cardinality-finite-enumeration X f) -is-upper-bound-finite-enumeration X eq f = {! !} +is-upper-bound-finite-enumeration X eq f = + rec-trunc-Prop + ( leq-ℕ-Prop + ( number-of-elements-count (count-finite-enumeration-discrete eq f)) + ( cardinality-finite-enumeration X f)) + ( leq-injection-count + ( count-finite-enumeration-discrete eq f) + ( count-Fin (cardinality-finite-enumeration X f))) + ( has-injective-map-is-upper-bound-finite-enumeration X eq f) ``` ### Finite types are finitely enumerable From 64c46c54eef8f991766d7c2a70a69e240d42796e Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sun, 31 Aug 2025 20:54:59 -0600 Subject: [PATCH 30/35] oof! --- src/univalent-combinatorics/finitely-enumerable-types.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index 5c29dff5ea..b809050655 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -174,7 +174,7 @@ has-injective-map-is-upper-bound-finite-enumeration X eq f = ( is-injective-Prop (is-set-has-decidable-equality eq))) ( λ g → unit-trunc-Prop ( ( λ x → inclusion-fiber (map-finite-enumeration X f) (g x)) , - ( {! is-injective-is-section !}))) + ( is-injective-is-section {! !} {! !} {! !}))) ( has-section-has-decidable-equality-finite-enumeration X eq f) is-upper-bound-finite-enumeration : From 4c31c183c69deafeeb4af12aa19d38dba192c998 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Tue, 2 Sep 2025 14:56:51 -0600 Subject: [PATCH 31/35] got it for 0, 1, 2!! --- .../suspensions-of-types.lagda.md | 20 ++++++++++++++----- .../finite-types.lagda.md | 12 +++++++++++ .../finitely-enumerable-types.lagda.md | 2 +- 3 files changed, 28 insertions(+), 6 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index fb59eb8d10..fa48e8f1ab 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -795,6 +795,9 @@ In fact, the following are logically equivalent: - `X` is [inhabited or empty](logic.propositionally-decidable-types.md) - `trunc-Set (Σ X)` is [finite](univalent-combinatorics.finite-types.md) +Note the relationship with this and +[Diaconescu's theorem](foundation.diaconescus-theorem.md). + **Proof.** (->): When `X` is empty, its suspension is the set `Fin 2`. When `X` is @@ -859,20 +862,27 @@ module _ is-inhabited-or-empty-is-finite-suspension : is-finite (type-trunc-Set (suspension X)) → is-inhabited-or-empty X - is-inhabited-or-empty-is-finite-suspension p with number-of-elements-is-finite p + is-inhabited-or-empty-is-finite-suspension p with number-of-elements-is-finite p in eq ... | 0 = ex-falso ( is-nonempty-is-inhabited ( is-inhabited-suspension X) ( is-empty-set-truncation-is-empty - ( is-empty-is-zero-number-of-elements-is-finite p {! refl !}))) + ( is-empty-is-zero-number-of-elements-is-finite p eq))) ... | 1 = inl ( is-inhabited-suspension-is-0-connected ( X) - ( is-contr-is-one-number-of-elements-is-finite p {! refl !})) - ... | 2 = inr (is-empty-trunc-suspension-has-two-elements {! !}) - ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! !} + ( is-contr-is-one-number-of-elements-is-finite p eq)) + ... | 2 = + inr + ( is-empty-trunc-suspension-has-two-elements + ( map-inv-equiv-has-cardinality-id-number-of-elements-is-finite + ( type-trunc-Set (suspension X)) + ( p) + ( 2) + ( eq))) + ... | succ-ℕ (succ-ℕ (succ-ℕ n)) = ex-falso {! is-upper-bound-finite-enumeration !} ``` ## See also diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index ab9b151fe7..bc2bb88f8a 100644 --- a/src/univalent-combinatorics/finite-types.lagda.md +++ b/src/univalent-combinatorics/finite-types.lagda.md @@ -772,6 +772,18 @@ abstract ( λ m → has-cardinality-ℕ m X) ( p) ( pr2 (has-finite-cardinality-is-finite H))) + + map-equiv-has-cardinality-id-number-of-elements-is-finite : + {l : Level} (X : UU l) ( H : is-finite X) (n : ℕ) → + has-cardinality-ℕ n X → Id (number-of-elements-is-finite H) n + map-equiv-has-cardinality-id-number-of-elements-is-finite X H n = + map-equiv (equiv-has-cardinality-id-number-of-elements-is-finite X H n) + + map-inv-equiv-has-cardinality-id-number-of-elements-is-finite : + {l : Level} (X : UU l) ( H : is-finite X) (n : ℕ) → + Id (number-of-elements-is-finite H) n → has-cardinality-ℕ n X + map-inv-equiv-has-cardinality-id-number-of-elements-is-finite X H n = + map-inv-equiv (equiv-has-cardinality-id-number-of-elements-is-finite X H n) ``` ## External links diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index b809050655..2e19215320 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -174,7 +174,7 @@ has-injective-map-is-upper-bound-finite-enumeration X eq f = ( is-injective-Prop (is-set-has-decidable-equality eq))) ( λ g → unit-trunc-Prop ( ( λ x → inclusion-fiber (map-finite-enumeration X f) (g x)) , - ( is-injective-is-section {! !} {! !} {! !}))) + ( {! !}))) ( has-section-has-decidable-equality-finite-enumeration X eq f) is-upper-bound-finite-enumeration : From eac9ee3fd22909642618df495abd9c960abb3c35 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Tue, 2 Sep 2025 15:58:18 -0600 Subject: [PATCH 32/35] makin progress --- .../suspensions-of-propositions.lagda.md | 91 ++++++++++++++++++- .../suspensions-of-types.lagda.md | 8 +- 2 files changed, 91 insertions(+), 8 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md index 9fa972b1f0..1f178d59e2 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md @@ -547,9 +547,29 @@ module _ ＝ z) ( suspension-structure-suspension (type-trunc-Prop X)) pr1 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension = - ap trunc-set-suspension-suspension-trunc-prop {! !} ∙ {! !} + ap + ( trunc-set-suspension-suspension-trunc-prop) + ( compute-north-cogap-suspension + ( suspension-structure-suspension-trunc-prop-trunc-set-suspension)) ∙ + triangle-universal-property-trunc-Set + ( suspension-set-Prop (trunc-Prop X)) + ( cogap-suspension + ( suspension-structure-trunc-set-suspension-suspension-trunc-prop)) + ( north-suspension) ∙ + compute-north-cogap-suspension + ( suspension-structure-trunc-set-suspension-suspension-trunc-prop) pr1 (pr2 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension) = - ap trunc-set-suspension-suspension-trunc-prop {! !} ∙ {! !} + ap + ( trunc-set-suspension-suspension-trunc-prop) + ( compute-south-cogap-suspension + ( suspension-structure-suspension-trunc-prop-trunc-set-suspension)) ∙ + triangle-universal-property-trunc-Set + ( suspension-set-Prop (trunc-Prop X)) + ( cogap-suspension + ( suspension-structure-trunc-set-suspension-suspension-trunc-prop)) + ( south-suspension) ∙ + compute-south-cogap-suspension + ( suspension-structure-trunc-set-suspension-suspension-trunc-prop) pr2 (pr2 dependent-suspension-structure-suspension-trunc-prop-trunc-set-suspension) _ = eq-is-prop ( is-set-suspension-Prop @@ -559,6 +579,67 @@ module _ ( south-suspension)) ( south-suspension)) + dependent-suspension-structure-eq-type-trunc-set-suspension : + dependent-suspension-structure + (λ z → type-Set + (set-Prop + (Id-Prop + (trunc-Set (suspension X)) + ( (suspension-trunc-prop-trunc-set-suspension ∘ + trunc-set-suspension-suspension-trunc-prop) + (unit-trunc-Set z)) + (unit-trunc-Set z)))) + (suspension-structure-suspension X) + pr1 dependent-suspension-structure-eq-type-trunc-set-suspension = + ap + ( suspension-trunc-prop-trunc-set-suspension) + ( {! !}) ∙ + {! !} ∙ + ap + ( unit-trunc-Set) + ( compute-north-cogap-suspension + ( suspension-structure-suspension X)) + pr1 (pr2 dependent-suspension-structure-eq-type-trunc-set-suspension) = + ap + ( suspension-trunc-prop-trunc-set-suspension) + ( {! !}) ∙ + {! !} ∙ + ap + ( unit-trunc-Set) + ( compute-south-cogap-suspension + ( suspension-structure-suspension X)) + pr2 (pr2 dependent-suspension-structure-eq-type-trunc-set-suspension) x = + eq-is-prop + ( is-set-type-trunc-Set + ( ( suspension-trunc-prop-trunc-set-suspension ∘ + trunc-set-suspension-suspension-trunc-prop) + ( unit-trunc-Set + ( south-suspension-structure + ( suspension-structure-suspension X)))) + ( unit-trunc-Set + ( south-suspension-structure + ( suspension-structure-suspension X)))) + + eq-type-trunc-set-suspension : + (x : type-trunc-Set (suspension X)) → + ( suspension-trunc-prop-trunc-set-suspension ∘ + trunc-set-suspension-suspension-trunc-prop) + x ＝ + x + eq-type-trunc-set-suspension x = + function-dependent-universal-property-trunc-Set + ( λ y → + set-Prop + ( Id-Prop + ( trunc-Set (suspension X)) + ( ( suspension-trunc-prop-trunc-set-suspension ∘ + trunc-set-suspension-suspension-trunc-prop) + ( y)) + ( y))) + ( dependent-cogap-suspension _ + ( dependent-suspension-structure-eq-type-trunc-set-suspension)) + ( x) + suspension-structure-eq-trunc-set-suspension : (x : type-trunc-Set (suspension X)) → suspension-structure @@ -567,8 +648,10 @@ module _ trunc-set-suspension-suspension-trunc-prop) x ＝ x) - pr1 (suspension-structure-eq-trunc-set-suspension x) = {! !} - pr1 (pr2 (suspension-structure-eq-trunc-set-suspension x)) = {! !} + pr1 (suspension-structure-eq-trunc-set-suspension x) = + eq-type-trunc-set-suspension x + pr1 (pr2 (suspension-structure-eq-trunc-set-suspension x)) = + eq-type-trunc-set-suspension x pr2 (pr2 (suspension-structure-eq-trunc-set-suspension x)) _ = eq-is-prop ( is-set-type-trunc-Set diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index fa48e8f1ab..0870637b41 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -806,10 +806,10 @@ contractible and hence are `Fin 1`. (<-): Such a cardinality can only be 1 or 2 - suspensions are inhabited, say, by `north`, and the cardinality of a type finitely enumerated by `Fin 2 ＝ bool` -can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` is 0-connected -and hence contractible, well, this is the definition of 0-connectedness of -`Σ X`, and therefore `X` is inhabited. When it's 2, i.e. when there are no -identifications `north ＝ south` in `Σ X`, then `X` better have been empty. ∎ +can be no more than 2. When it's 1, i.e. when `trunc-Set (Σ X)` is contractible, +well, this is the definition of 0-connectedness of `Σ X`, and therefore `X` is +inhabited. When it's 2, i.e. when there are no identifications `north ＝ south` +in `Σ X`, then `X` better have been empty. ∎ ```agda module _ From 7bf58fe816180ffa65abff20283f75646816f58d Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Tue, 2 Sep 2025 15:59:09 -0600 Subject: [PATCH 33/35] lossy unification --- .../suspensions-of-propositions.lagda.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md index 1f178d59e2..77dc80b67f 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md @@ -1,6 +1,8 @@ # Suspensions of propositions ```agda +{-# OPTIONS --lossy-unification #-} + module synthetic-homotopy-theory.suspensions-of-propositions where ``` From e326b9be98892c295afe619791fe6533509c3139 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Tue, 2 Sep 2025 16:23:54 -0600 Subject: [PATCH 34/35] got the prop!! --- .../suspensions-of-propositions.lagda.md | 30 +++++++++++-------- 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md index 77dc80b67f..d97a85203f 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md @@ -595,21 +595,27 @@ module _ pr1 dependent-suspension-structure-eq-type-trunc-set-suspension = ap ( suspension-trunc-prop-trunc-set-suspension) - ( {! !}) ∙ - {! !} ∙ - ap - ( unit-trunc-Set) - ( compute-north-cogap-suspension - ( suspension-structure-suspension X)) + ( triangle-universal-property-trunc-Set + ( suspension-set-Prop (trunc-Prop X)) + ( cogap-suspension + suspension-structure-trunc-set-suspension-suspension-trunc-prop) + ( north-suspension) ∙ + ( compute-north-cogap-suspension + ( suspension-structure-trunc-set-suspension-suspension-trunc-prop))) ∙ + compute-north-cogap-suspension + ( suspension-structure-suspension-trunc-prop-trunc-set-suspension) pr1 (pr2 dependent-suspension-structure-eq-type-trunc-set-suspension) = ap ( suspension-trunc-prop-trunc-set-suspension) - ( {! !}) ∙ - {! !} ∙ - ap - ( unit-trunc-Set) - ( compute-south-cogap-suspension - ( suspension-structure-suspension X)) + ( triangle-universal-property-trunc-Set + ( suspension-set-Prop (trunc-Prop X)) + ( cogap-suspension + suspension-structure-trunc-set-suspension-suspension-trunc-prop) + ( south-suspension) ∙ + ( compute-south-cogap-suspension + ( suspension-structure-trunc-set-suspension-suspension-trunc-prop))) ∙ + compute-south-cogap-suspension + ( suspension-structure-suspension-trunc-prop-trunc-set-suspension) pr2 (pr2 dependent-suspension-structure-eq-type-trunc-set-suspension) x = eq-is-prop ( is-set-type-trunc-Set From 5d8e28d482c82d5513c1a7b20ef36a2d3a55adea Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Wed, 3 Sep 2025 10:15:39 -0600 Subject: [PATCH 35/35] a couple of the edits worked in; will get the rest later --- .../suspensions-of-propositions.lagda.md | 6 +----- .../suspensions-of-types.lagda.md | 12 ++++++------ 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md index d97a85203f..4f5ffd36ae 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-propositions.lagda.md @@ -492,11 +492,7 @@ module _ ( surjection-equiv equiv-bool-Fin-2)) ``` -### Suspensions _almost_ commute with propositional truncations - -The problem is that empty types suspend to a two-element set. This is easily -fixed by adjusting the truncation level, and we do have that -`Σ (trunc-Prop X) = trunc-Set (Σ X)`. +### The suspension of the propositional truncation is the set-truncation of the suspension ```agda module _ diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 0870637b41..f59962a476 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -775,15 +775,15 @@ particular we [merely](foundation.mere-equality.md) have `p ∈ north ＝ south` such identifications are inductively generated by `X`. ```agda -suspension-is-0-connected-is-inhabited : +is-0-connected-suspension-is-inhabited : {l : Level} (X : UU l) → is-inhabited X → is-0-connected (suspension X) -suspension-is-0-connected-is-inhabited X x = +is-0-connected-suspension-is-inhabited X x = is-connected-succ-suspension-is-connected ( is-neg-one-connected-is-inhabited X x) -is-inhabited-suspension-is-0-connected : +is-inhabited-is-0-connected-suspension : {l : Level} (X : UU l) → is-0-connected (suspension X) → is-inhabited X -is-inhabited-suspension-is-0-connected X ΣX-conn = +is-inhabited-is-0-connected-suspension X ΣX-conn = rec-trunc-Prop (is-inhabited-Prop X) (λ h → {! !}) p where p : mere-eq (north-suspension {X = X}) (south-suspension {X = X}) @@ -819,7 +819,7 @@ module _ trunc-suspension-is-contractible-is-pointed : X → is-contr (type-trunc-Set (suspension X)) trunc-suspension-is-contractible-is-pointed x = - suspension-is-0-connected-is-inhabited X (unit-trunc-Prop x) + is-0-connected-suspension-is-inhabited X (unit-trunc-Prop x) trunc-suspension-is-contractible-is-inhabited : is-inhabited X → is-contr (type-trunc-Set (suspension X)) @@ -871,7 +871,7 @@ module _ ( is-empty-is-zero-number-of-elements-is-finite p eq))) ... | 1 = inl - ( is-inhabited-suspension-is-0-connected + ( is-inhabited-is-0-connected-suspension ( X) ( is-contr-is-one-number-of-elements-is-finite p eq)) ... | 2 =