diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index 4ac03848a2..d2a86967a1 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -25,7 +25,6 @@ open import foundation-core.equality-dependent-pair-types public open import foundation-core.equivalence-relations public open import foundation-core.equivalences public open import foundation-core.fibers-of-maps public -open import foundation-core.function-extensionality public open import foundation-core.function-types public open import foundation-core.functoriality-dependent-function-types public open import foundation-core.functoriality-dependent-pair-types public diff --git a/src/foundation-core/function-extensionality.lagda.md b/src/foundation-core/function-extensionality.lagda.md deleted file mode 100644 index a1dba7e527..0000000000 --- a/src/foundation-core/function-extensionality.lagda.md +++ /dev/null @@ -1,86 +0,0 @@ -# Function extensionality - -```agda -module foundation-core.function-extensionality where -``` - -
Imports - -```agda -open import foundation.action-on-identifications-functions -open import foundation.universe-levels - -open import foundation-core.equivalences -open import foundation-core.function-types -open import foundation-core.homotopies -open import foundation-core.identity-types -``` - -
- -## Idea - -The function extensionality axiom asserts that identifications of (dependent) -functions are equivalently described as pointwise equalities between them. In -other words, a function is completely determined by its values. - -In this file, we define the statement of the axiom. The axiom itself is -postulated in -[`foundation.function-extensionality`](foundation.function-extensionality.md) as -`funext`. - -## Statement - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : A → UU l2} - where - - htpy-eq : {f g : (x : A) → B x} → f ＝ g → f ~ g - htpy-eq refl = refl-htpy - - instance-function-extensionality : (f g : (x : A) → B x) → UU (l1 ⊔ l2) - instance-function-extensionality f g = is-equiv (htpy-eq {f} {g}) - - based-function-extensionality : (f : (x : A) → B x) → UU (l1 ⊔ l2) - based-function-extensionality f = - (g : (x : A) → B x) → is-equiv (htpy-eq {f} {g}) - -function-extensionality-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) -function-extensionality-Level l1 l2 = - {A : UU l1} {B : A → UU l2} - (f g : (x : A) → B x) → - instance-function-extensionality f g - -function-extensionality : UUω -function-extensionality = {l1 l2 : Level} → function-extensionality-Level l1 l2 -``` - -## Properties - -### Naturality of `htpy-eq` - -```agda -square-htpy-eq : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B) → - ( g h : B → C) → - ( (λ (p : (y : B) → g y ＝ h y) (x : A) → p (f x)) ∘ htpy-eq) ~ - ( htpy-eq ∘ (ap (precomp f C))) -square-htpy-eq f g .g refl = refl -``` - -### The action on paths of an evaluation map - -```agda -ap-ev : - {l1 l2 : Level} {A : UU l1} {B : UU l2} (a : A) → {f g : A → B} → - (p : f ＝ g) → (ap (λ h → h a) p) ＝ htpy-eq p a -ap-ev a refl = refl -``` - -## See also - -- That the univalence axiom implies function extensionality is proven in - [`foundation.univalence-implies-function-extensionality`](foundation.univalence-implies-function-extensionality.md). -- Weak function extensionality is defined in - [`foundation.weak-function-extensionality`](foundation.weak-function-extensionality.md). diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md index de3ee5e483..42205ec1a9 100644 --- a/src/foundation-core/homotopies.lagda.md +++ b/src/foundation-core/homotopies.lagda.md @@ -41,7 +41,7 @@ module _ map-compute-dependent-identification-eq-value : {x y : X} (p : x ＝ y) (q : eq-value x) (r : eq-value y) → - coherence-square-identifications (apd f p) r (ap (tr P p) q) (apd g p) → + coherence-square-identifications (ap (tr P p) q) (apd f p) (apd g p) r → dependent-identification eq-value p q r map-compute-dependent-identification-eq-value refl q r = inv ∘ (concat' r (right-unit ∙ ap-id q)) @@ -61,14 +61,14 @@ module _ map-compute-dependent-identification-eq-value-function : {x y : X} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) → - coherence-square-identifications (ap f p) r q (ap g p) → + coherence-square-identifications q (ap f p) (ap g p) r → dependent-identification eq-value-function p q r map-compute-dependent-identification-eq-value-function refl q r = inv ∘ concat' r right-unit map-compute-dependent-identification-eq-value-id-id : {l1 : Level} {A : UU l1} {a b : A} (p : a ＝ b) (q : a ＝ a) (r : b ＝ b) → - coherence-square-identifications p r q p → + coherence-square-identifications q p p r → dependent-identification (eq-value id id) p q r map-compute-dependent-identification-eq-value-id-id refl q r s = inv (s ∙ right-unit) @@ -76,7 +76,7 @@ map-compute-dependent-identification-eq-value-id-id refl q r s = map-compute-dependent-identification-eq-value-comp-id : {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : B → A) (f : A → B) {a b : A} (p : a ＝ b) (q : eq-value (g ∘ f) id a) (r : eq-value (g ∘ f) id b) → - coherence-square-identifications (ap g (ap f p)) r q p → + coherence-square-identifications q (ap g (ap f p)) p r → dependent-identification (eq-value (g ∘ f) id) p q r map-compute-dependent-identification-eq-value-comp-id g f refl q r s = inv (s ∙ right-unit) @@ -335,7 +335,7 @@ syntax step-homotopy-reasoning p h q = p ~ h by q - We postulate that homotopies characterize identifications of (dependent) functions in the file - [`foundation-core.function-extensionality`](foundation-core.function-extensionality.md). + [`foundation.function-extensionality`](foundation.function-extensionality.md). - [Multivariable homotopies](foundation.multivariable-homotopies.md). - The [whiskering operations](foundation.whiskering-homotopies.md) on homotopies. diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md index f55b64f2b5..1b394e0c5a 100644 --- a/src/foundation-core/propositions.lagda.md +++ b/src/foundation-core/propositions.lagda.md @@ -8,13 +8,13 @@ module foundation-core.propositions where ```agda open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.contractible-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types diff --git a/src/foundation-core/transport-along-identifications.lagda.md b/src/foundation-core/transport-along-identifications.lagda.md index b3bccb86b3..c255397028 100644 --- a/src/foundation-core/transport-along-identifications.lagda.md +++ b/src/foundation-core/transport-along-identifications.lagda.md @@ -7,6 +7,7 @@ module foundation-core.transport-along-identifications where
Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.universe-levels open import foundation-core.identity-types @@ -25,7 +26,7 @@ The fact that `tr B p` is an [equivalence](foundation-core.equivalences.md) is recorded in [`foundation.transport-along-identifications`](foundation.transport-along-identifications.md). -## Definition +## Definitions ### Transport @@ -79,6 +80,17 @@ preserves-tr : preserves-tr f refl x = refl ``` +### Transporting along the action on identifications of a function + +```agda +tr-ap : + {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} {D : C → UU l4} + (f : A → C) (g : (x : A) → B x → D (f x)) + {x y : A} (p : x ＝ y) (z : B x) → + tr D (ap f p) (g x z) ＝ g y (tr B p z) +tr-ap f g refl z = refl +``` + ### Computing maps out of identity types as transports ```agda @@ -91,3 +103,21 @@ module _ (x : A) (p : a ＝ x) → f x p ＝ tr B p (f a refl) compute-map-out-of-identity-type x refl = refl ``` + +### Computing transport in the type family of identifications with a fixed target + +```agda +tr-Id-left : + {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : b ＝ a) → + tr (_＝ a) q p ＝ ((inv q) ∙ p) +tr-Id-left refl p = refl +``` + +### Computing transport in the type family of identifications with a fixed source + +```agda +tr-Id-right : + {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : a ＝ b) → + tr (a ＝_) q p ＝ (p ∙ q) +tr-Id-right refl refl = refl +``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 98b8aa8bd7..1d473c3b33 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -83,6 +83,7 @@ open import foundation.decidable-types public open import foundation.dependent-binary-homotopies public open import foundation.dependent-binomial-theorem public open import foundation.dependent-epimorphisms public +open import foundation.dependent-homotopies public open import foundation.dependent-identifications public open import foundation.dependent-pair-types public open import foundation.dependent-sequences public @@ -290,6 +291,7 @@ open import foundation.towers public open import foundation.transfinite-cocomposition-of-maps public open import foundation.transport-along-equivalences public open import foundation.transport-along-higher-identifications public +open import foundation.transport-along-homotopies public open import foundation.transport-along-identifications public open import foundation.trivial-relaxed-sigma-decompositions public open import foundation.trivial-sigma-decompositions public diff --git a/src/foundation/action-on-identifications-functions.lagda.md b/src/foundation/action-on-identifications-functions.lagda.md index 4fd28c92ed..d8627e45ac 100644 --- a/src/foundation/action-on-identifications-functions.lagda.md +++ b/src/foundation/action-on-identifications-functions.lagda.md @@ -12,7 +12,6 @@ open import foundation.universe-levels open import foundation-core.constant-maps open import foundation-core.function-types open import foundation-core.identity-types -open import foundation-core.transport-along-identifications ```
@@ -97,17 +96,6 @@ ap-const : ap-const b refl = refl ``` -### Transporting along the action on identifications of a function - -```agda -tr-ap : - {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} {D : C → UU l4} - (f : A → C) (g : (x : A) → B x → D (f x)) - {x y : A} (p : x ＝ y) (z : B x) → - tr D (ap f p) (g x z) ＝ g y (tr B p z) -tr-ap f g refl z = refl -``` - ### The action on identifications of concatenating by `refl` on the right Note that `_∙ refl` is only homotopic to the identity function. Therefore we diff --git a/src/foundation/cantors-diagonal-argument.lagda.md b/src/foundation/cantors-diagonal-argument.lagda.md index fba7fc9574..203101f83f 100644 --- a/src/foundation/cantors-diagonal-argument.lagda.md +++ b/src/foundation/cantors-diagonal-argument.lagda.md @@ -8,6 +8,7 @@ module foundation.cantors-diagonal-argument where ```agda open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations @@ -16,7 +17,6 @@ open import foundation.universe-levels open import foundation-core.empty-types open import foundation-core.fibers-of-maps -open import foundation-core.function-extensionality open import foundation-core.propositions ``` diff --git a/src/foundation/commuting-squares-of-identifications.lagda.md b/src/foundation/commuting-squares-of-identifications.lagda.md index e84892d6ba..179914ea0d 100644 --- a/src/foundation/commuting-squares-of-identifications.lagda.md +++ b/src/foundation/commuting-squares-of-identifications.lagda.md @@ -42,9 +42,8 @@ module _ where coherence-square-identifications : - (left : x ＝ z) (bottom : z ＝ w) - (top : x ＝ y) (right : y ＝ w) → UU l - coherence-square-identifications left bottom top right = + (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) → UU l + coherence-square-identifications top left right bottom = (left ∙ bottom) ＝ (top ∙ right) ``` @@ -65,10 +64,10 @@ module _ where coherence-square-identifications-comp-horizontal : - coherence-square-identifications p-left p-bottom p-top middle → - coherence-square-identifications middle q-bottom q-top q-right → + coherence-square-identifications p-top p-left middle p-bottom → + coherence-square-identifications q-top middle q-right q-bottom → coherence-square-identifications - p-left (p-bottom ∙ q-bottom) (p-top ∙ q-top) q-right + (p-top ∙ q-top) p-left q-right (p-bottom ∙ q-bottom) coherence-square-identifications-comp-horizontal p q = ( ( ( inv (assoc p-left p-bottom q-bottom) ∙ ap-binary (_∙_) p (refl {x = q-bottom})) ∙ @@ -85,10 +84,10 @@ module _ where coherence-square-identifications-comp-vertical : - coherence-square-identifications p-left middle p-top p-right → - coherence-square-identifications q-left q-bottom middle q-right → + coherence-square-identifications p-top p-left p-right middle → + coherence-square-identifications middle q-left q-right q-bottom → coherence-square-identifications - (p-left ∙ q-left) q-bottom p-top (p-right ∙ q-right) + p-top (p-left ∙ q-left) (p-right ∙ q-right) q-bottom coherence-square-identifications-comp-vertical p q = ( assoc p-left q-left q-bottom ∙ ( ( ap-binary (_∙_) (refl {x = p-left}) q ∙ @@ -111,26 +110,26 @@ module _ coherence-square-identifications-left-paste : {left' : x ＝ z} (s : left ＝ left') → - coherence-square-identifications left bottom top right → - coherence-square-identifications left' bottom top right + coherence-square-identifications top left right bottom → + coherence-square-identifications top left' right bottom coherence-square-identifications-left-paste refl sq = sq coherence-square-identifications-bottom-paste : {bottom' : z ＝ w} (s : bottom ＝ bottom') → - coherence-square-identifications left bottom top right → - coherence-square-identifications left bottom' top right + coherence-square-identifications top left right bottom → + coherence-square-identifications top left right bottom' coherence-square-identifications-bottom-paste refl sq = sq coherence-square-identifications-top-paste : {top' : x ＝ y} (s : top ＝ top') → - coherence-square-identifications left bottom top right → - coherence-square-identifications left bottom top' right + coherence-square-identifications top left right bottom → + coherence-square-identifications top' left right bottom coherence-square-identifications-top-paste refl sq = sq coherence-square-identifications-right-paste : {right' : y ＝ w} (s : right ＝ right') → - coherence-square-identifications left bottom top right → - coherence-square-identifications left bottom top right' + coherence-square-identifications top left right bottom → + coherence-square-identifications top left right' bottom coherence-square-identifications-right-paste refl sq = sq ``` @@ -147,36 +146,36 @@ module _ coherence-square-identifications-top-left-whisk' : {x' : A} (p : x' ＝ x) → - coherence-square-identifications left bottom top right → - coherence-square-identifications (p ∙ left) bottom (p ∙ top) right + coherence-square-identifications top left right bottom → + coherence-square-identifications (p ∙ top) (p ∙ left) right bottom coherence-square-identifications-top-left-whisk' refl sq = sq coherence-square-identifications-top-left-whisk : {x' : A} (p : x ＝ x') → - coherence-square-identifications left bottom top right → - coherence-square-identifications (inv p ∙ left) bottom (inv p ∙ top) right + coherence-square-identifications top left right bottom → + coherence-square-identifications (inv p ∙ top) (inv p ∙ left) right bottom coherence-square-identifications-top-left-whisk refl sq = sq coherence-square-identifications-top-right-whisk : {y' : A} (p : y ＝ y') → - coherence-square-identifications left bottom top right → - coherence-square-identifications left bottom (top ∙ p) (inv p ∙ right) + coherence-square-identifications top left right bottom → + coherence-square-identifications (top ∙ p) left (inv p ∙ right) bottom coherence-square-identifications-top-right-whisk refl = coherence-square-identifications-top-paste left bottom top right (inv right-unit) coherence-square-identifications-bottom-left-whisk : {z' : A} (p : z ＝ z') → - coherence-square-identifications left bottom top right → - coherence-square-identifications (left ∙ p) (inv p ∙ bottom) top right + coherence-square-identifications top left right bottom → + coherence-square-identifications top (left ∙ p) right (inv p ∙ bottom) coherence-square-identifications-bottom-left-whisk refl = coherence-square-identifications-left-paste left bottom top right (inv right-unit) coherence-square-identifications-bottom-right-whisk : {w' : A} (p : w ＝ w') → - coherence-square-identifications left bottom top right → - coherence-square-identifications left (bottom ∙ p) top (right ∙ p) + coherence-square-identifications top left right bottom → + coherence-square-identifications top left (right ∙ p) (bottom ∙ p) coherence-square-identifications-bottom-right-whisk refl = ( coherence-square-identifications-bottom-paste left bottom top (right ∙ refl) (inv right-unit)) ∘ diff --git a/src/foundation/constant-maps.lagda.md b/src/foundation/constant-maps.lagda.md index 50da27c564..69dd9619d5 100644 --- a/src/foundation/constant-maps.lagda.md +++ b/src/foundation/constant-maps.lagda.md @@ -12,6 +12,7 @@ open import foundation-core.constant-maps public open import foundation.0-maps open import foundation.dependent-pair-types open import foundation.faithful-maps +open import foundation.function-extensionality open import foundation.type-arithmetic-unit-type open import foundation.unit-type open import foundation.universe-levels @@ -21,7 +22,6 @@ open import foundation-core.contractible-maps open import foundation-core.embeddings open import foundation-core.equivalences open import foundation-core.fibers-of-maps -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.injective-maps diff --git a/src/foundation/dependent-homotopies.lagda.md b/src/foundation/dependent-homotopies.lagda.md new file mode 100644 index 0000000000..27e973f0e3 --- /dev/null +++ b/src/foundation/dependent-homotopies.lagda.md @@ -0,0 +1,76 @@ +# Dependent homotopies + +```agda +module foundation.dependent-homotopies where +``` + +
Imports + +```agda +open import foundation.universe-levels + +open import foundation-core.dependent-identifications +open import foundation-core.homotopies +``` + +
+ +## Idea + +Consider a [homotopy](foundation-core.homotopies.md) `H : f ~ g` between two +functions `f g : (x : A) → B x`. Furthermore, consider a type family +`C : (x : A) → B x → 𝒰` and two functions + +```text + f' : (x : A) → C x (f x) + g' : (x : A) → C x (g x) +``` + +A **dependent homotopy** from `f'` to `g'` over `H` is a family of +[dependent identifications](foundation-core.dependent-identifications.md) from +`f' x` to `g' x` over `H x`. + +## Definitions + +### Dependent homotopies + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) + {f g : (x : A) → B x} (H : f ~ g) + where + + dependent-homotopy : + ((x : A) → C x (f x)) → ((x : A) → C x (g x)) → UU (l1 ⊔ l3) + dependent-homotopy f' g' = + (x : A) → dependent-identification (C x) (H x) (f' x) (g' x) +``` + +### The reflexive dependent homotopy + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) + {f : (x : A) → B x} + where + + refl-dependent-homotopy : + {f' : (x : A) → C x (f x)} → dependent-homotopy C refl-htpy f' f' + refl-dependent-homotopy = refl-htpy +``` + +### Iterated dependent homotopies + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) + {f g : (x : A) → B x} {H K : f ~ g} (L : H ~ K) + where + + dependent-homotopy² : + {f' : (x : A) → C x (f x)} {g' : (x : A) → C x (g x)} → + dependent-homotopy C H f' g' → + dependent-homotopy C K f' g' → UU (l1 ⊔ l3) + dependent-homotopy² {f'} {g'} H' K' = + (x : A) → dependent-identification² (C x) (L x) (H' x) (K' x) +``` diff --git a/src/foundation/function-extensionality.lagda.md b/src/foundation/function-extensionality.lagda.md index a50b0c7de6..af9e61b9f9 100644 --- a/src/foundation/function-extensionality.lagda.md +++ b/src/foundation/function-extensionality.lagda.md @@ -2,8 +2,6 @@ ```agda module foundation.function-extensionality where - -open import foundation-core.function-extensionality public ```
Imports @@ -24,24 +22,83 @@ open import foundation-core.identity-types ## Idea -The function extensionality axiom asserts that identifications of (dependent) -functions are equivalently described as pointwise equalities between them. In -other words, a function is completely determined by its values. +The **function extensionality axiom** asserts that +[identifications](foundation-core.identity-types.md) of (dependent) functions +are [equivalently](foundation-core.equivalences.md) described as pointwise +equalities between them. In other words, a function is completely determined by +its values. -In this file we postulate the function extensionality axiom. Its statement is -defined in -[`foundation-core.function-extensionality`](foundation-core.function-extensionality.md). +## Definitions -## Postulate +### Equalities induce homotopies ```agda -postulate - funext : function-extensionality +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + htpy-eq : {f g : (x : A) → B x} → f ＝ g → f ~ g + htpy-eq refl = refl-htpy +``` + +### An instance of function extensionality + +This property asserts that, _given_ two functions `f` and `g`, the map + +```text + htpy-eq : f ＝ g → f ~ g +``` + +is an equivalence. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + instance-function-extensionality : (f g : (x : A) → B x) → UU (l1 ⊔ l2) + instance-function-extensionality f g = is-equiv (htpy-eq {f = f} {g}) +``` + +### Based function extensionality + +This property asserts that, _given_ a function `f`, the map + +```text + htpy-eq : f ＝ g → f ~ g ``` -### Components of `funext` +is an equivalence is an equivalence for any function `g` of the same type. ```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + based-function-extensionality : (f : (x : A) → B x) → UU (l1 ⊔ l2) + based-function-extensionality f = + (g : (x : A) → B x) → is-equiv (htpy-eq {f = f} {g}) +``` + +### The function extensionality principle with respect to a universe level + +```agda +function-extensionality-Level : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +function-extensionality-Level l1 l2 = + {A : UU l1} {B : A → UU l2} + (f g : (x : A) → B x) → + instance-function-extensionality f g +``` + +### The function extensionality axiom + +```agda +function-extensionality : UUω +function-extensionality = {l1 l2 : Level} → function-extensionality-Level l1 l2 + +postulate + funext : function-extensionality + module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where @@ -77,6 +134,26 @@ module _ ## Properties +### Naturality of `htpy-eq` + +```agda +square-htpy-eq : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B) → + ( g h : B → C) → + ( (λ (p : (y : B) → g y ＝ h y) (x : A) → p (f x)) ∘ htpy-eq) ~ + ( htpy-eq ∘ (ap (precomp f C))) +square-htpy-eq f g .g refl = refl +``` + +### Computing the action on paths of an evaluation map + +```agda +ap-ev : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (a : A) → {f g : A → B} → + (p : f ＝ g) → (ap (λ h → h a) p) ＝ htpy-eq p a +ap-ev a refl = refl +``` + ### `htpy-eq` preserves concatenation of identifications ```agda @@ -116,7 +193,10 @@ module _ ## See also -- That the univalence axiom implies function extensionality is proven in +- The fact that the univalence axiom implies function extensionality is proven + in [`foundation.univalence-implies-function-extensionality`](foundation.univalence-implies-function-extensionality.md). - Weak function extensionality is defined in [`foundation.weak-function-extensionality`](foundation.weak-function-extensionality.md). +- Transporting along homotopies is defined in + [`foundation.transport-along-homotopies`](foundation.transport-along-homotopies.md). diff --git a/src/foundation/functoriality-propositional-truncation.lagda.md b/src/foundation/functoriality-propositional-truncation.lagda.md index 80eb4d34d1..0bec93023c 100644 --- a/src/foundation/functoriality-propositional-truncation.lagda.md +++ b/src/foundation/functoriality-propositional-truncation.lagda.md @@ -9,12 +9,12 @@ module foundation.functoriality-propositional-truncation where ```agda open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.propositional-truncations open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalences -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.propositions diff --git a/src/foundation/functoriality-truncation.lagda.md b/src/foundation/functoriality-truncation.lagda.md index 99719b5469..d41e07346c 100644 --- a/src/foundation/functoriality-truncation.lagda.md +++ b/src/foundation/functoriality-truncation.lagda.md @@ -9,13 +9,13 @@ module foundation.functoriality-truncation where ```agda open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.truncations open import foundation.universe-levels open import foundation-core.commuting-squares-of-maps open import foundation-core.contractible-types open import foundation-core.equivalences -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.truncation-levels diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md index ceb2020f8b..2d9062cd1d 100644 --- a/src/foundation/homotopies.lagda.md +++ b/src/foundation/homotopies.lagda.md @@ -12,6 +12,7 @@ open import foundation-core.homotopies public open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.binary-equivalences +open import foundation.commuting-squares-of-identifications open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.homotopy-induction @@ -234,7 +235,8 @@ module _ compute-dependent-identification-eq-value-function : {a0 a1 : A} (p : a0 ＝ a1) (q : f a0 ＝ g a0) (q' : f a1 ＝ g a1) → - (((ap f p) ∙ q') ＝ (q ∙ (ap g p))) ≃ ((tr (eq-value f g) p q) ＝ q') + ( coherence-square-identifications q (ap f p) (ap g p) q') ≃ + ( tr (eq-value f g) p q ＝ q') pr1 (compute-dependent-identification-eq-value-function p q q') = map-compute-dependent-identification-eq-value-function f g p q q' pr2 (compute-dependent-identification-eq-value-function p q q') = diff --git a/src/foundation/homotopy-induction.lagda.md b/src/foundation/homotopy-induction.lagda.md index d213deb6c4..3e8644fcfe 100644 --- a/src/foundation/homotopy-induction.lagda.md +++ b/src/foundation/homotopy-induction.lagda.md @@ -133,4 +133,4 @@ module _ ## See also - [Homotopies](foundation.homotopies.md). -- [Function extensionality](foundation-core.function-extensionality.md). +- [Function extensionality](foundation.function-extensionality.md). diff --git a/src/foundation/lawveres-fixed-point-theorem.lagda.md b/src/foundation/lawveres-fixed-point-theorem.lagda.md index 749b5aeac7..00323ca065 100644 --- a/src/foundation/lawveres-fixed-point-theorem.lagda.md +++ b/src/foundation/lawveres-fixed-point-theorem.lagda.md @@ -9,11 +9,11 @@ module foundation.lawveres-fixed-point-theorem where ```agda open import foundation.dependent-pair-types open import foundation.existential-quantification +open import foundation.function-extensionality open import foundation.propositional-truncations open import foundation.surjective-maps open import foundation.universe-levels -open import foundation-core.function-extensionality open import foundation-core.identity-types ``` diff --git a/src/foundation/negated-equality.lagda.md b/src/foundation/negated-equality.lagda.md index 94b324dbad..4959d79292 100644 --- a/src/foundation/negated-equality.lagda.md +++ b/src/foundation/negated-equality.lagda.md @@ -10,11 +10,11 @@ module foundation.negated-equality where open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.negation open import foundation.universe-levels open import foundation-core.cartesian-product-types -open import foundation-core.function-extensionality open import foundation-core.identity-types open import foundation-core.propositions ``` diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md index 45af40a7d8..4bf44f330e 100644 --- a/src/foundation/path-algebra.lagda.md +++ b/src/foundation/path-algebra.lagda.md @@ -66,11 +66,11 @@ horizontal-concat-square : {l : Level} {A : UU l} {a b c d e f : A} (p-lleft : a ＝ b) (p-lbottom : b ＝ d) (p-rbottom : d ＝ f) (p-middle : c ＝ d) (p-ltop : a ＝ c) (p-rtop : c ＝ e) (p-rright : e ＝ f) - (s-left : coherence-square-identifications p-lleft p-lbottom p-ltop p-middle) + (s-left : coherence-square-identifications p-ltop p-lleft p-middle p-lbottom) (s-right : - coherence-square-identifications p-middle p-rbottom p-rtop p-rright) → + coherence-square-identifications p-rtop p-middle p-rright p-rbottom) → coherence-square-identifications - p-lleft (p-lbottom ∙ p-rbottom) (p-ltop ∙ p-rtop) p-rright + (p-ltop ∙ p-rtop) p-lleft p-rright (p-lbottom ∙ p-rbottom) horizontal-concat-square {a = a} {f = f} p-lleft p-lbottom p-rbottom p-middle p-ltop p-rtop p-rright s-left s-right = ( inv (assoc p-lleft p-lbottom p-rbottom)) ∙ @@ -81,13 +81,13 @@ horizontal-concat-square {a = a} {f = f} horizontal-unit-square : {l : Level} {A : UU l} {a b : A} (p : a ＝ b) → - coherence-square-identifications p refl refl p + coherence-square-identifications refl p p refl horizontal-unit-square p = right-unit left-unit-law-horizontal-concat-square : {l : Level} {A : UU l} {a b c d : A} (p-left : a ＝ b) (p-bottom : b ＝ d) (p-top : a ＝ c) (p-right : c ＝ d) → - (s : coherence-square-identifications p-left p-bottom p-top p-right) → + (s : coherence-square-identifications p-top p-left p-right p-bottom) → ( horizontal-concat-square p-left refl p-bottom p-left refl p-top p-right ( horizontal-unit-square p-left) @@ -100,11 +100,11 @@ vertical-concat-square : {l : Level} {A : UU l} {a b c d e f : A} (p-tleft : a ＝ b) (p-bleft : b ＝ c) (p-bbottom : c ＝ f) (p-middle : b ＝ e) (p-ttop : a ＝ d) (p-tright : d ＝ e) (p-bright : e ＝ f) - (s-top : coherence-square-identifications p-tleft p-middle p-ttop p-tright) + (s-top : coherence-square-identifications p-ttop p-tleft p-tright p-middle) (s-bottom : - coherence-square-identifications p-bleft p-bbottom p-middle p-bright) → + coherence-square-identifications p-middle p-bleft p-bright p-bbottom) → coherence-square-identifications - (p-tleft ∙ p-bleft) p-bbottom p-ttop (p-tright ∙ p-bright) + p-ttop (p-tleft ∙ p-bleft) (p-tright ∙ p-bright) p-bbottom vertical-concat-square {a = a} {f = f} p-tleft p-bleft p-bbottom p-middle p-ttop p-tright p-bright s-top s-bottom = ( assoc p-tleft p-bleft p-bbottom) ∙ @@ -300,10 +300,10 @@ module _ nat-sq-right-unit-Id² : coherence-square-identifications - ( right-unit) - ( α) ( horizontal-concat-Id² α refl) ( right-unit) + ( right-unit) + ( α) nat-sq-right-unit-Id² = ( ( horizontal-concat-Id² refl (inv (ap-id α))) ∙ ( nat-htpy htpy-right-unit α)) ∙ @@ -311,10 +311,10 @@ module _ nat-sq-left-unit-Id² : coherence-square-identifications - ( left-unit) - ( α) ( horizontal-concat-Id² (refl {x = refl}) α) ( left-unit) + ( left-unit) + ( α) nat-sq-left-unit-Id² = ( ( (inv (ap-id α) ∙ (nat-htpy htpy-left-unit α)) ∙ right-unit) ∙ ( inv (left-unit-law-horizontal-concat-Id² α))) ∙ inv right-unit @@ -353,20 +353,20 @@ module _ path-swap-nat-identification-left-whisk : {q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') → coherence-square-identifications - ( identification-left-whisk p β) - ( identification-right-whisk α q') ( identification-right-whisk α q) + ( identification-left-whisk p β) ( identification-left-whisk p' β) + ( identification-right-whisk α q') path-swap-nat-identification-left-whisk β = nat-htpy (htpy-identification-left-whisk β) path-swap-nat-identification-right-whisk : {p p' : x ＝ y} (α : p ＝ p') {q q' : y ＝ z} (β : q ＝ q') → coherence-square-identifications - ( identification-right-whisk α q) - ( identification-left-whisk p' β) ( identification-left-whisk p β) + ( identification-right-whisk α q) ( identification-right-whisk α q') + ( identification-left-whisk p' β) path-swap-nat-identification-right-whisk α = nat-htpy (identification-right-whisk α) @@ -400,10 +400,10 @@ module _ nat-sq-right-inv-Id² : coherence-square-identifications - ( right-inv p) - ( refl) ( horizontal-concat-Id² α (horizontal-inv-Id² α)) + ( right-inv p) ( right-inv p') + ( refl) nat-sq-right-inv-Id² = ( ( ( horizontal-concat-Id² refl (inv (ap-const refl α))) ∙ ( nat-htpy right-inv α)) ∙ @@ -416,10 +416,10 @@ module _ nat-sq-left-inv-Id² : coherence-square-identifications - ( left-inv p) - ( refl) ( horizontal-concat-Id² (horizontal-inv-Id² α) α) + ( left-inv p) ( left-inv p') + ( refl) nat-sq-left-inv-Id² = ( ( ( horizontal-concat-Id² refl (inv (ap-const refl α))) ∙ ( nat-htpy left-inv α)) ∙ @@ -499,10 +499,10 @@ module _ nat-sq-ap-inv-Id² : coherence-square-identifications - ( ap-inv f p) - ( horizontal-inv-Id² (ap² f α)) ( ap² f (horizontal-inv-Id² α)) + ( ap-inv f p) ( ap-inv f p') + ( horizontal-inv-Id² (ap² f α)) nat-sq-ap-inv-Id² = (inv (horizontal-concat-Id² refl (ap-comp inv (ap f) α)) ∙ (nat-htpy (ap-inv f) α)) ∙ @@ -518,17 +518,17 @@ module _ where nat-sq-ap-id-Id² : - coherence-square-identifications (ap-id p) α (ap² id α) (ap-id p') + coherence-square-identifications (ap² id α) (ap-id p) (ap-id p') α nat-sq-ap-id-Id² = ((horizontal-concat-Id² refl (inv (ap-id α))) ∙ (nat-htpy ap-id α)) nat-sq-ap-const-Id² : (b : B) → coherence-square-identifications - ( ap-const b p) - ( refl) ( ap² (const A B b) α) + ( ap-const b p) ( ap-const b p') + ( refl) nat-sq-ap-const-Id² b = ( inv (horizontal-concat-Id² refl (ap-const refl α))) ∙ ( nat-htpy (ap-const b) α) @@ -544,10 +544,10 @@ module _ nat-sq-ap-comp-Id² : coherence-square-identifications - ( ap-comp g f p) - ( (ap² g ∘ ap² f) α) ( ap² (g ∘ f) α) + ( ap-comp g f p) ( ap-comp g f p') + ( (ap² g ∘ ap² f) α) nat-sq-ap-comp-Id² = (horizontal-concat-Id² refl (inv (ap-comp (ap g) (ap f) α)) ∙ (nat-htpy (ap-comp g f) α)) @@ -725,12 +725,12 @@ module _ (p00̂1 : x001 ＝ x011) (p0̂01 : x001 ＝ x101) (p010̂ : x010 ＝ x011) (p0̂10 : x010 ＝ x110) (p100̂ : x100 ＝ x101) (p10̂0 : x100 ＝ x110) (p0̂11 : x011 ＝ x111) (p10̂1 : x101 ＝ x111) (p110̂ : x110 ＝ x111) - (p00̂0̂ : coherence-square-identifications p000̂ p00̂1 p00̂0 p010̂) - (p0̂00̂ : coherence-square-identifications p000̂ p0̂01 p0̂00 p100̂) - (p0̂0̂0 : coherence-square-identifications p00̂0 p0̂10 p0̂00 p10̂0) - (p0̂0̂1 : coherence-square-identifications p00̂1 p0̂11 p0̂01 p10̂1) - (p0̂10̂ : coherence-square-identifications p010̂ p0̂11 p0̂10 p110̂) - (p10̂0̂ : coherence-square-identifications p100̂ p10̂1 p10̂0 p110̂) → UU l + (p00̂0̂ : coherence-square-identifications p00̂0 p000̂ p010̂ p00̂1) + (p0̂00̂ : coherence-square-identifications p0̂00 p000̂ p100̂ p0̂01) + (p0̂0̂0 : coherence-square-identifications p0̂00 p00̂0 p10̂0 p0̂10) + (p0̂0̂1 : coherence-square-identifications p0̂01 p00̂1 p10̂1 p0̂11) + (p0̂10̂ : coherence-square-identifications p0̂10 p010̂ p110̂ p0̂11) + (p10̂0̂ : coherence-square-identifications p10̂0 p100̂ p110̂ p10̂1) → UU l cube p000̂ p00̂0 p0̂00 p00̂1 p0̂01 p010̂ p0̂10 p100̂ p10̂0 p0̂11 p10̂1 p110̂ p00̂0̂ p0̂00̂ p0̂0̂0 p0̂0̂1 p0̂10̂ p10̂0̂ = diff --git a/src/foundation/set-quotients.lagda.md b/src/foundation/set-quotients.lagda.md index 22ec38744d..02f23d8a97 100644 --- a/src/foundation/set-quotients.lagda.md +++ b/src/foundation/set-quotients.lagda.md @@ -13,6 +13,7 @@ open import foundation.effective-maps-equivalence-relations open import foundation.embeddings open import foundation.equivalence-classes open import foundation.equivalences +open import foundation.function-extensionality open import foundation.identity-types open import foundation.inhabited-subtypes open import foundation.reflecting-maps-equivalence-relations @@ -25,7 +26,6 @@ open import foundation.universal-property-set-quotients open import foundation.universe-levels open import foundation-core.equivalence-relations -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.functoriality-dependent-function-types open import foundation-core.homotopies diff --git a/src/foundation/transport-along-higher-identifications.lagda.md b/src/foundation/transport-along-higher-identifications.lagda.md index 44efce26a7..babae89b03 100644 --- a/src/foundation/transport-along-higher-identifications.lagda.md +++ b/src/foundation/transport-along-higher-identifications.lagda.md @@ -13,9 +13,10 @@ open import foundation.dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.path-algebra -open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation.whiskering-homotopies + +open import foundation-core.transport-along-identifications ```
@@ -49,10 +50,10 @@ module _ tr²-Id-right : (α : q ＝ q') (p : a ＝ b) → coherence-square-identifications - ( tr² (Id a) α p) - ( tr-Id-right q' p) ( tr-Id-right q p) + ( tr² (Id a) α p) ( identification-left-whisk p α) + ( tr-Id-right q' p) tr²-Id-right α p = inv-nat-htpy (λ (t : b ＝ c) → tr-Id-right t p) α ``` @@ -78,19 +79,19 @@ module _ tr²-left-whisk : (p : x ＝ y) {q q' : y ＝ z} (β : q ＝ q') (b : B x) → coherence-square-identifications - ( tr² B (identification-left-whisk p β) b) - ( tr-concat p q' b) ( tr-concat p q b) + ( tr² B (identification-left-whisk p β) b) ( htpy-right-whisk (tr² B β) (tr B p) b) + ( tr-concat p q' b) tr²-left-whisk refl refl b = refl tr²-right-whisk : {p p' : x ＝ y} (α : p ＝ p') (q : y ＝ z) (b : B x) → coherence-square-identifications - ( tr² B (identification-right-whisk α q) b) - ( tr-concat p' q b) ( tr-concat p q b) + ( tr² B (identification-right-whisk α q) b) ( htpy-left-whisk (tr B q) (tr² B α) b) + ( tr-concat p' q b) tr²-right-whisk refl refl b = inv right-unit ``` @@ -105,43 +106,43 @@ module _ tr³-htpy-swap-path-swap : {q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') (b : B x) → coherence-square-identifications + ( ( identification-right-whisk + ( tr²-concat (identification-left-whisk p β) + ( identification-right-whisk α q') b) + ( tr-concat p' q' b)) ∙ + ( vertical-concat-square + ( tr² B (identification-left-whisk p β) b) + ( tr² B (identification-right-whisk α q') b) + ( tr-concat p' q' b) + ( tr-concat p q' b) + ( tr-concat p q b) + ( htpy-right-whisk (tr² B β) (tr B p) b) + ( htpy-left-whisk (tr B q') (tr² B α) b) + ( tr²-left-whisk p β b) + ( tr²-right-whisk α q' b))) ( identification-right-whisk ( tr³ ( B) ( path-swap-nat-identification-left-whisk β α) ( b)) ( tr-concat p' q' b)) + ( identification-left-whisk + ( tr-concat p q b) + ( htpy-swap-nat-right-htpy (tr² B β) (tr² B α) b)) ( ( identification-right-whisk ( tr²-concat ( identification-right-whisk α q) ( identification-left-whisk p' β) b) ( tr-concat p' q' b)) ∙ - ( vertical-concat-square - ( tr² B (identification-right-whisk α q) b) - ( tr² B (identification-left-whisk p' β) b) - ( tr-concat p' q' b) - ( tr-concat p' q b) - ( tr-concat p q b) - ( htpy-left-whisk (tr B q) (tr² B α) b) - ( htpy-right-whisk (tr² B β) (tr B p') b) - ( tr²-right-whisk α q b) - ( tr²-left-whisk p' β b))) - ( ( identification-right-whisk - ( tr²-concat (identification-left-whisk p β) - ( identification-right-whisk α q') b) - ( tr-concat p' q' b)) ∙ - ( vertical-concat-square - ( tr² B (identification-left-whisk p β) b) - ( tr² B (identification-right-whisk α q') b) - ( tr-concat p' q' b) - ( tr-concat p q' b) - ( tr-concat p q b) - ( htpy-right-whisk (tr² B β) (tr B p) b) - ( htpy-left-whisk (tr B q') (tr² B α) b) - ( tr²-left-whisk p β b) - ( tr²-right-whisk α q' b))) - ( identification-left-whisk - ( tr-concat p q b) - ( htpy-swap-nat-right-htpy (tr² B β) (tr² B α) b)) + ( vertical-concat-square + ( tr² B (identification-right-whisk α q) b) + ( tr² B (identification-left-whisk p' β) b) + ( tr-concat p' q' b) + ( tr-concat p' q b) + ( tr-concat p q b) + ( htpy-left-whisk (tr B q) (tr² B α) b) + ( htpy-right-whisk (tr² B β) (tr B p') b) + ( tr²-right-whisk α q b) + ( tr²-left-whisk p' β b))) tr³-htpy-swap-path-swap {q = refl} refl {p = refl} refl b = refl ``` diff --git a/src/foundation/transport-along-homotopies.lagda.md b/src/foundation/transport-along-homotopies.lagda.md new file mode 100644 index 0000000000..7d6f72b731 --- /dev/null +++ b/src/foundation/transport-along-homotopies.lagda.md @@ -0,0 +1,84 @@ +# Transport along homotopies + +```agda +module foundation.transport-along-homotopies where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.function-extensionality +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.transport-along-higher-identifications +open import foundation.universe-levels + +open import foundation-core.identity-types +open import foundation-core.transport-along-identifications +``` + +
+ +## Idea + +If `C : (x : A) → B x → 𝒰` is a type family, and `H : f ~ g` is a homotopy +between functions `f g : (x : A) → B x`, then there is a natural transport +operation that transports an element `z : C x (f x)` along the homotopy `H` to +an element of type `C x (g x)`. + +## Definitions + +### Transporting along homotopies + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) + {f g : (x : A) → B x} + where + + tr-htpy : + (f ~ g) → ((x : A) → C x (f x)) → ((x : A) → C x (g x)) + tr-htpy H f' x = tr (C x) (H x) (f' x) + + tr-htpy² : + {H K : f ~ g} (L : H ~ K) (f' : (x : A) → C x (f x)) → + tr-htpy H f' ~ tr-htpy K f' + tr-htpy² L f' x = tr² (C x) (L x) (f' x) +``` + +## Properties + +### Transport along a homotopy `H` is homotopic to transport along the identification `eq-htpy H` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) + where + + statement-compute-tr-htpy : + {f g : (x : A) → B x} (H : f ~ g) → UU (l1 ⊔ l3) + statement-compute-tr-htpy H = + tr (λ u → (x : A) → C x (u x)) (eq-htpy H) ~ tr-htpy C H + + base-case-compute-tr-htpy : + {f : (x : A) → B x} → statement-compute-tr-htpy (refl-htpy' f) + base-case-compute-tr-htpy = + htpy-eq (ap (tr (λ u → (x : A) → C x (u x))) (eq-htpy-refl-htpy _)) + + abstract + compute-tr-htpy : + {f g : (x : A) → B x} (H : f ~ g) → statement-compute-tr-htpy H + compute-tr-htpy {f} {g} = + ind-htpy f + ( λ _ → statement-compute-tr-htpy) + ( base-case-compute-tr-htpy) + + compute-tr-htpy-refl-htpy : + {f : (x : A) → B x} → + compute-tr-htpy (refl-htpy' f) ＝ base-case-compute-tr-htpy + compute-tr-htpy-refl-htpy {f} = + compute-ind-htpy f + ( λ _ → statement-compute-tr-htpy) + ( base-case-compute-tr-htpy) +``` diff --git a/src/foundation/transport-along-identifications.lagda.md b/src/foundation/transport-along-identifications.lagda.md index 19aee17a05..12cf640e41 100644 --- a/src/foundation/transport-along-identifications.lagda.md +++ b/src/foundation/transport-along-identifications.lagda.md @@ -12,12 +12,13 @@ open import foundation-core.transport-along-identifications public open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-identifications open import foundation.dependent-pair-types +open import foundation.homotopies open import foundation.path-algebra +open import foundation.transport-along-higher-identifications open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.function-types -open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.whiskering-homotopies ``` @@ -84,24 +85,6 @@ substitution-law-tr : substitution-law-tr B f refl = refl ``` -### Computing transport in the type family of identifications with a fixed target - -```agda -tr-Id-left : - {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : b ＝ a) → - tr (_＝ a) q p ＝ ((inv q) ∙ p) -tr-Id-left refl p = refl -``` - -### Computing transport in the type family of identifications with a fixed source - -```agda -tr-Id-right : - {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : a ＝ b) → - tr (a ＝_) q p ＝ (p ∙ q) -tr-Id-right refl refl = refl -``` - ### Computing transport of loops ```agda diff --git a/src/foundation/uniqueness-set-quotients.lagda.md b/src/foundation/uniqueness-set-quotients.lagda.md index e93f996528..5afe565939 100644 --- a/src/foundation/uniqueness-set-quotients.lagda.md +++ b/src/foundation/uniqueness-set-quotients.lagda.md @@ -10,6 +10,7 @@ module foundation.uniqueness-set-quotients where open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalences +open import foundation.function-extensionality open import foundation.reflecting-maps-equivalence-relations open import foundation.sets open import foundation.subtype-identity-principle @@ -18,7 +19,6 @@ open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalence-relations -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.functoriality-function-types open import foundation-core.homotopies diff --git a/src/foundation/univalence-implies-function-extensionality.lagda.md b/src/foundation/univalence-implies-function-extensionality.lagda.md index 3722baad26..7eb97ba0d2 100644 --- a/src/foundation/univalence-implies-function-extensionality.lagda.md +++ b/src/foundation/univalence-implies-function-extensionality.lagda.md @@ -9,6 +9,7 @@ module foundation.univalence-implies-function-extensionality where ```agda open import foundation.dependent-pair-types open import foundation.equivalence-induction +open import foundation.function-extensionality open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation.weak-function-extensionality @@ -16,7 +17,6 @@ open import foundation.weak-function-extensionality open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.fibers-of-maps -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types @@ -28,7 +28,7 @@ open import foundation-core.transport-along-identifications ## Idea The [univalence axiom](foundation-core.univalence.md) implies -[function extensionality](foundation-core.function-extensionality.md). +[function extensionality](foundation.function-extensionality.md). ## Theorem diff --git a/src/foundation/weak-function-extensionality.lagda.md b/src/foundation/weak-function-extensionality.lagda.md index 34f2b61906..0e41c31c87 100644 --- a/src/foundation/weak-function-extensionality.lagda.md +++ b/src/foundation/weak-function-extensionality.lagda.md @@ -11,6 +11,7 @@ open import foundation.action-on-identifications-functions open import foundation.decidable-equality open import foundation.decidable-types open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.fundamental-theorem-of-identity-types open import foundation.universe-levels @@ -19,7 +20,6 @@ open import foundation-core.coproduct-types open import foundation-core.empty-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences -open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.propositions @@ -32,7 +32,7 @@ open import foundation-core.propositions **Weak function extensionality** is the principle that any dependent product of [contractible types](foundation-core.contractible-types.md) is contractible. This principle is [equivalent](foundation-core.equivalences.md) to -[the function extensionality axiom](foundation-core.function-extensionality.md). +[the function extensionality axiom](foundation.function-extensionality.md). ## Definition diff --git a/src/group-theory/isomorphisms-semigroups.lagda.md b/src/group-theory/isomorphisms-semigroups.lagda.md index 7a3dd8cf15..9b02b7058e 100644 --- a/src/group-theory/isomorphisms-semigroups.lagda.md +++ b/src/group-theory/isomorphisms-semigroups.lagda.md @@ -13,6 +13,7 @@ open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences +open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies @@ -23,8 +24,6 @@ open import foundation.torsorial-type-families open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels -open import foundation-core.function-extensionality - open import group-theory.equivalences-semigroups open import group-theory.homomorphisms-semigroups open import group-theory.precategory-of-semigroups diff --git a/src/synthetic-homotopy-theory/acyclic-types.lagda.md b/src/synthetic-homotopy-theory/acyclic-types.lagda.md index d138ed4669..63214580ab 100644 --- a/src/synthetic-homotopy-theory/acyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-types.lagda.md @@ -18,7 +18,9 @@ open import synthetic-homotopy-theory.suspensions-of-types ## Idea -A type `A` is said to be **acyclic** if its suspension is contractible. +A type `A` is said to be **acyclic** if its +[suspension](synthetic-homotopy-theory.suspensions-of-types.md) is +[contractible](foundation.contractible-types.md). ## Definition diff --git a/src/synthetic-homotopy-theory/cavallos-trick.lagda.md b/src/synthetic-homotopy-theory/cavallos-trick.lagda.md index 0baefe38cf..a147b24389 100644 --- a/src/synthetic-homotopy-theory/cavallos-trick.lagda.md +++ b/src/synthetic-homotopy-theory/cavallos-trick.lagda.md @@ -24,10 +24,13 @@ open import structured-types.pointed-types ## Idea -Cavallo's trick is a way of upgrading an unpointed homotopy between pointed maps -to a pointed homotopy. Originally, this trick was formulated by Evan Cavallo for -homogeneous spaces, but it works as soon as the evaluation map `(id ~ id) → Ω B` -has a section. +**Cavallo's trick** is a way of upgrading an unpointed +[homotopy](foundation.homotopies.md) between +[pointed maps](structured-types.pointed-maps.md) to a +[pointed homotopy](structured-types.pointed-homotopies.md). + +Originally, this trick was formulated by Evan Cavallo for homogeneous spaces, +but it works as soon as the evaluation map `(id ~ id) → Ω B` has a section. ## Theorem diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index d4f1738a83..469a67856c 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -43,6 +43,11 @@ open import univalent-combinatorics.standard-finite-types +## Idea + +**The circle** is the initial type equipped with a base point and a +[loop](synthetic-homotopy-theory.loop-spaces.md). + ## Postulates ```agda @@ -301,13 +306,13 @@ sphere-1-circle-sphere-1-south-sphere-1 = apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 : ( n : Fin 2) → coherence-square-identifications - ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n))) - ( sphere-1-circle-sphere-1-south-sphere-1) ( ap ( sphere-1-circle) ( ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹) ∙ ( map-sphere-0-eq-base-𝕊¹ n))) + ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n))) ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) + ( sphere-1-circle-sphere-1-south-sphere-1) apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n = ( inv ( assoc @@ -333,10 +338,10 @@ apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n = apply-loop-universal-property-𝕊¹-sphere-1-circle-sphere-1 : coherence-square-identifications - ( ap sphere-1-circle loop-𝕊¹) - ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1) + ( ap sphere-1-circle loop-𝕊¹) ( meridian-sphere 0 (zero-Fin 1)) + ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) apply-loop-universal-property-𝕊¹-sphere-1-circle-sphere-1 = ( inv ( assoc @@ -447,10 +452,10 @@ circle-sphere-1-circle-base-𝕊¹ = apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle : coherence-square-identifications - ( ap circle-sphere-1 (inv (meridian-sphere 0 (one-Fin 1)))) - ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹) ( refl) + ( ap circle-sphere-1 (inv (meridian-sphere 0 (one-Fin 1)))) ( circle-sphere-1-south-sphere-1-eq-base-𝕊¹) + ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹) apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle = ( identification-right-whisk ( ap-inv @@ -478,10 +483,10 @@ apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle = apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle : coherence-square-identifications - ( ap (circle-sphere-1) (north-sphere-1-loop)) - ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹) ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹) + ( ap (circle-sphere-1) (north-sphere-1-loop)) ( loop-𝕊¹) + ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹) apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle = ( identification-right-whisk ( ap-concat @@ -504,10 +509,10 @@ apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle = circle-sphere-1-circle-loop-𝕊¹ : coherence-square-identifications - ( ap circle-sphere-1 (ap sphere-1-circle loop-𝕊¹)) - ( circle-sphere-1-circle-base-𝕊¹) ( circle-sphere-1-circle-base-𝕊¹) + ( ap circle-sphere-1 (ap sphere-1-circle loop-𝕊¹)) ( loop-𝕊¹) + ( circle-sphere-1-circle-base-𝕊¹) circle-sphere-1-circle-loop-𝕊¹ = ( inv ( assoc diff --git a/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md index a6a1a67148..6c606499df 100644 --- a/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md @@ -24,8 +24,12 @@ open import synthetic-homotopy-theory.cocones-under-spans ## Idea -A cocone under a span of pointed types is a **pointed cocone** if it consists of -pointed maps such that the proofs of point-preservation cohere. +A [cocone under a span](synthetic-homotopy-theory.cocones-under-spans.md) of +[pointed types](structured-types.pointed-types.md) is a **pointed cocone** if it +consists of [pointed maps](structured-types.pointed-maps.md) equipped with a +[pointed homotopy](structured-types.pointed-homotopies.md) witnessing that the +naturality square +[commutes](structured-types.commuting-squares-of-pointed-maps.md). The type of pointed cocones under a span of pointed types is again canonically pointed at the constant cocone, with `refl` as coherence proof. diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md index a96698838e..9cd48baab3 100644 --- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md @@ -31,8 +31,9 @@ open import foundation-core.torsorial-type-families ## Idea -A cocone under a span `A <-f- S -g-> B` with vertex `X` consists of two maps -`i : A → X` and `j : B → X` equipped with a homotopy witnessing that the square +A **cocone under a [span](foundation.spans.md)** `A <-f- S -g-> B` with codomain +`X` consists of two maps `i : A → X` and `j : B → X` equipped with a +[homotopy](foundation.homotopies.md) witnessing that the square ```text g @@ -44,7 +45,7 @@ A cocone under a span `A <-f- S -g-> B` with vertex `X` consists of two maps i ``` -commutes. +[commutes](foundation.commuting-squares-of-maps.md). ## Definitions diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md index 067b64566a..2a7e9afd49 100644 --- a/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md @@ -44,7 +44,8 @@ functions j' : (b : B) → P (j b) ``` -and a family of dependent identifications +and a family of +[dependent identifications](foundation.dependent-identifications.md) ```text (s : S) → dependent-identification P (H s) (i' (f s)) (j' (g s)). diff --git a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md index 2017650ebe..1f55709c41 100644 --- a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md @@ -22,6 +22,11 @@ open import synthetic-homotopy-theory.cocones-under-spans ## Idea +The **dependent pullback property** of +[pushouts](synthetic-homotopy-theory.pushouts.md) asserts that the type of +sections of a type family over a pushout can be expressed as a +[pullback](foundation.pullbacks.md). + The fact that the dependent pullback property of pushouts is [logically equivalent](foundation.logical-equivalences.md) to the [dependent universal property](synthetic-homotopy-theory.dependent-universal-property-pushouts.md) diff --git a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md index 16f582a0c6..8f3ca5a3f0 100644 --- a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md @@ -226,12 +226,12 @@ module _ ( λ S-htpy → (x : X) → coherence-square-identifications - ( meridian-dependent-suspension-structure d x) - ( S-htpy) ( ap ( tr B (meridian-suspension-structure c x)) ( N-htpy)) - ( meridian-dependent-suspension-structure d' x))) + ( meridian-dependent-suspension-structure d x) + ( meridian-dependent-suspension-structure d' x) + ( S-htpy))) module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) @@ -256,12 +256,12 @@ module _ htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1) → ( x : X) → coherence-square-identifications - ( meridian-dependent-suspension-structure d-susp-str0 x) - ( south-htpy-dependent-suspension-structure d-susp-str) ( ap ( tr B (meridian-suspension-structure susp-str x)) ( north-htpy-dependent-suspension-structure d-susp-str)) + ( meridian-dependent-suspension-structure d-susp-str0 x) ( meridian-dependent-suspension-structure d-susp-str1 x) + ( south-htpy-dependent-suspension-structure d-susp-str) meridian-htpy-dependent-suspension-structure = pr2 ∘ pr2 module _ @@ -281,10 +281,10 @@ module _ ( λ S-htpy → (x : X) → coherence-square-identifications - ( meridian-dependent-suspension-structure d x) - ( S-htpy) ( ap (tr B (meridian-suspension-structure c x)) N-htpy) - ( m x))) + ( meridian-dependent-suspension-structure d x) + ( m x) + ( S-htpy))) ( refl) ( refl , λ x → right-unit) ( λ N → id-equiv) diff --git a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md index 4ff850188b..ecfdc7c547 100644 --- a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md @@ -24,6 +24,12 @@ open import synthetic-homotopy-theory.loop-spaces +## Idea + +The **double loop space** of a [pointed type](structured-types.pointed-types.md) +`A` is the [loop space](synthetic-homotopy-theory.loop-spaces.md) of the loop +space of `A`. + ## Definition ```agda diff --git a/src/synthetic-homotopy-theory/free-loops.lagda.md b/src/synthetic-homotopy-theory/free-loops.lagda.md index d97584d218..cfb9301b46 100644 --- a/src/synthetic-homotopy-theory/free-loops.lagda.md +++ b/src/synthetic-homotopy-theory/free-loops.lagda.md @@ -25,8 +25,9 @@ open import foundation.universe-levels ## Idea -A free loop in a type `X` consists of a point `x : X` and an identification -`x ＝ x`. The type of free loops in `X` is equivalent to the type of maps +A **free loop** in a type `X` consists of a point `x : X` and an +[identification](foundation.identity-types.md) `x ＝ x`. The type of free loops +in `X` is [equivalent](foundation-core.equivalences.md) to the type of maps `𝕊¹ → X`. ## Definitions diff --git a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md index d489f066fd..af5d1a3962 100644 --- a/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/functoriality-loop-spaces.lagda.md @@ -28,9 +28,9 @@ open import synthetic-homotopy-theory.loop-spaces ## Idea Any [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` induces a -pointed map `pointed-map-Ω f : Ω A →∗ Ω B`. Furthermore, this operation respects -the groupoidal operations on -[loop spaces](synthetic-homotopy-theory.loop-spaces.md). +pointed map `pointed-map-Ω f : Ω A →∗ Ω B`` on +[loop spaces](synthetic-homotopy-theory.loop-spaces.md). Furthermore, this +operation respects the groupoidal operations on loop spaces. ## Definition diff --git a/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md b/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md index 07921e3055..cfa1ef495a 100644 --- a/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md +++ b/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md @@ -23,6 +23,14 @@ open import synthetic-homotopy-theory.loop-spaces +## Idea + +The [loop space](synthetic-homotopy-theory.loop-spaces.md) of any +[pointed](structured-types.pointed-types.md) [1-type](foundation.1-types.md) is +a [group](group-theory.groups.md). + +## Definitions + ```agda module _ {l : Level} (A : Pointed-Type l) diff --git a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md index 5e9c5ae4d4..68d89269b2 100644 --- a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md +++ b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md @@ -18,6 +18,7 @@ open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types +open import foundation.path-algebra open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.type-arithmetic-cartesian-product-types @@ -38,9 +39,12 @@ open import synthetic-homotopy-theory.powers-of-loops ## Idea -**Hatcher's** example of an acyclic type is a higher inductive type equipped -with a point and two loops `a` and `b`, and identifications witnessing that -`a⁵ ＝ b³` and `b³ = (ab)²`. +**Hatcher's [acyclic type](synthetic-homotopy-theory.acyclic-types.md)** is a +higher inductive type [equipped](foundation.structure.md) with a base point and +two [loops](synthetic-homotopy-theory.loop-spaces.md) `a` and `b`, and +[identifications](foundation.identity-types.md) witnessing that `a⁵ ＝ b³` and +`b³ = (ab)²`. This type is acyclic, because the structure on Hatcher's acyclic +type on any loop space is [contractible](foundation.contractible-types.md). ## Definitions @@ -80,19 +84,19 @@ hom-algebra-Hatcher-Acyclic-Type Σ ( map-Ω f a2 ＝ b2) ( λ v → ( coherence-square-identifications - ( map-power-nat-Ω 5 f a1 ∙ ap (power-nat-Ω 5 B) u) - ( s1) ( ap (map-Ω f) r1) - ( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)) × - coherence-square-identifications + ( map-power-nat-Ω 5 f a1 ∙ ap (power-nat-Ω 5 B) u) ( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v) - ( s2) + ( s1)) × + ( coherence-square-identifications ( ap (map-Ω f) r2) + ( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v) ( ( map-power-nat-Ω 2 f (a1 ∙ a2)) ∙ ( ap ( power-nat-Ω 2 B) ( ( preserves-mul-map-Ω f a1 a2) ∙ - ( ap-binary _∙_ u v))))))) + ( horizontal-concat-Id² u v)))) + ( s2))))) ``` ### The Hatcher acyclic type is the initial Hatcher acyclic algebra diff --git a/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md b/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md index c4f43f2b0e..d56de3d21a 100644 --- a/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md @@ -16,6 +16,7 @@ open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences +open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types @@ -28,8 +29,6 @@ open import foundation.torsorial-type-families open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels -open import foundation-core.function-extensionality - open import structured-types.equivalences-types-equipped-with-endomorphisms open import structured-types.initial-pointed-type-equipped-with-automorphism open import structured-types.mere-equivalences-types-equipped-with-endomorphisms @@ -44,6 +43,8 @@ open import univalent-combinatorics.cyclic-finite-types +## Definitions + ```agda Infinite-Cyclic-Type : (l : Level) → UU (lsuc l) Infinite-Cyclic-Type l = Cyclic-Type l zero-ℕ diff --git a/src/synthetic-homotopy-theory/interval-type.lagda.md b/src/synthetic-homotopy-theory/interval-type.lagda.md index 1492581343..eb421618ba 100644 --- a/src/synthetic-homotopy-theory/interval-type.lagda.md +++ b/src/synthetic-homotopy-theory/interval-type.lagda.md @@ -9,10 +9,13 @@ module synthetic-homotopy-theory.interval-type where ```agda open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions +open import foundation.commuting-squares-of-identifications open import foundation.contractible-types +open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality +open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle open import foundation.transport-along-identifications @@ -23,8 +26,8 @@ open import foundation.universe-levels ## Idea -The interval type is a higher inductive type with two points and an -identification between them. +**The interval type** is a higher inductive type with two points and an +[identification](foundation.identity-types.md) between them. ## Postulates @@ -41,22 +44,24 @@ postulate ind-𝕀 : {l : Level} (P : 𝕀 → UU l) (u : P source-𝕀) (v : P target-𝕀) - (q : Id (tr P path-𝕀 u) v) → (x : 𝕀) → P x + (q : dependent-identification P path-𝕀 u v) → (x : 𝕀) → P x compute-source-𝕀 : {l : Level} {P : 𝕀 → UU l} (u : P source-𝕀) (v : P target-𝕀) - (q : Id (tr P path-𝕀 u) v) → Id (ind-𝕀 P u v q source-𝕀) u + (q : dependent-identification P path-𝕀 u v) → Id (ind-𝕀 P u v q source-𝕀) u compute-target-𝕀 : {l : Level} {P : 𝕀 → UU l} (u : P source-𝕀) (v : P target-𝕀) - (q : Id (tr P path-𝕀 u) v) → Id (ind-𝕀 P u v q target-𝕀) v + (q : dependent-identification P path-𝕀 u v) → Id (ind-𝕀 P u v q target-𝕀) v compute-path-𝕀 : {l : Level} {P : 𝕀 → UU l} (u : P source-𝕀) (v : P target-𝕀) - (q : Id (tr P path-𝕀 u) v) → - Id - ( apd (ind-𝕀 P u v q) path-𝕀 ∙ compute-target-𝕀 u v q) - ( ap (tr P path-𝕀) (compute-source-𝕀 u v q) ∙ q) + (q : dependent-identification P path-𝕀 u v) → + coherence-square-identifications + ( ap (tr P path-𝕀) (compute-source-𝕀 u v q)) + ( apd (ind-𝕀 P u v q) path-𝕀) + ( q) + ( compute-target-𝕀 u v q) ``` ## Properties @@ -65,7 +70,10 @@ postulate ```agda Data-𝕀 : {l : Level} → (𝕀 → UU l) → UU l -Data-𝕀 P = Σ (P source-𝕀) (λ u → Σ (P target-𝕀) (λ v → Id (tr P path-𝕀 u) v)) +Data-𝕀 P = + Σ ( P source-𝕀) + ( λ u → + Σ ( P target-𝕀) (dependent-identification P path-𝕀 u)) ev-𝕀 : {l : Level} {P : 𝕀 → UU l} → ((x : 𝕀) → P x) → Data-𝕀 P ev-𝕀 f = triple (f source-𝕀) (f target-𝕀) (apd f path-𝕀) @@ -76,15 +84,27 @@ module _ Eq-Data-𝕀 : (x y : Data-𝕀 P) → UU l Eq-Data-𝕀 x y = - Σ ( Id (pr1 x) (pr1 y)) (λ α → - Σ ( Id (pr1 (pr2 x)) (pr1 (pr2 y))) (λ β → - Id ( pr2 (pr2 x) ∙ β) ( (ap (tr P path-𝕀) α) ∙ pr2 (pr2 y)))) + Σ ( pr1 x ＝ pr1 y) + ( λ α → + Σ ( pr1 (pr2 x) ＝ pr1 (pr2 y)) + ( λ β → + coherence-square-identifications + ( ap (tr P path-𝕀) α) + ( pr2 (pr2 x)) + ( pr2 (pr2 y)) + ( β))) extensionality-Data-𝕀 : (x y : Data-𝕀 P) → Id x y ≃ Eq-Data-𝕀 x y extensionality-Data-𝕀 (pair u (pair v α)) = extensionality-Σ ( λ {u'} vα' p → - Σ (Id v (pr1 vα')) (λ q → Id (α ∙ q) (ap (tr P path-𝕀) p ∙ pr2 vα'))) + Σ ( v ＝ pr1 vα') + ( λ q → + coherence-square-identifications + ( ap (tr P path-𝕀) p) + ( α) + ( pr2 vα') + ( q))) ( refl) ( pair refl right-unit) ( λ u' → id-equiv) @@ -105,10 +125,14 @@ module _ eq-Eq-Data-𝕀' {x} {y} = map-inv-equiv (extensionality-Data-𝕀 x y) eq-Eq-Data-𝕀 : - {x y : Data-𝕀 P} (α : Id (pr1 x) (pr1 y)) - (β : Id (pr1 (pr2 x)) (pr1 (pr2 y))) - (γ : Id (pr2 (pr2 x) ∙ β) (ap (tr P path-𝕀) α ∙ pr2 (pr2 y))) → - Id x y + {x y : Data-𝕀 P} (α : pr1 x ＝ pr1 y) (β : pr1 (pr2 x) ＝ pr1 (pr2 y)) + (γ : + coherence-square-identifications + ( ap (tr P path-𝕀) α) + ( pr2 (pr2 x)) + ( pr2 (pr2 y)) + ( β)) → + x ＝ y eq-Eq-Data-𝕀 α β γ = eq-Eq-Data-𝕀' (triple α β γ) ``` @@ -138,10 +162,13 @@ is-retraction-inv-ev-𝕀 : is-retraction-inv-ev-𝕀 {l} {P} f = eq-htpy ( ind-𝕀 - ( λ x → Id (inv-ev-𝕀 (ev-𝕀 f) x) (f x)) + ( eq-value (inv-ev-𝕀 (ev-𝕀 f)) f) ( compute-source-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀)) ( compute-target-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀)) - ( tr-value (inv-ev-𝕀 (ev-𝕀 f)) f path-𝕀 + ( map-compute-dependent-identification-eq-value + ( inv-ev-𝕀 (ev-𝕀 f)) + ( f) + ( path-𝕀) ( compute-source-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀)) ( compute-target-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀)) ( compute-path-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀)))) @@ -152,16 +179,13 @@ abstract is-equiv-ev-𝕀 P = is-equiv-is-invertible inv-ev-𝕀 is-section-inv-ev-𝕀 is-retraction-inv-ev-𝕀 -tr-eq : {l : Level} {A : UU l} {x y : A} (p : Id x y) → Id (tr (Id x) p refl) p -tr-eq refl = refl - contraction-𝕀 : (x : 𝕀) → Id source-𝕀 x contraction-𝕀 = ind-𝕀 ( Id source-𝕀) ( refl) ( path-𝕀) - ( tr-eq path-𝕀) + ( tr-Id-right path-𝕀 refl) abstract is-contr-𝕀 : is-contr 𝕀 diff --git a/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md index bca49b8f41..b6d2d3f159 100644 --- a/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md @@ -9,6 +9,7 @@ module synthetic-homotopy-theory.iterated-loop-spaces where ```agda open import elementary-number-theory.natural-numbers +open import foundation.iterating-functions open import foundation.universe-levels open import structured-types.pointed-types @@ -18,12 +19,24 @@ open import synthetic-homotopy-theory.loop-spaces +## Idea + +An **iterated loop space** `Ωⁿ A` is the +[pointed type](structured-types.pointed-types.md) obtained by `n` times +[iterating](foundation.iterating-functions.md) the +[loop space](synthetic-homotopy-theory.loop-spaces.md) functor +`Ω : Pointed-Type → Pointed-Type`. + ```agda module _ {l : Level} where iterated-loop-space : ℕ → Pointed-Type l → Pointed-Type l - iterated-loop-space zero-ℕ A = A - iterated-loop-space (succ-ℕ n) A = Ω (iterated-loop-space n A) + iterated-loop-space n = iterate n Ω ``` + +## See also + +- [Double loop spaces](synthetic-homotopy-theory.double-loop-spaces.md) +- [Triple loop spaces](synthetic-homotopy-theory.triple-loop-spaces.md) diff --git a/src/synthetic-homotopy-theory/joins-of-types.lagda.md b/src/synthetic-homotopy-theory/joins-of-types.lagda.md index fb4759be46..b1bf34beb5 100644 --- a/src/synthetic-homotopy-theory/joins-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/joins-of-types.lagda.md @@ -32,7 +32,9 @@ open import synthetic-homotopy-theory.universal-property-pushouts ## Idea -The join of `A` and `B` is the pushout of the span `A ← A × B → B`. +The **join** of `A` and `B` is the +[pushout](synthetic-homotopy-theory.pushouts.md) of the +[span](foundation.spans.md) `A ← A × B → B`. ## Definition diff --git a/src/synthetic-homotopy-theory/multiplication-circle.lagda.md b/src/synthetic-homotopy-theory/multiplication-circle.lagda.md index 9e1ac9c52c..99ce5de1b9 100644 --- a/src/synthetic-homotopy-theory/multiplication-circle.lagda.md +++ b/src/synthetic-homotopy-theory/multiplication-circle.lagda.md @@ -30,7 +30,8 @@ Classically, the circle can be viewed as the subset of the complex numbers of absolute value 1. The absolute value of a product of complex numbers is the product of their absolute values. This implies that when we multiply two complex numbers on the unit circle, the result is a complex number on the unit circle. -This multiplicative structure carries over to the homotopy type of the circle. +This multiplicative structure carries over to the homotopy type of the +[circle](synthetic-homotopy-theory.circle.md). ## Definition diff --git a/src/synthetic-homotopy-theory/plus-principle.lagda.md b/src/synthetic-homotopy-theory/plus-principle.lagda.md index 546cc8f517..30af8ac24a 100644 --- a/src/synthetic-homotopy-theory/plus-principle.lagda.md +++ b/src/synthetic-homotopy-theory/plus-principle.lagda.md @@ -19,8 +19,10 @@ open import synthetic-homotopy-theory.acyclic-types ## Idea -The **plus-principle** asserts that any acyclic 1-connected type is -contractible. +The **plus-principle** asserts that any +[acyclic](synthetic-homotopy-theory.acyclic-types.md) +[1-connected type](foundation.connected-types.md) is +[contractible](foundation.contractible-types.md). ## Definition diff --git a/src/synthetic-homotopy-theory/powers-of-loops.lagda.md b/src/synthetic-homotopy-theory/powers-of-loops.lagda.md index 68d4b8f229..6a1e1c3b88 100644 --- a/src/synthetic-homotopy-theory/powers-of-loops.lagda.md +++ b/src/synthetic-homotopy-theory/powers-of-loops.lagda.md @@ -30,8 +30,9 @@ open import synthetic-homotopy-theory.loop-spaces ## Idea -The `n`-th power of a loop `ω` in a type `A` is defined by iterated -concatenation of `ω` with itself. +The **`n`-th power of a [loop](synthetic-homotopy-theory.loop-spaces.md)** `ω` +in a type `A` is defined by [iterated](foundation.iterating-functions.md) +[concatenation](foundation.identity-types.md) of `ω` with itself. ## Definitions diff --git a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md index 7b328268d2..e781819a3a 100644 --- a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md @@ -36,9 +36,11 @@ pushout of `S` if and only if the square Y^A -----> Y^S ``` -is a pullback square for every type `Y`. Below, we first define the cone of this -commuting square, and then we introduce the type pullback-property-pushout, -which states that the above square is a pullback. +is a [pullback square](foundation.pullback-squares.md) for every type `Y`. +Below, we first define the [cone](foundation.cones-over-cospans.md) of this +[commuting square](foundation.commuting-squares-of-maps.md), and then we +introduce the type `pullback-property-pushout`, which states that the above +square is a [pullback](foundation-core.universal-property-pullbacks.md). ## Definition diff --git a/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md index 0e17c56180..3ddcacfc23 100644 --- a/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts-of-pointed-types.lagda.md @@ -23,8 +23,9 @@ open import synthetic-homotopy-theory.pushouts ## Idea -Given a span of pointed maps, then the pushout is in fact a pushout diagram in -the category of pointed types. +Given a span of [pointed maps](structured-types.pointed-maps.md), then the +[pushout](synthetic-homotopy-theory.pushouts.md) is in fact a pushout diagram in +the (wild) category of [pointed types](structured-types.pointed-types.md). ## Definition diff --git a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md index de94056b1e..2cf1d0ac32 100644 --- a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md @@ -24,8 +24,9 @@ open import synthetic-homotopy-theory.wedges-of-pointed-types ## Idea -Given two pointed types `a : A` and `b : B` we may form their **smash product** -as the following pushout +Given two [pointed types](structured-types.pointed-types.md) `a : A` and `b : B` +we may form their **smash product** as the following +[pushout](synthetic-homotopy-theory.pushouts.md) ```text A ∨∗ B ----> A ×∗ B @@ -36,7 +37,9 @@ as the following pushout ``` where the map `A ∨∗ B → A ×∗ B` is the canonical inclusion -`map-wedge-prod-Pointed-Type`. +`map-wedge-prod-Pointed-Type` from the +[wedge](synthetic-homotopy-theory.wedges-of-pointed-types.md) into the +[pointed cartesian product](structured-types.pointed-cartesian-product-types.md). ## Definition diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index b69dfaa20f..a19d91dedd 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -279,14 +279,14 @@ module _ ( suspension-structure-suspension X)) (x : X) → coherence-square-identifications - ( apd - ( map-inv-dependent-up-suspension d) - ( meridian-suspension x)) - ( dependent-up-suspension-south-suspension d) ( ap ( tr B (meridian-suspension x)) ( dependent-up-suspension-north-suspension d)) + ( apd + ( map-inv-dependent-up-suspension d) + ( meridian-suspension x)) ( meridian-dependent-suspension-structure d x) + ( dependent-up-suspension-south-suspension d) dependent-up-suspension-meridian-suspension d = meridian-htpy-dependent-suspension-structure ( B) @@ -315,10 +315,10 @@ module _ ( λ q → (x : X) → coherence-square-identifications - ( ap f (meridian-suspension x)) - ( q) ( p) - ( ap g (meridian-suspension x)))) + ( ap f (meridian-suspension x)) + ( ap g (meridian-suspension x)) + ( q))) north-htpy-function-out-of-suspension : htpy-function-out-of-suspension → @@ -334,45 +334,31 @@ module _ (h : htpy-function-out-of-suspension) → (x : X) → coherence-square-identifications - ( ap f (meridian-suspension x)) - ( south-htpy-function-out-of-suspension h) ( north-htpy-function-out-of-suspension h) + ( ap f (meridian-suspension x)) ( ap g (meridian-suspension x)) + ( south-htpy-function-out-of-suspension h) meridian-htpy-function-out-of-suspension = pr2 ∘ pr2 equiv-htpy-function-out-of-suspension-htpy : (f ~ g) ≃ htpy-function-out-of-suspension equiv-htpy-function-out-of-suspension-htpy = - equivalence-reasoning - (f ~ g) - ≃ dependent-suspension-structure - ( eq-value f g) - ( suspension-structure-suspension X) - by equiv-dependent-up-suspension (eq-value f g) - ≃ htpy-function-out-of-suspension - by + ( equiv-tot + ( λ p → equiv-tot - ( λ p → - equiv-tot - ( λ q → - equiv-Π - ( λ x → - coherence-square-identifications - ( ap f (meridian-suspension x)) - ( q) - ( p) - ( ap g (meridian-suspension x))) - ( id-equiv) - ( λ x → - inv-equiv - ( compute-dependent-identification-eq-value-function - ( f) - ( g) - ( meridian-suspension-structure - ( suspension-structure-suspension X) - ( x)) - ( p) - ( q))))) + ( λ q → + equiv-Π-equiv-family + ( λ x → + inv-equiv + ( compute-dependent-identification-eq-value-function + ( f) + ( g) + ( meridian-suspension-structure + ( suspension-structure-suspension X) + ( x)) + ( p) + ( q)))))) ∘e + ( equiv-dependent-up-suspension (eq-value f g)) htpy-function-out-of-suspension-htpy : (f ~ g) → htpy-function-out-of-suspension diff --git a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md index 255444edda..755771796b 100644 --- a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md @@ -22,6 +22,11 @@ open import synthetic-homotopy-theory.iterated-loop-spaces +## Idea + +A **triple loop space** is a three times +[iterated loop space](synthetic-homotopy-theory.iterated-loop-spaces.md). + ## Definition ```agda