-
Notifications
You must be signed in to change notification settings - Fork 73
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Define left half-smash products (#1320)
- Loading branch information
1 parent
46bee5c
commit 74d97dd
Showing
11 changed files
with
566 additions
and
265 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
134 changes: 134 additions & 0 deletions
134
src/synthetic-homotopy-theory/cofibers-of-maps.lagda.md
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,134 @@ | ||
| # Cofibers of maps | ||
|
|
||
| ```agda | ||
| module synthetic-homotopy-theory.cofibers-of-maps where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.constant-maps | ||
| open import foundation.contractible-types | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.equivalences | ||
| open import foundation.unit-type | ||
| open import foundation.universe-levels | ||
|
|
||
| open import structured-types.pointed-maps | ||
| open import structured-types.pointed-types | ||
| open import structured-types.pointed-unit-type | ||
|
|
||
| open import synthetic-homotopy-theory.cocones-under-spans | ||
| open import synthetic-homotopy-theory.dependent-cocones-under-spans | ||
| open import synthetic-homotopy-theory.dependent-universal-property-pushouts | ||
| open import synthetic-homotopy-theory.pushouts | ||
| open import synthetic-homotopy-theory.universal-property-pushouts | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| The | ||
| {{#concept "cofiber" Disambiguation="of a map of types" WD="mapping cone" WDID=Q306560 Agda=cofiber}} | ||
| of a map `f : A → B` is the [pushout](synthetic-homotopy-theory.pushouts.md) of | ||
| the span `B ← A → *`. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### The cofiber of a map | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) | ||
| where | ||
|
|
||
| cofiber : UU (l1 ⊔ l2) | ||
| cofiber = pushout f (terminal-map A) | ||
|
|
||
| cocone-cofiber : cocone f (terminal-map A) cofiber | ||
| cocone-cofiber = cocone-pushout f (terminal-map A) | ||
|
|
||
| inl-cofiber : B → cofiber | ||
| inl-cofiber = pr1 cocone-cofiber | ||
|
|
||
| inr-cofiber : unit → cofiber | ||
| inr-cofiber = pr1 (pr2 cocone-cofiber) | ||
|
|
||
| point-cofiber : cofiber | ||
| point-cofiber = inr-cofiber star | ||
|
|
||
| pointed-type-cofiber : Pointed-Type (l1 ⊔ l2) | ||
| pointed-type-cofiber = (cofiber , point-cofiber) | ||
|
|
||
| inr-pointed-map-cofiber : unit-Pointed-Type →∗ pointed-type-cofiber | ||
| inr-pointed-map-cofiber = inclusion-point-Pointed-Type (pointed-type-cofiber) | ||
|
|
||
| universal-property-cofiber : | ||
| universal-property-pushout f (terminal-map A) cocone-cofiber | ||
| universal-property-cofiber = up-pushout f (terminal-map A) | ||
|
|
||
| dependent-universal-property-cofiber : | ||
| dependent-universal-property-pushout f (terminal-map A) cocone-cofiber | ||
| dependent-universal-property-cofiber = dup-pushout f (terminal-map A) | ||
|
|
||
| cogap-cofiber : | ||
| {l : Level} {X : UU l} → cocone f (terminal-map A) X → cofiber → X | ||
| cogap-cofiber = cogap f (terminal-map A) | ||
|
|
||
| dependent-cogap-cofiber : | ||
| {l : Level} {P : cofiber → UU l} | ||
| (c : dependent-cocone f (terminal-map A) (cocone-cofiber) P) | ||
| (x : cofiber) → P x | ||
| dependent-cogap-cofiber = dependent-cogap f (terminal-map A) | ||
| ``` | ||
|
|
||
| ## Properties | ||
|
|
||
| ### The cofiber of an equivalence is contractible | ||
|
|
||
| Note that this is not a logical equivalence. Not every map whose cofibers are | ||
| all contractible is an equivalence. For instance, the cofiber of `X → 1` where | ||
| `X` is an [acyclic type](synthetic-homotopy-theory.acyclic-types.md) is by | ||
| definition contractible. Examples of noncontractible acyclic types include | ||
| [Hatcher's acyclic type](synthetic-homotopy-theory.hatchers-acyclic-type.md). | ||
|
|
||
| ```agda | ||
| is-contr-cofiber-is-equiv : | ||
| {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → | ||
| is-equiv f → is-contr (cofiber f) | ||
| is-contr-cofiber-is-equiv {A = A} f is-equiv-f = | ||
| is-contr-equiv-unit' | ||
| ( inr-cofiber f , | ||
| is-equiv-universal-property-pushout | ||
| ( f) | ||
| ( terminal-map A) | ||
| ( cocone-cofiber f) | ||
| ( is-equiv-f) | ||
| ( universal-property-cofiber f)) | ||
| ``` | ||
|
|
||
| ### The cofibers of the point inclusions in `B` are equivalent to `B` | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l : Level} {B : UU l} (b : B) | ||
| where | ||
|
|
||
| is-equiv-inl-cofiber-point : is-equiv (inl-cofiber (point b)) | ||
| is-equiv-inl-cofiber-point = | ||
| is-equiv-universal-property-pushout' | ||
| ( point b) | ||
| ( terminal-map unit) | ||
| ( cocone-pushout (point b) (terminal-map unit)) | ||
| ( is-equiv-is-contr (terminal-map unit) is-contr-unit is-contr-unit) | ||
| ( up-pushout (point b) (terminal-map unit)) | ||
|
|
||
| compute-cofiber-point : B ≃ cofiber (point b) | ||
| compute-cofiber-point = (inl-cofiber (point b) , is-equiv-inl-cofiber-point) | ||
| ``` | ||
|
|
||
| ## See also | ||
|
|
||
| - Cofibers of maps are formally dual to | ||
| [fibers of maps](foundation-core.fibers-of-maps.md) |
78 changes: 78 additions & 0 deletions
78
src/synthetic-homotopy-theory/cofibers-of-pointed-maps.lagda.md
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,78 @@ | ||
| # Cofibers of pointed maps | ||
|
|
||
| ```agda | ||
| module synthetic-homotopy-theory.cofibers-of-pointed-maps where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.constant-maps | ||
| open import foundation.contractible-types | ||
| open import foundation.dependent-pair-types | ||
| open import foundation.equivalences | ||
| open import foundation.unit-type | ||
| open import foundation.universe-levels | ||
|
|
||
| open import structured-types.pointed-maps | ||
| open import structured-types.pointed-types | ||
| open import structured-types.pointed-unit-type | ||
|
|
||
| open import synthetic-homotopy-theory.cocones-under-pointed-span-diagrams | ||
| open import synthetic-homotopy-theory.cocones-under-spans | ||
| open import synthetic-homotopy-theory.cofibers-of-maps | ||
| open import synthetic-homotopy-theory.dependent-cocones-under-spans | ||
| open import synthetic-homotopy-theory.dependent-universal-property-pushouts | ||
| open import synthetic-homotopy-theory.pushouts | ||
| open import synthetic-homotopy-theory.pushouts-of-pointed-types | ||
| open import synthetic-homotopy-theory.universal-property-pushouts | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| The | ||
| {{#concept "cofiber" Disambiguation="of a pointed map of pointed types" WD="mapping cone" WDID=Q306560 Agda=cofiber-Pointed-Type}} | ||
| of a [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` is the | ||
| [pushout](synthetic-homotopy-theory.pushouts-of-pointed-types.md) of the span of | ||
| pointed maps `B ← A → *`. | ||
|
|
||
| ## Definitions | ||
|
|
||
| ### The cofiber of a pointed map | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) | ||
| where | ||
|
|
||
| type-cofiber-Pointed-Type : UU (l1 ⊔ l2) | ||
| type-cofiber-Pointed-Type = | ||
| type-pushout-Pointed-Type f (terminal-pointed-map A) | ||
|
|
||
| point-cofiber-Pointed-Type : Pointed-Type (l1 ⊔ l2) | ||
| point-cofiber-Pointed-Type = pushout-Pointed-Type f (terminal-pointed-map A) | ||
|
|
||
| cofiber-Pointed-Type : Pointed-Type (l1 ⊔ l2) | ||
| cofiber-Pointed-Type = pushout-Pointed-Type f (terminal-pointed-map A) | ||
|
|
||
| inl-cofiber-Pointed-Type : B →∗ cofiber-Pointed-Type | ||
| inl-cofiber-Pointed-Type = inl-pushout-Pointed-Type f (terminal-pointed-map A) | ||
|
|
||
| inr-cofiber-Pointed-Type : unit-Pointed-Type →∗ cofiber-Pointed-Type | ||
| inr-cofiber-Pointed-Type = inr-pushout-Pointed-Type f (terminal-pointed-map A) | ||
|
|
||
| map-cogap-cofiber-Pointed-Type : | ||
| {l : Level} {X : Pointed-Type l} → | ||
| cocone-Pointed-Type f (terminal-pointed-map A) X → | ||
| type-cofiber-Pointed-Type → type-Pointed-Type X | ||
| map-cogap-cofiber-Pointed-Type = | ||
| map-cogap-Pointed-Type f (terminal-pointed-map A) | ||
|
|
||
| cogap-cofiber-Pointed-Type : | ||
| {l : Level} {X : Pointed-Type l} → | ||
| cocone-Pointed-Type f (terminal-pointed-map A) X → | ||
| cofiber-Pointed-Type →∗ X | ||
| cogap-cofiber-Pointed-Type = cogap-Pointed-Type f (terminal-pointed-map A) | ||
| ``` |
Oops, something went wrong.