-
Notifications
You must be signed in to change notification settings - Fork 67
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
A (mere) `k`-path-cosplit map is defined inductively - A (mere) `-2`-path-cosplit map is a map that is (merely) a retract - A (mere) `k+1`-path-cosplit map is a map whose action on identifications is (merely) `k`-path-cosplit. We show - Mere `k`-path-cosplitting is a property - `k`-truncated maps are `k`-path-cosplit - (merely) `k`-path-cosplit maps are (merely) `k+1`-path-cosplit - types that map into `k`-truncated types via (mere) `k`-path-cosplit maps are `k`-truncated - (mere) `k`-path-cosplit maps into `k`-truncated types are `k`-truncated.
- Loading branch information
1 parent
dafc57a
commit 270c39f
Showing
8 changed files
with
370 additions
and
17 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,171 @@ | ||
| # Mere path-cosplit maps | ||
|
|
||
| ```agda | ||
| module foundation.mere-path-cosplit-maps where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.action-on-identifications-functions | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.inhabited-types | ||
| open import foundation.iterated-dependent-product-types | ||
| open import foundation.logical-equivalences | ||
| open import foundation.propositional-truncations | ||
| open import foundation.truncated-maps | ||
| open import foundation.truncation-levels | ||
| open import foundation.universe-levels | ||
|
|
||
| open import foundation-core.contractible-maps | ||
| open import foundation-core.contractible-types | ||
| open import foundation-core.equivalences | ||
| open import foundation-core.propositions | ||
| open import foundation-core.retractions | ||
| open import foundation-core.truncated-types | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| In Homotopy Type Theory, there are multiple nonequivalent ways to state that a | ||
| map is "injective" that are more or less informed by the homotopy structures of | ||
| its domain and codomain. A | ||
| {{#concept "mere path-cosplit map" Disambiguation="between types" Agda=is-mere-path-cosplit}} | ||
| is one such notion, lying somewhere between | ||
| [embeddings](foundation-core.embeddings.md) and | ||
| [injective maps](foundation-core.injective-maps.md). In fact, given an integer | ||
| `k β₯ -2`, if we understand `k`-injective map to mean the `k+2`-dimensional | ||
| [action on identifications](foundation.action-on-higher-identifications-functions.md) | ||
| has a converse map, then we have proper inclusions | ||
|
|
||
| ```text | ||
| k-injective maps β k-path-cosplit maps β k-truncated maps. | ||
| ``` | ||
|
|
||
| While `k`-truncatedness answers the question: | ||
|
|
||
| > At which dimension is the action on higher identifications of a function | ||
| > always an [equivalence](foundation-core.equivalences.md)? | ||
|
|
||
| Mere `k`-path-cosplitting instead answers the question: | ||
|
|
||
| > At which dimension is the action merely a | ||
| > [retract](foundation-core.retracts-of-types.md)? | ||
|
|
||
| Thus a _merely `-2`-path-cosplit map_ is a map that merely is a retract. A | ||
| _merely `k+1`-path-cosplit map_ is a map whose | ||
| [action on identifications](foundation.action-on-identifications-functions.md) | ||
| is merely `k`-path-cosplit. | ||
|
|
||
| We show that mere `k`-path-cosplittness coincides with `k`-truncatedness when | ||
| the codomain is `k`-truncated, but more generally mere `k`-path-cosplitting may | ||
| only induce mere retracts on higher homotopy groups. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ```agda | ||
| is-mere-path-cosplit : | ||
| {l1 l2 : Level} (k : π) {A : UU l1} {B : UU l2} β (A β B) β UU (l1 β l2) | ||
| is-mere-path-cosplit neg-two-π f = is-inhabited (retraction f) | ||
| is-mere-path-cosplit (succ-π k) {A} f = | ||
| (x y : A) β is-mere-path-cosplit k (ap f {x} {y}) | ||
| ``` | ||
|
|
||
| ## Properties | ||
|
|
||
| ### Being merely path-cosplit is a property | ||
|
|
||
| ```agda | ||
| is-prop-is-mere-path-cosplit : | ||
| {l1 l2 : Level} (k : π) {A : UU l1} {B : UU l2} (f : A β B) β | ||
| is-prop (is-mere-path-cosplit k f) | ||
| is-prop-is-mere-path-cosplit neg-two-π f = | ||
| is-property-is-inhabited (retraction f) | ||
| is-prop-is-mere-path-cosplit (succ-π k) f = | ||
| is-prop-Ξ (Ξ» x β is-prop-Ξ Ξ» y β is-prop-is-mere-path-cosplit k (ap f)) | ||
|
|
||
| is-mere-path-cosplit-Prop : | ||
| {l1 l2 : Level} (k : π) {A : UU l1} {B : UU l2} β (A β B) β Prop (l1 β l2) | ||
| is-mere-path-cosplit-Prop k f = | ||
| (is-mere-path-cosplit k f , is-prop-is-mere-path-cosplit k f) | ||
| ``` | ||
|
|
||
| ### If a map is `k`-truncated then it is merely `k`-path-cosplit | ||
|
|
||
| ```agda | ||
| is-mere-path-cosplit-is-trunc : | ||
| {l1 l2 : Level} (k : π) {A : UU l1} {B : UU l2} {f : A β B} β | ||
| is-trunc-map k f β is-mere-path-cosplit k f | ||
| is-mere-path-cosplit-is-trunc neg-two-π is-trunc-f = | ||
| unit-trunc-Prop (retraction-is-contr-map is-trunc-f) | ||
| is-mere-path-cosplit-is-trunc (succ-π k) {f = f} is-trunc-f x y = | ||
| is-mere-path-cosplit-is-trunc k | ||
| ( is-trunc-map-ap-is-trunc-map k f is-trunc-f x y) | ||
| ``` | ||
|
|
||
| ### If a map is `k`-path-cosplit then it is merely `k+1`-path-cosplit | ||
|
|
||
| ```agda | ||
| is-mere-path-cosplit-succ-is-mere-path-cosplit : | ||
| {l1 l2 : Level} (k : π) {A : UU l1} {B : UU l2} {f : A β B} β | ||
| is-mere-path-cosplit k f β is-mere-path-cosplit (succ-π k) f | ||
| is-mere-path-cosplit-succ-is-mere-path-cosplit | ||
| neg-two-π {f = f} is-cosplit-f x y = | ||
| rec-trunc-Prop | ||
| ( is-mere-path-cosplit-Prop neg-two-π (ap f)) | ||
| ( Ξ» r β unit-trunc-Prop (retraction-ap f r)) | ||
| ( is-cosplit-f) | ||
| is-mere-path-cosplit-succ-is-mere-path-cosplit (succ-π k) is-cosplit-f x y = | ||
| is-mere-path-cosplit-succ-is-mere-path-cosplit k (is-cosplit-f x y) | ||
| ``` | ||
|
|
||
| ### If a type maps into a `k`-truncted type via a merely `k`-path-cosplit map then it is `k`-truncated | ||
|
|
||
| ```agda | ||
| is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain : | ||
| {l1 l2 : Level} (k : π) {A : UU l1} {B : UU l2} {f : A β B} β | ||
| is-trunc k B β is-mere-path-cosplit k f β is-trunc k A | ||
| is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain neg-two-π | ||
| {A} {B} {f} is-trunc-B = | ||
| rec-trunc-Prop | ||
| ( is-trunc-Prop neg-two-π A) | ||
| ( Ξ» r β is-trunc-retract-of (f , r) is-trunc-B) | ||
| is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain | ||
| (succ-π k) {A} {B} {f} is-trunc-B is-cosplit-f x y = | ||
| is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain k | ||
| ( is-trunc-B (f x) (f y)) | ||
| ( is-cosplit-f x y) | ||
| ``` | ||
|
|
||
| This result generalizes the following statements: | ||
|
|
||
| - A type that injects into a set is a set. | ||
|
|
||
| - A type that embeds into a `k+1`-truncated type is `k+1`-truncated. | ||
|
|
||
| - A type that maps into a `k`-truncated type via a `k`-truncated map is | ||
| `k`-truncated. | ||
|
|
||
| ### If the codomain of a mere `k`-path-cosplit map is `k`-truncated then the map is `k`-truncated | ||
|
|
||
| ```agda | ||
| is-trunc-map-is-mere-path-cosplit-is-trunc-codomain : | ||
| {l1 l2 : Level} (k : π) {A : UU l1} {B : UU l2} {f : A β B} β | ||
| is-trunc k B β is-mere-path-cosplit k f β is-trunc-map k f | ||
| is-trunc-map-is-mere-path-cosplit-is-trunc-codomain k is-trunc-B is-cosplit-f = | ||
| is-trunc-map-is-trunc-domain-codomain k | ||
| ( is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain k | ||
| ( is-trunc-B) | ||
| ( is-cosplit-f)) | ||
| ( is-trunc-B) | ||
| ``` | ||
|
|
||
| ## See also | ||
|
|
||
| - [Path-cosplit maps](foundation.path-cosplit-maps.md) | ||
| - [Path-split maps](foundation.path-cosplit-maps.md) | ||
| - [Injective maps](foundation-core.injective-maps.md) | ||
| - [Truncated maps](foundation-core.truncated-maps.md) | ||
| - [Embeddings](foundation-core.embeddings.md) |
Oops, something went wrong.