From 2fa02f6f1a8d4a064589695b7e74b07b0bcd2f3a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 12:09:33 +0100 Subject: [PATCH 01/16] pointed function h-spaces --- src/structured-types.lagda.md | 2 + ...inted-dependent-function-h-spaces.lagda.md | 153 ++++++++++++++++++ .../pointed-dependent-functions.lagda.md | 1 + .../pointed-function-h-spaces.lagda.md | 102 ++++++++++++ 4 files changed, 258 insertions(+) create mode 100644 src/structured-types/pointed-dependent-function-h-spaces.lagda.md create mode 100644 src/structured-types/pointed-function-h-spaces.lagda.md diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index dc561cf951..cdc006f621 100644 --- a/src/structured-types.lagda.md +++ b/src/structured-types.lagda.md @@ -54,10 +54,12 @@ open import structured-types.noncoherent-h-spaces public open import structured-types.opposite-pointed-spans public open import structured-types.pointed-2-homotopies public open import structured-types.pointed-cartesian-product-types public +open import structured-types.pointed-dependent-function-h-spaces public open import structured-types.pointed-dependent-functions public open import structured-types.pointed-dependent-pair-types public open import structured-types.pointed-equivalences public open import structured-types.pointed-families-of-types public +open import structured-types.pointed-function-h-spaces public open import structured-types.pointed-homotopies public open import structured-types.pointed-isomorphisms public open import structured-types.pointed-maps public diff --git a/src/structured-types/pointed-dependent-function-h-spaces.lagda.md b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md new file mode 100644 index 0000000000..fe0ee49719 --- /dev/null +++ b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md @@ -0,0 +1,153 @@ +# Pointed dependent function H-spaces + +```agda +module structured-types.pointed-dependent-function-h-spaces where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.unital-binary-operations +open import foundation.universe-levels + +open import structured-types.h-spaces +open import structured-types.noncoherent-h-spaces +open import structured-types.pointed-dependent-functions +open import structured-types.pointed-homotopies +open import structured-types.pointed-types +``` + +
+ +## Idea + +Given a family of [H-spaces](structured-types.h-spaces.md) `M i` indexed by a +[pointed type](structured-types.pointed-types.md) `i∗ : I`, the +{{#concept "pointed dependent functions" Disambiguation="H-space" Agda=pointed-Π-H-Space}} +`Π∗(i : I), M i` is an H-space consisting of +[pointed dependent functions](structured-types.pointed-dependent-functions.md) +taking `i : I` to an element of the underlying type of `M i`, and taking `i∗` to +the unit of `M i∗`. The multiplication is given pointwise, and at the base point +by the +[binary action on identifications](foundation.action-on-identifications-binary-functions.md) +of the multiplication operation of `M i∗`. + +## Definition + +```agda +module _ + {l1 l2 : Level} (I∗ : Pointed-Type l1) + (let I = type-Pointed-Type I∗) + (let i∗ = point-Pointed-Type I∗) + (M : I → H-Space l2) + where + + type-pointed-Π-H-Space : UU (l1 ⊔ l2) + type-pointed-Π-H-Space = Π∗ I∗ (type-H-Space ∘ M , unit-H-Space (M i∗)) + + unit-pointed-Π-H-Space : type-pointed-Π-H-Space + unit-pointed-Π-H-Space = (unit-H-Space ∘ M , refl) + + pointed-type-pointed-Π-H-Space : Pointed-Type (l1 ⊔ l2) + pointed-type-pointed-Π-H-Space = + ( type-pointed-Π-H-Space , unit-pointed-Π-H-Space) + + mul-pointed-Π-H-Space : + type-pointed-Π-H-Space → type-pointed-Π-H-Space → type-pointed-Π-H-Space + pr1 (mul-pointed-Π-H-Space (f , f∗) (g , g∗)) i = + mul-H-Space (M i) (f i) (g i) + pr2 (mul-pointed-Π-H-Space (f , f∗) (g , g∗)) = + ( ap-binary (mul-H-Space (M i∗)) f∗ g∗) ∙ + ( left-unit-law-mul-H-Space (M i∗) (unit-H-Space (M i∗))) + + pointed-htpy-left-unit-law-mul-pointed-Π-H-Space : + (f : type-pointed-Π-H-Space) → + mul-pointed-Π-H-Space unit-pointed-Π-H-Space f ~∗ f + pr1 (pointed-htpy-left-unit-law-mul-pointed-Π-H-Space (f , f∗)) i = + left-unit-law-mul-H-Space (M i) (f i) + pr2 (pointed-htpy-left-unit-law-mul-pointed-Π-H-Space (f , f∗)) = + inv-nat-htpy-id (left-unit-law-mul-H-Space (M i∗)) f∗ + + left-unit-law-mul-pointed-Π-H-Space : + (f : type-pointed-Π-H-Space) → + mul-pointed-Π-H-Space unit-pointed-Π-H-Space f ＝ f + left-unit-law-mul-pointed-Π-H-Space f = + eq-pointed-htpy + ( mul-pointed-Π-H-Space unit-pointed-Π-H-Space f) + ( f) + ( pointed-htpy-left-unit-law-mul-pointed-Π-H-Space f) + + pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' : + (f : type-pointed-Π-H-Space) → + mul-pointed-Π-H-Space f unit-pointed-Π-H-Space ~∗ f + pr1 (pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' (f , f∗)) i = + right-unit-law-mul-H-Space (M i) (f i) + pr2 (pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' (f , f∗)) = + equational-reasoning + (ap (λ f → mul-H-Space (M i∗) f (unit-H-Space (M i∗))) f∗ ∙ refl) ∙ + left-unit-law-mul-H-Space (M i∗) (unit-H-Space (M i∗)) + ＝ ap (λ f → mul-H-Space (M i∗) f (unit-H-Space (M i∗))) f∗ ∙ + right-unit-law-mul-H-Space (M i∗) (unit-H-Space (M i∗)) + by ap-binary (_∙_) right-unit (coh-unit-laws-mul-H-Space (M i∗)) + ＝ right-unit-law-mul-H-Space (M i∗) (f i∗) ∙ f∗ + by inv-nat-htpy-id (right-unit-law-mul-H-Space (M i∗)) f∗ + + right-unit-law-mul-pointed-Π-H-Space' : + (f : type-pointed-Π-H-Space) → + mul-pointed-Π-H-Space f unit-pointed-Π-H-Space ＝ f + right-unit-law-mul-pointed-Π-H-Space' f = + eq-pointed-htpy + ( mul-pointed-Π-H-Space f unit-pointed-Π-H-Space) + ( f) + ( pointed-htpy-right-unit-law-mul-pointed-Π-H-Space' f) + + noncoherent-h-space-pointed-Π-H-Space : Noncoherent-H-Space (l1 ⊔ l2) + noncoherent-h-space-pointed-Π-H-Space = + ( pointed-type-pointed-Π-H-Space , + mul-pointed-Π-H-Space , + left-unit-law-mul-pointed-Π-H-Space , + right-unit-law-mul-pointed-Π-H-Space') + + pointed-Π-H-Space : H-Space (l1 ⊔ l2) + pointed-Π-H-Space = + h-space-Noncoherent-H-Space noncoherent-h-space-pointed-Π-H-Space + + right-unit-law-mul-pointed-Π-H-Space : + (f : type-pointed-Π-H-Space) → + mul-pointed-Π-H-Space f unit-pointed-Π-H-Space ＝ f + right-unit-law-mul-pointed-Π-H-Space = + right-unit-law-mul-H-Space pointed-Π-H-Space + + is-unital-mul-pointed-Π-H-Space : is-unital mul-pointed-Π-H-Space + is-unital-mul-pointed-Π-H-Space = is-unital-mul-H-Space pointed-Π-H-Space + + coh-unit-laws-mul-pointed-Π-H-Space : + coh-unit-laws + ( mul-pointed-Π-H-Space) + ( unit-pointed-Π-H-Space) + ( left-unit-law-mul-pointed-Π-H-Space) + ( right-unit-law-mul-pointed-Π-H-Space) + coh-unit-laws-mul-pointed-Π-H-Space = + coh-unit-laws-mul-H-Space pointed-Π-H-Space + + coherent-unit-laws-mul-pointed-Π-H-Space : + coherent-unit-laws mul-pointed-Π-H-Space unit-pointed-Π-H-Space + coherent-unit-laws-mul-pointed-Π-H-Space = + coherent-unit-laws-mul-H-Space pointed-Π-H-Space + + is-coherently-unital-mul-pointed-Π-H-Space : + is-coherently-unital mul-pointed-Π-H-Space + is-coherently-unital-mul-pointed-Π-H-Space = + is-coherently-unital-mul-H-Space pointed-Π-H-Space + + coherent-unital-mul-pointed-Π-H-Space : + coherent-unital-mul-Pointed-Type pointed-type-pointed-Π-H-Space + coherent-unital-mul-pointed-Π-H-Space = + coherent-unital-mul-H-Space pointed-Π-H-Space +``` diff --git a/src/structured-types/pointed-dependent-functions.lagda.md b/src/structured-types/pointed-dependent-functions.lagda.md index b9ebc6b54f..72126019ed 100644 --- a/src/structured-types/pointed-dependent-functions.lagda.md +++ b/src/structured-types/pointed-dependent-functions.lagda.md @@ -38,6 +38,7 @@ module _ ( ev-point (point-Pointed-Type A) {fam-Pointed-Fam A B}) ( point-Pointed-Fam A B) + Π∗ : UU (l1 ⊔ l2) Π∗ = pointed-Π ``` diff --git a/src/structured-types/pointed-function-h-spaces.lagda.md b/src/structured-types/pointed-function-h-spaces.lagda.md new file mode 100644 index 0000000000..04ee52c1f5 --- /dev/null +++ b/src/structured-types/pointed-function-h-spaces.lagda.md @@ -0,0 +1,102 @@ +# Pointed function H-spaces + +```agda +module structured-types.pointed-function-h-spaces where +``` + +
Imports + +```agda +open import foundation.identity-types +open import foundation.unital-binary-operations +open import foundation.universe-levels + +open import structured-types.h-spaces +open import structured-types.pointed-dependent-function-h-spaces +open import structured-types.pointed-types +``` + +
+ +## Idea + +Given a [H-space](structured-types.h-spaces.md) `M` and a +[pointed type](structured-types.pointed-types.md) `I`, the +{{#concept "pointed function H-space" Agda=pointed-function-H-Space}} `I →∗ M` +consists of [pointed functions](structured-types.pointed-maps.md) from `I` to +the underlying pointed type of `M`. The multiplication is given pointwise, and +at the base point by the +[binary action on identifications](foundation.action-on-identifications-binary-functions.md) +of the multiplication operation of `M`. + +## Definition + +```agda +module _ + {l1 l2 : Level} (I∗ : Pointed-Type l1) (M : H-Space l2) + where + + pointed-function-H-Space : H-Space (l1 ⊔ l2) + pointed-function-H-Space = pointed-Π-H-Space I∗ (λ _ → M) + + pointed-type-pointed-function-H-Space : Pointed-Type (l1 ⊔ l2) + pointed-type-pointed-function-H-Space = + pointed-type-H-Space pointed-function-H-Space + + type-pointed-function-H-Space : UU (l1 ⊔ l2) + type-pointed-function-H-Space = + type-H-Space pointed-function-H-Space + + unit-pointed-function-H-Space : type-pointed-function-H-Space + unit-pointed-function-H-Space = + unit-H-Space pointed-function-H-Space + + mul-pointed-function-H-Space : + type-pointed-function-H-Space → + type-pointed-function-H-Space → + type-pointed-function-H-Space + mul-pointed-function-H-Space = mul-H-Space pointed-function-H-Space + + left-unit-law-mul-pointed-function-H-Space : + (f : type-pointed-function-H-Space) → + mul-pointed-function-H-Space unit-pointed-function-H-Space f ＝ f + left-unit-law-mul-pointed-function-H-Space = + left-unit-law-mul-H-Space pointed-function-H-Space + + right-unit-law-mul-pointed-function-H-Space : + (f : type-pointed-function-H-Space) → + mul-pointed-function-H-Space f unit-pointed-function-H-Space ＝ f + right-unit-law-mul-pointed-function-H-Space = + right-unit-law-mul-H-Space pointed-function-H-Space + + is-unital-mul-pointed-function-H-Space : + is-unital mul-pointed-function-H-Space + is-unital-mul-pointed-function-H-Space = + is-unital-mul-H-Space pointed-function-H-Space + + coh-unit-laws-mul-pointed-function-H-Space : + coh-unit-laws + ( mul-pointed-function-H-Space) + ( unit-pointed-function-H-Space) + ( left-unit-law-mul-pointed-function-H-Space) + ( right-unit-law-mul-pointed-function-H-Space) + coh-unit-laws-mul-pointed-function-H-Space = + coh-unit-laws-mul-H-Space pointed-function-H-Space + + coherent-unit-laws-mul-pointed-function-H-Space : + coherent-unit-laws + ( mul-pointed-function-H-Space) + ( unit-pointed-function-H-Space) + coherent-unit-laws-mul-pointed-function-H-Space = + coherent-unit-laws-mul-H-Space pointed-function-H-Space + + is-coherently-unital-mul-pointed-function-H-Space : + is-coherently-unital mul-pointed-function-H-Space + is-coherently-unital-mul-pointed-function-H-Space = + is-coherently-unital-mul-H-Space pointed-function-H-Space + + coherent-unital-mul-pointed-function-H-Space : + coherent-unital-mul-Pointed-Type pointed-type-pointed-function-H-Space + coherent-unital-mul-pointed-function-H-Space = + coherent-unital-mul-H-Space pointed-function-H-Space +``` From e3eeb1aa5c8c6d37eb273c36e9d99789d3e192ee Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 12:35:43 +0100 Subject: [PATCH 02/16] some refactoring `extensions-maps` --- src/foundation/continuations.lagda.md | 1 + src/foundation/surjective-maps.lagda.md | 2 + src/orthogonal-factorization-systems.lagda.md | 2 + .../extensions-dependent-maps.lagda.md | 352 ++++++++++++++++++ .../extensions-maps.lagda.md | 306 +-------------- .../lifting-structures-on-squares.lagda.md | 1 + .../postcomposition-extensions-maps.lagda.md | 155 ++++++++ .../types-local-at-maps.lagda.md | 1 + ...alizations-at-global-subuniverses.lagda.md | 1 + 9 files changed, 522 insertions(+), 299 deletions(-) create mode 100644 src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md create mode 100644 src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md diff --git a/src/foundation/continuations.lagda.md b/src/foundation/continuations.lagda.md index 3c7d65926e..be733f980f 100644 --- a/src/foundation/continuations.lagda.md +++ b/src/foundation/continuations.lagda.md @@ -34,6 +34,7 @@ open import foundation-core.retractions open import foundation-core.sections open import foundation-core.transport-along-identifications +open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.types-local-at-maps diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 0f9dde78f7..bb0e252233 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -52,7 +52,9 @@ open import foundation-core.torsorial-type-families open import foundation-core.truncated-maps open import foundation-core.truncation-levels +open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps +open import orthogonal-factorization-systems.postcomposition-extensions-maps ``` diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index e2a8bf7286..728cc834ab 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -16,6 +16,7 @@ open import orthogonal-factorization-systems.closed-modalities public open import orthogonal-factorization-systems.continuation-modalities public open import orthogonal-factorization-systems.double-lifts-families-of-elements public open import orthogonal-factorization-systems.double-negation-sheaves public +open import orthogonal-factorization-systems.extensions-dependent-maps public open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public open import orthogonal-factorization-systems.extensions-maps public @@ -56,6 +57,7 @@ open import orthogonal-factorization-systems.null-types public open import orthogonal-factorization-systems.open-modalities public open import orthogonal-factorization-systems.orthogonal-factorization-systems public open import orthogonal-factorization-systems.orthogonal-maps public +open import orthogonal-factorization-systems.postcomposition-extensions-maps public open import orthogonal-factorization-systems.precomposition-lifts-families-of-elements public open import orthogonal-factorization-systems.pullback-hom public open import orthogonal-factorization-systems.raise-modalities public diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md new file mode 100644 index 0000000000..7cbe061dac --- /dev/null +++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md @@ -0,0 +1,352 @@ +# Extensions of dependent maps + +```agda +module orthogonal-factorization-systems.extensions-dependent-maps where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.monomorphisms +open import foundation.postcomposition-functions +open import foundation.propositions +open import foundation.sets +open import foundation.structure-identity-principle +open import foundation.transport-along-identifications +open import foundation.truncated-types +open import foundation.truncation-levels +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +An **extension** of a map `f : (x : A) → P x` along a map `i : A → B` is a map +`g : (y : B) → Q y` such that `Q` restricts along `i` to `P` and `g` restricts +along `i` to `f`. + +```text + A + | \ + i f + | \ + ∨ ∨ + B - g -> P +``` + +## Definition + +### Extensions of dependent functions + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + where + + is-extension : + {P : B → UU l3} → + ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) + is-extension f g = f ~ (g ∘ i) + + is-extension' : + {P : B → UU l3} → + ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) + is-extension' f g = (g ∘ i) ~ f + + extension-dependent-type : + (P : B → UU l3) → + ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) + extension-dependent-type P f = Σ ((y : B) → P y) (is-extension f) + + extension-dependent-type' : + (P : B → UU l3) → + ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) + extension-dependent-type' P f = Σ ((y : B) → P y) (is-extension' f) + + total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3) + total-extension-dependent-type P = + Σ ((x : A) → P (i x)) (extension-dependent-type P) + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B} + {P : B → UU l3} {f : (x : A) → P (i x)} + where + + map-extension : extension-dependent-type i P f → (y : B) → P y + map-extension = pr1 + + is-extension-map-extension : + (E : extension-dependent-type i P f) → is-extension i f (map-extension E) + is-extension-map-extension = pr2 +``` + +## Operations + +### Vertical composition of extensions of maps + +```text + A + | \ + i f + | \ + ∨ ∨ + B - g -> P + | ∧ + j / + | h + ∨ / + C +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} + {i : A → B} {j : B → C} + {f : (x : A) → P (j (i x))} {g : (x : B) → P (j x)} {h : (x : C) → P x} + where + + is-extension-comp-vertical : + is-extension j g h → is-extension i f g → is-extension (j ∘ i) f h + is-extension-comp-vertical H G x = G x ∙ H (i x) +``` + +### Horizontal composition of extensions of maps + +```text + A + / | \ + f g h + / | \ + ∨ ∨ ∨ + B - i -> C - j -> P +``` + +#### Horizontal composition of extensions of dependent functions + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} + {f : A → B} {g : A → C} {h : (x : A) → P (g x)} + {i : B → C} {j : (z : C) → P z} + where + + is-extension-dependent-type-comp-horizontal : + (I : is-extension f g i) → + is-extension g h j → is-extension f (λ x → tr P (I x) (h x)) (j ∘ i) + is-extension-dependent-type-comp-horizontal I J x = + ap (tr P (I x)) (J x) ∙ apd j (I x) +``` + +### Left whiskering of extensions of maps + +```text + A + | \ + i f + | \ + ∨ ∨ + B - g -> C - h -> P +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} + {i : A → B} {f : A → C} {g : B → C} + where + + is-extension-left-whisker : + (h : (x : C) → P x) (F : is-extension i f g) → + (is-extension i (λ x → tr P (F x) (h (f x))) (h ∘ g)) + is-extension-left-whisker h F = apd h ∘ F +``` + +### Right whiskering of extensions of maps + +```text + X - h -> A + | \ + i f + | \ + ∨ ∨ + B - g -> P +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : B → UU l3} {X : UU l4} + {i : A → B} {f : (x : A) → P (i x)} {g : (y : B) → P y} + where + + is-extension-right-whisker : + (F : is-extension i f g) (h : X → A) → is-extension (i ∘ h) (f ∘ h) g + is-extension-right-whisker F h = F ∘ h +``` + +## Properties + +### Characterizing identifications of extensions of maps + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + {P : B → UU l3} + (f : (x : A) → P (i x)) + where + + coherence-htpy-extension : + (e e' : extension-dependent-type i P f) → + map-extension e ~ map-extension e' → UU (l1 ⊔ l3) + coherence-htpy-extension e e' K = + (is-extension-map-extension e ∙h (K ·r i)) ~ is-extension-map-extension e' + + htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3) + htpy-extension e e' = + Σ ( map-extension e ~ map-extension e') + ( coherence-htpy-extension e e') + + refl-htpy-extension : + (e : extension-dependent-type i P f) → htpy-extension e e + pr1 (refl-htpy-extension e) = refl-htpy + pr2 (refl-htpy-extension e) = right-unit-htpy + + htpy-eq-extension : + (e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension e e' + htpy-eq-extension e .e refl = refl-htpy-extension e + + is-torsorial-htpy-extension : + (e : extension-dependent-type i P f) → is-torsorial (htpy-extension e) + is-torsorial-htpy-extension e = + is-torsorial-Eq-structure + ( is-torsorial-htpy (map-extension e)) + ( map-extension e , refl-htpy) + ( is-torsorial-htpy (is-extension-map-extension e ∙h refl-htpy)) + + is-equiv-htpy-eq-extension : + (e e' : extension-dependent-type i P f) → is-equiv (htpy-eq-extension e e') + is-equiv-htpy-eq-extension e = + fundamental-theorem-id + ( is-torsorial-htpy-extension e) + ( htpy-eq-extension e) + + extensionality-extension : + (e e' : extension-dependent-type i P f) → (e ＝ e') ≃ (htpy-extension e e') + pr1 (extensionality-extension e e') = htpy-eq-extension e e' + pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e' + + eq-htpy-extension : + (e e' : extension-dependent-type i P f) + (H : map-extension e ~ map-extension e') → + coherence-htpy-extension e e' H → e ＝ e' + eq-htpy-extension e e' H K = + map-inv-equiv (extensionality-extension e e') (H , K) +``` + +### The total type of extensions is equivalent to `(y : B) → P y` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + where + + inv-compute-total-extension-dependent-type : + {P : B → UU l3} → total-extension-dependent-type i P ≃ ((y : B) → P y) + inv-compute-total-extension-dependent-type = + ( right-unit-law-Σ-is-contr (λ f → is-torsorial-htpy' (f ∘ i))) ∘e + ( equiv-left-swap-Σ) + + compute-total-extension-dependent-type : + {P : B → UU l3} → ((y : B) → P y) ≃ total-extension-dependent-type i P + compute-total-extension-dependent-type = + inv-equiv (inv-compute-total-extension-dependent-type) +``` + +### The truncation level of the type of extensions is bounded by the truncation level of the codomains + +```agda +module _ + {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (i : A → B) + where + + is-trunc-is-extension-dependent-type : + {P : B → UU l3} (f : (x : A) → P (i x)) → + ((x : A) → is-trunc (succ-𝕋 k) (P (i x))) → + (g : (x : B) → P x) → is-trunc k (is-extension i f g) + is-trunc-is-extension-dependent-type f is-trunc-P g = + is-trunc-Π k λ x → is-trunc-P x (f x) (g (i x)) + + is-trunc-extension-dependent-type : + {P : B → UU l3} (f : (x : A) → P (i x)) → + ((x : B) → is-trunc k (P x)) → is-trunc k (extension-dependent-type i P f) + is-trunc-extension-dependent-type f is-trunc-P = + is-trunc-Σ + ( is-trunc-Π k is-trunc-P) + ( is-trunc-is-extension-dependent-type f + ( is-trunc-succ-is-trunc k ∘ (is-trunc-P ∘ i))) + + is-trunc-total-extension-dependent-type : + {P : B → UU l3} → + ((x : B) → is-trunc k (P x)) → + is-trunc k (total-extension-dependent-type i P) + is-trunc-total-extension-dependent-type {P} is-trunc-P = + is-trunc-equiv' k + ( (y : B) → P y) + ( compute-total-extension-dependent-type i) + ( is-trunc-Π k is-trunc-P) + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + where + + is-contr-is-extension : + {P : B → UU l3} (f : (x : A) → P (i x)) → + ((x : A) → is-prop (P (i x))) → + (g : (x : B) → P x) → is-contr (is-extension i f g) + is-contr-is-extension f is-prop-P g = + is-contr-Π λ x → is-prop-P x (f x) (g (i x)) + + is-prop-is-extension : + {P : B → UU l3} (f : (x : A) → P (i x)) → + ((x : A) → is-set (P (i x))) → + (g : (x : B) → P x) → is-prop (is-extension i f g) + is-prop-is-extension f is-set-P g = + is-prop-Π (λ x → is-set-P x (f x) (g (i x))) +``` + +## Examples + +### Every map is an extension of itself along the identity + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {P : A → UU l2} (f : (x : A) → P x) + where + + is-extension-self : is-extension id f f + is-extension-self = refl-htpy + + extension-self : extension-dependent-type id P f + extension-self = (f , is-extension-self) +``` + +## See also + +- [`orthogonal-factorization-systems.lifts-maps`](orthogonal-factorization-systems.lifts-maps.md) + for the dual notion. diff --git a/src/orthogonal-factorization-systems/extensions-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md index ccdc296bd0..4dc8ba0b83 100644 --- a/src/orthogonal-factorization-systems/extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md @@ -33,6 +33,8 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.torsorial-type-families + +open import orthogonal-factorization-systems.extensions-dependent-maps ``` @@ -61,97 +63,16 @@ module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where - is-extension : - {P : B → UU l3} → - ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) - is-extension f g = f ~ (g ∘ i) - - extension-dependent-type : - (P : B → UU l3) → - ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) - extension-dependent-type P f = Σ ((y : B) → P y) (is-extension f) - extension : {X : UU l3} → (A → X) → UU (l1 ⊔ l2 ⊔ l3) - extension {X} = extension-dependent-type (λ _ → X) - - total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3) - total-extension-dependent-type P = - Σ ((x : A) → P (i x)) (extension-dependent-type P) + extension {X} = extension-dependent-type i (λ _ → X) total-extension : (X : UU l3) → UU (l1 ⊔ l2 ⊔ l3) - total-extension X = total-extension-dependent-type (λ _ → X) - -module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B} - {P : B → UU l3} {f : (x : A) → P (i x)} - where - - map-extension : extension-dependent-type i P f → (y : B) → P y - map-extension = pr1 - - is-extension-map-extension : - (E : extension-dependent-type i P f) → is-extension i f (map-extension E) - is-extension-map-extension = pr2 + total-extension X = total-extension-dependent-type i (λ _ → X) ``` ## Operations -### Vertical composition of extensions of maps - -```text - A - | \ - i f - | \ - ∨ ∨ - B - g -> P - | ∧ - j / - | h - ∨ / - C -``` - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} - {i : A → B} {j : B → C} - {f : (x : A) → P (j (i x))} {g : (x : B) → P (j x)} {h : (x : C) → P x} - where - - is-extension-comp-vertical : - is-extension j g h → is-extension i f g → is-extension (j ∘ i) f h - is-extension-comp-vertical H G x = G x ∙ H (i x) -``` - -### Horizontal composition of extensions of maps - -```text - A - / | \ - f g h - / | \ - ∨ ∨ ∨ - B - i -> C - j -> P -``` - -#### Horizontal composition of extensions of dependent functions - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} - {f : A → B} {g : A → C} {h : (x : A) → P (g x)} - {i : B → C} {j : (z : C) → P z} - where - - is-extension-dependent-type-comp-horizontal : - (I : is-extension f g i) → - is-extension g h j → is-extension f (λ x → tr P (I x) (h x)) (j ∘ i) - is-extension-dependent-type-comp-horizontal I J x = - ap (tr P (I x)) (J x) ∙ apd j (I x) -``` - #### Horizontal composition of extensions of ordinary maps ```agda @@ -166,219 +87,26 @@ module _ is-extension-comp-horizontal I J x = (J x) ∙ ap j (I x) ``` -### Left whiskering of extensions of maps - -```text - A - | \ - i f - | \ - ∨ ∨ - B - g -> C - h -> P -``` - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} - {i : A → B} {f : A → C} {g : B → C} - where - - is-extension-left-whisker : - (h : (x : C) → P x) (F : is-extension i f g) → - (is-extension i (λ x → tr P (F x) (h (f x))) (h ∘ g)) - is-extension-left-whisker h F = apd h ∘ F -``` - -### Right whiskering of extensions of maps - -```text - X - h -> A - | \ - i f - | \ - ∨ ∨ - B - g -> P -``` - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : B → UU l3} {X : UU l4} - {i : A → B} {f : (x : A) → P (i x)} {g : (y : B) → P y} - where - - is-extension-right-whisker : - (F : is-extension i f g) (h : X → A) → is-extension (i ∘ h) (f ∘ h) g - is-extension-right-whisker F h = F ∘ h -``` - -### Postcomposition of extensions - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - where - - postcomp-extension : - (f : A → B) (i : A → X) (g : X → Y) → - extension f i → extension f (g ∘ i) - postcomp-extension f i g = - map-Σ (is-extension f (g ∘ i)) (postcomp B g) (λ j H → g ·l H) -``` - ## Properties -### Characterizing identifications of extensions of maps +### The total type of extensions is equivalent to `B → X` ```agda module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) - {P : B → UU l3} - (f : (x : A) → P (i x)) where - coherence-htpy-extension : - (e e' : extension-dependent-type i P f) → - map-extension e ~ map-extension e' → UU (l1 ⊔ l3) - coherence-htpy-extension e e' K = - (is-extension-map-extension e ∙h (K ·r i)) ~ is-extension-map-extension e' - - htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3) - htpy-extension e e' = - Σ ( map-extension e ~ map-extension e') - ( coherence-htpy-extension e e') - - refl-htpy-extension : - (e : extension-dependent-type i P f) → htpy-extension e e - pr1 (refl-htpy-extension e) = refl-htpy - pr2 (refl-htpy-extension e) = right-unit-htpy - - htpy-eq-extension : - (e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension e e' - htpy-eq-extension e .e refl = refl-htpy-extension e - - is-torsorial-htpy-extension : - (e : extension-dependent-type i P f) → is-torsorial (htpy-extension e) - is-torsorial-htpy-extension e = - is-torsorial-Eq-structure - ( is-torsorial-htpy (map-extension e)) - ( map-extension e , refl-htpy) - ( is-torsorial-htpy (is-extension-map-extension e ∙h refl-htpy)) - - is-equiv-htpy-eq-extension : - (e e' : extension-dependent-type i P f) → is-equiv (htpy-eq-extension e e') - is-equiv-htpy-eq-extension e = - fundamental-theorem-id - ( is-torsorial-htpy-extension e) - ( htpy-eq-extension e) - - extensionality-extension : - (e e' : extension-dependent-type i P f) → (e ＝ e') ≃ (htpy-extension e e') - pr1 (extensionality-extension e e') = htpy-eq-extension e e' - pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e' - - eq-htpy-extension : - (e e' : extension-dependent-type i P f) - (H : map-extension e ~ map-extension e') → - coherence-htpy-extension e e' H → e ＝ e' - eq-htpy-extension e e' H K = - map-inv-equiv (extensionality-extension e e') (H , K) -``` - -### The total type of extensions is equivalent to `(y : B) → P y` - -```agda -module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) - where - - inv-compute-total-extension-dependent-type : - {P : B → UU l3} → total-extension-dependent-type i P ≃ ((y : B) → P y) - inv-compute-total-extension-dependent-type = - ( right-unit-law-Σ-is-contr (λ f → is-torsorial-htpy' (f ∘ i))) ∘e - ( equiv-left-swap-Σ) - - compute-total-extension-dependent-type : - {P : B → UU l3} → ((y : B) → P y) ≃ total-extension-dependent-type i P - compute-total-extension-dependent-type = - inv-equiv (inv-compute-total-extension-dependent-type) - inv-compute-total-extension : {X : UU l3} → total-extension i X ≃ (B → X) - inv-compute-total-extension = inv-compute-total-extension-dependent-type + inv-compute-total-extension = inv-compute-total-extension-dependent-type i compute-total-extension : {X : UU l3} → (B → X) ≃ total-extension i X - compute-total-extension = compute-total-extension-dependent-type -``` - -### The truncation level of the type of extensions is bounded by the truncation level of the codomains - -```agda -module _ - {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (i : A → B) - where - - is-trunc-is-extension-dependent-type : - {P : B → UU l3} (f : (x : A) → P (i x)) → - ((x : A) → is-trunc (succ-𝕋 k) (P (i x))) → - (g : (x : B) → P x) → is-trunc k (is-extension i f g) - is-trunc-is-extension-dependent-type f is-trunc-P g = - is-trunc-Π k λ x → is-trunc-P x (f x) (g (i x)) - - is-trunc-extension-dependent-type : - {P : B → UU l3} (f : (x : A) → P (i x)) → - ((x : B) → is-trunc k (P x)) → is-trunc k (extension-dependent-type i P f) - is-trunc-extension-dependent-type f is-trunc-P = - is-trunc-Σ - ( is-trunc-Π k is-trunc-P) - ( is-trunc-is-extension-dependent-type f - ( is-trunc-succ-is-trunc k ∘ (is-trunc-P ∘ i))) - - is-trunc-total-extension-dependent-type : - {P : B → UU l3} → - ((x : B) → is-trunc k (P x)) → - is-trunc k (total-extension-dependent-type i P) - is-trunc-total-extension-dependent-type {P} is-trunc-P = - is-trunc-equiv' k - ( (y : B) → P y) - ( compute-total-extension-dependent-type i) - ( is-trunc-Π k is-trunc-P) - -module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) - where - - is-contr-is-extension : - {P : B → UU l3} (f : (x : A) → P (i x)) → - ((x : A) → is-prop (P (i x))) → - (g : (x : B) → P x) → is-contr (is-extension i f g) - is-contr-is-extension f is-prop-P g = - is-contr-Π λ x → is-prop-P x (f x) (g (i x)) - - is-prop-is-extension : - {P : B → UU l3} (f : (x : A) → P (i x)) → - ((x : A) → is-set (P (i x))) → - (g : (x : B) → P x) → is-prop (is-extension i f g) - is-prop-is-extension f is-set-P g = - is-prop-Π (λ x → is-set-P x (f x) (g (i x))) + compute-total-extension = compute-total-extension-dependent-type i ``` ## Examples -### Every map is an extension of itself along the identity - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {P : A → UU l2} (f : (x : A) → P x) - where - - is-extension-self : is-extension id f f - is-extension-self = refl-htpy - - extension-self : extension-dependent-type id P f - extension-self = f , is-extension-self -``` - ### The identity is an extension of every map along themselves ```agda @@ -393,26 +121,6 @@ module _ extension-along-self = id , is-extension-along-self ``` -### Postcomposition of extensions by an embedding is an embedding - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - where - - is-emb-postcomp-extension : - (f : A → B) (i : A → X) (g : X → Y) → is-emb g → - is-emb (postcomp-extension f i g) - is-emb-postcomp-extension f i g H = - is-emb-map-Σ - ( is-extension f (g ∘ i)) - ( is-mono-is-emb g H B) - ( λ j → - is-emb-is-equiv - ( is-equiv-map-Π-is-fiberwise-equiv - ( λ x → H (i x) (j (f x))))) -``` - ## See also - [`orthogonal-factorization-systems.lifts-maps`](orthogonal-factorization-systems.lifts-maps.md) diff --git a/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md b/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md index cd33ef10d2..dc113af9c6 100644 --- a/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md +++ b/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md @@ -33,6 +33,7 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation.whiskering-identifications-concatenation +open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.lifts-maps open import orthogonal-factorization-systems.pullback-hom diff --git a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md new file mode 100644 index 0000000000..7d6d5b89ea --- /dev/null +++ b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md @@ -0,0 +1,155 @@ +# Postcomposition of extensions of maps + +```agda +module orthogonal-factorization-systems.postcomposition-extensions-maps where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.functoriality-function-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.monomorphisms +open import foundation.postcomposition-functions +open import foundation.propositions +open import foundation.sets +open import foundation.structure-identity-principle +open import foundation.transport-along-identifications +open import foundation.truncated-maps +open import foundation.truncated-types +open import foundation.truncation-levels +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.torsorial-type-families + +open import orthogonal-factorization-systems.extensions-dependent-maps +open import orthogonal-factorization-systems.extensions-maps +``` + +
+ +## Idea + +Given a map `i : A → B` and a map `f : A → X`, then we may +{{#concept "postcompose" Disambiguation="extension of map by map" Agda=postcomp-extension}} +any [extension](orthogonal-factorization-systems.extensions-maps.md) +`α : extension i f` by `g` to obtain an extension `g ∘ α : extension i (g ∘ f)`. + +## Definition + +### Postcomposition of extensions + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + where + + postcomp-extension : + (i : A → B) (f : A → X) (g : X → Y) → + extension i f → extension i (g ∘ f) + postcomp-extension i f g = + map-Σ (is-extension i (g ∘ f)) (postcomp B g) (λ j H → g ·l H) +``` + +## Properties + +### Postcomposition of extensions by an equivalence is an equivalence + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + where + + is-equiv-postcomp-extension : + (f : A → B) (i : A → X) (g : X → Y) → is-equiv g → + is-equiv (postcomp-extension f i g) + is-equiv-postcomp-extension f i g G = + is-equiv-map-Σ + ( is-extension f (g ∘ i)) + ( is-equiv-postcomp-is-equiv g G B) + ( λ j → + is-equiv-map-Π-is-fiberwise-equiv + ( λ x → is-emb-is-equiv G (i x) (j (f x)))) + + equiv-postcomp-extension : + (f : A → B) (i : A → X) (g : X ≃ Y) → + extension f i ≃ extension f (map-equiv g ∘ i) + equiv-postcomp-extension f i (g , G) = + ( postcomp-extension f i g , is-equiv-postcomp-extension f i g G) +``` + +### Postcomposition of extensions by an embedding is an embedding + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + where + + is-emb-postcomp-extension : + (f : A → B) (i : A → X) (g : X → Y) → is-emb g → + is-emb (postcomp-extension f i g) + is-emb-postcomp-extension f i g H = + is-emb-map-Σ + ( is-extension f (g ∘ i)) + ( is-mono-is-emb g H B) + ( λ j → + is-emb-is-equiv + ( is-equiv-map-Π-is-fiberwise-equiv + ( λ x → H (i x) (j (f x))))) + + emb-postcomp-extension : + (f : A → B) (i : A → X) (g : X ↪ Y) → + extension f i ↪ extension f (map-emb g ∘ i) + emb-postcomp-extension f i (g , G) = + postcomp-extension f i g , is-emb-postcomp-extension f i g G +``` + +### Postcomposition of extensions by a `k`-truncated map is `k`-truncated + +```agda +module _ + {l1 l2 l3 l4 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + where + + is-trunc-map-postcomp-extension : + (f : A → B) (i : A → X) (g : X → Y) → is-trunc-map k g → + is-trunc-map k (postcomp-extension f i g) + is-trunc-map-postcomp-extension f i g G = + is-trunc-map-map-Σ k + ( is-extension f (g ∘ i)) + ( is-trunc-map-postcomp-is-trunc-map k g G B) + ( λ j → + is-trunc-map-map-Π k + ( λ a → ap g) + ( λ a → + is-trunc-map-ap-is-trunc-map k g + ( is-trunc-map-succ-is-trunc-map k G) + ( i a) + ( j (f a)))) + + trunc-map-postcomp-extension : + (f : A → B) (i : A → X) (g : trunc-map k X Y) → + trunc-map k (extension f i) (extension f (map-trunc-map g ∘ i)) + trunc-map-postcomp-extension f i (g , G) = + ( postcomp-extension f i g , is-trunc-map-postcomp-extension f i g G) +``` + +## See also + +- In [`foundation.surjective-maps`](foundation.surjective-maps.md) it is shown + that postcomposition of extensions along surjective maps by an embedding is an + equivalence. diff --git a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md index 1ebbc9e3de..6d9f82230b 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -41,6 +41,7 @@ open import foundation.universal-property-empty-type open import foundation.universal-property-equivalences open import foundation.universe-levels +open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps ``` diff --git a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md index a3c2143af4..74825118eb 100644 --- a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md @@ -28,6 +28,7 @@ open import foundation.unit-type open import foundation.univalence open import foundation.universe-levels +open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.types-local-at-maps ``` From 30b157cc72157ad797c5f81e70d290ac2ddbb99d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 12:38:51 +0100 Subject: [PATCH 03/16] edits --- .../extensions-dependent-maps.lagda.md | 22 +++++++++---------- 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md index 7cbe061dac..caefab265e 100644 --- a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md @@ -39,9 +39,9 @@ open import foundation-core.torsorial-type-families ## Idea -An **extension** of a map `f : (x : A) → P x` along a map `i : A → B` is a map -`g : (y : B) → Q y` such that `Q` restricts along `i` to `P` and `g` restricts -along `i` to `f`. +An **extension** of a dependent map `f : (x : A) → P x` along a map `i : A → B` +is a map `g : (y : B) → Q y` such that `Q` restricts along `i` to `P` and `g` +restricts along `i` to `f`. ```text A @@ -100,7 +100,7 @@ module _ ## Operations -### Vertical composition of extensions of maps +### Vertical composition of extensions of dependent maps ```text A @@ -128,7 +128,7 @@ module _ is-extension-comp-vertical H G x = G x ∙ H (i x) ``` -### Horizontal composition of extensions of maps +### Horizontal composition of extensions of dependent maps ```text A @@ -139,8 +139,6 @@ module _ B - i -> C - j -> P ``` -#### Horizontal composition of extensions of dependent functions - ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4} @@ -155,7 +153,7 @@ module _ ap (tr P (I x)) (J x) ∙ apd j (I x) ``` -### Left whiskering of extensions of maps +### Left whiskering of extensions of dependent maps ```text A @@ -178,7 +176,7 @@ module _ is-extension-left-whisker h F = apd h ∘ F ``` -### Right whiskering of extensions of maps +### Right whiskering of extensions of dependent maps ```text X - h -> A @@ -202,7 +200,7 @@ module _ ## Properties -### Characterizing identifications of extensions of maps +### Characterizing equality of extensions of dependent maps ```agda module _ @@ -278,7 +276,7 @@ module _ inv-equiv (inv-compute-total-extension-dependent-type) ``` -### The truncation level of the type of extensions is bounded by the truncation level of the codomains +### The truncation level of the type of extensions is bounded by the truncation level of the codomain ```agda module _ @@ -332,7 +330,7 @@ module _ ## Examples -### Every map is an extension of itself along the identity +### Every dependent map is an extension of itself along the identity ```agda module _ From 562171f6e9c9f052a0eecfa5d3b2e2f83c069588 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 15:50:28 +0100 Subject: [PATCH 04/16] silly importery --- src/foundation/continuations.lagda.md | 1 - src/foundation/surjective-maps.lagda.md | 1 - .../extensions-dependent-maps.lagda.md | 129 +++++++++++++++--- .../extensions-maps.lagda.md | 24 ++-- .../lifting-structures-on-squares.lagda.md | 1 - .../postcomposition-extensions-maps.lagda.md | 1 - .../types-local-at-maps.lagda.md | 1 - ...alizations-at-global-subuniverses.lagda.md | 1 - 8 files changed, 121 insertions(+), 38 deletions(-) diff --git a/src/foundation/continuations.lagda.md b/src/foundation/continuations.lagda.md index be733f980f..3c7d65926e 100644 --- a/src/foundation/continuations.lagda.md +++ b/src/foundation/continuations.lagda.md @@ -34,7 +34,6 @@ open import foundation-core.retractions open import foundation-core.sections open import foundation-core.transport-along-identifications -open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.types-local-at-maps diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index bb0e252233..07d51e9b4e 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -52,7 +52,6 @@ open import foundation-core.torsorial-type-families open import foundation-core.truncated-maps open import foundation-core.truncation-levels -open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.postcomposition-extensions-maps ``` diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md index caefab265e..769eb5c231 100644 --- a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md @@ -39,22 +39,23 @@ open import foundation-core.torsorial-type-families ## Idea -An **extension** of a dependent map `f : (x : A) → P x` along a map `i : A → B` -is a map `g : (y : B) → Q y` such that `Q` restricts along `i` to `P` and `g` -restricts along `i` to `f`. +An +{{#concept "extension" Disambiguation="of a dependent map along a map, types" Agda=extension-dependent-type}} +of a dependent map `f : (x : A) → P (i x)` along a map `i : A → B` is a map +`g : (y : B) → P y` such that `g` restricts along `i` to `f`. ```text - A - | \ - i f - | \ - ∨ ∨ - B - g -> P + A + | \ + i | \ f + | \ + ∨ g ∨ + b ∈ B -----> P b ``` ## Definition -### Extensions of dependent functions +### Extensions of dependent maps ```agda module _ @@ -64,23 +65,13 @@ module _ is-extension : {P : B → UU l3} → ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) - is-extension f g = f ~ (g ∘ i) - - is-extension' : - {P : B → UU l3} → - ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) - is-extension' f g = (g ∘ i) ~ f + is-extension f g = (f ~ g ∘ i) extension-dependent-type : (P : B → UU l3) → ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) extension-dependent-type P f = Σ ((y : B) → P y) (is-extension f) - extension-dependent-type' : - (P : B → UU l3) → - ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) - extension-dependent-type' P f = Σ ((y : B) → P y) (is-extension' f) - total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3) total-extension-dependent-type P = Σ ((x : A) → P (i x)) (extension-dependent-type P) @@ -98,6 +89,40 @@ module _ is-extension-map-extension = pr2 ``` +### Extensions of dependent maps with homotopies going the other way + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + where + + is-extension' : + {P : B → UU l3} → + ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) + is-extension' f g = (g ∘ i ~ f) + + extension-dependent-type' : + (P : B → UU l3) → + ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) + extension-dependent-type' P f = Σ ((y : B) → P y) (is-extension' f) + + total-extension-dependent-type' : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3) + total-extension-dependent-type' P = + Σ ((x : A) → P (i x)) (extension-dependent-type' P) + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B} + {P : B → UU l3} {f : (x : A) → P (i x)} + where + + map-extension' : extension-dependent-type' i P f → (y : B) → P y + map-extension' = pr1 + + is-extension-map-extension' : + (E : extension-dependent-type' i P f) → is-extension' i f (map-extension' E) + is-extension-map-extension' = pr2 +``` + ## Operations ### Vertical composition of extensions of dependent maps @@ -257,6 +282,68 @@ module _ map-inv-equiv (extensionality-extension e e') (H , K) ``` +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + {P : B → UU l3} + (f : (x : A) → P (i x)) + where + + coherence-htpy-extension-dependent-type' : + (e e' : extension-dependent-type' i P f) → + map-extension' e ~ map-extension' e' → UU (l1 ⊔ l3) + coherence-htpy-extension-dependent-type' e e' K = + is-extension-map-extension' e ~ (K ·r i) ∙h is-extension-map-extension' e' + + htpy-extension-dependent-type' : + (e e' : extension-dependent-type' i P f) → UU (l1 ⊔ l2 ⊔ l3) + htpy-extension-dependent-type' e e' = + Σ ( map-extension' e ~ map-extension' e') + ( coherence-htpy-extension-dependent-type' e e') + + refl-htpy-extension-dependent-type' : + (e : extension-dependent-type' i P f) → htpy-extension-dependent-type' e e + pr1 (refl-htpy-extension-dependent-type' e) = refl-htpy + pr2 (refl-htpy-extension-dependent-type' e) = refl-htpy + + htpy-eq-extension-dependent-type' : + (e e' : extension-dependent-type' i P f) → + e ＝ e' → htpy-extension-dependent-type' e e' + htpy-eq-extension-dependent-type' e .e refl = + refl-htpy-extension-dependent-type' e + + is-torsorial-htpy-extension-dependent-type' : + (e : extension-dependent-type' i P f) → + is-torsorial (htpy-extension-dependent-type' e) + is-torsorial-htpy-extension-dependent-type' e = + is-torsorial-Eq-structure + ( is-torsorial-htpy (map-extension' e)) + ( map-extension' e , refl-htpy) + ( is-torsorial-htpy (is-extension-map-extension' e)) + + is-equiv-htpy-eq-extension-dependent-type' : + (e e' : extension-dependent-type' i P f) → + is-equiv (htpy-eq-extension-dependent-type' e e') + is-equiv-htpy-eq-extension-dependent-type' e = + fundamental-theorem-id + ( is-torsorial-htpy-extension-dependent-type' e) + ( htpy-eq-extension-dependent-type' e) + + extensionality-extension-dependent-type' : + (e e' : extension-dependent-type' i P f) → + (e ＝ e') ≃ (htpy-extension-dependent-type' e e') + pr1 (extensionality-extension-dependent-type' e e') = + htpy-eq-extension-dependent-type' e e' + pr2 (extensionality-extension-dependent-type' e e') = + is-equiv-htpy-eq-extension-dependent-type' e e' + + eq-htpy-extension-dependent-type' : + (e e' : extension-dependent-type' i P f) → + htpy-extension-dependent-type' e e' → e ＝ e' + eq-htpy-extension-dependent-type' e e' = + map-inv-equiv (extensionality-extension-dependent-type' e e') +``` + ### The total type of extensions is equivalent to `(y : B) → P y` ```agda diff --git a/src/orthogonal-factorization-systems/extensions-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md index 4dc8ba0b83..44411d6334 100644 --- a/src/orthogonal-factorization-systems/extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md @@ -2,6 +2,8 @@ ```agda module orthogonal-factorization-systems.extensions-maps where + +open import orthogonal-factorization-systems.extensions-dependent-maps public ```
Imports @@ -34,29 +36,29 @@ open import foundation.whiskering-homotopies-composition open import foundation-core.torsorial-type-families -open import orthogonal-factorization-systems.extensions-dependent-maps ```
## Idea -An **extension** of a map `f : (x : A) → P x` along a map `i : A → B` is a map -`g : (y : B) → Q y` such that `Q` restricts along `i` to `P` and `g` restricts -along `i` to `f`. +An +{{#concept "extension" Disambiguation="of a map along a map, types" Agda=extension}} +of a map `f : A → X` along a map `i : A → B` is a map `g : B → X` such that `g` +restricts along `i` to `f`. ```text - A - | \ - i f - | \ - ∨ ∨ - B - g -> P + A + | \ + i | \ f + | \ + ∨ g ∨ + B -----> X ``` ## Definition -### Extensions of dependent functions +### Extensions of functions ```agda module _ diff --git a/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md b/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md index dc113af9c6..cd33ef10d2 100644 --- a/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md +++ b/src/orthogonal-factorization-systems/lifting-structures-on-squares.lagda.md @@ -33,7 +33,6 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation.whiskering-identifications-concatenation -open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.lifts-maps open import orthogonal-factorization-systems.pullback-hom diff --git a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md index 7d6d5b89ea..a93aa4ab6c 100644 --- a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md @@ -36,7 +36,6 @@ open import foundation.whiskering-homotopies-composition open import foundation-core.torsorial-type-families -open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps ``` diff --git a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md index 6d9f82230b..1ebbc9e3de 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -41,7 +41,6 @@ open import foundation.universal-property-empty-type open import foundation.universal-property-equivalences open import foundation.universe-levels -open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps ``` diff --git a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md index 74825118eb..a3c2143af4 100644 --- a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md @@ -28,7 +28,6 @@ open import foundation.unit-type open import foundation.univalence open import foundation.universe-levels -open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.types-local-at-maps ``` From 8a90b8a04915d5f396bc19c8f1200f95232c05ca Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 15:56:02 +0100 Subject: [PATCH 05/16] Dependent extension H-spaces --- .../extensions-maps.lagda.md | 1 - src/structured-types.lagda.md | 1 + .../dependent-extension-h-spaces.lagda.md | 168 ++++++++++++++++++ ...inted-dependent-function-h-spaces.lagda.md | 5 + 4 files changed, 174 insertions(+), 1 deletion(-) create mode 100644 src/structured-types/dependent-extension-h-spaces.lagda.md diff --git a/src/orthogonal-factorization-systems/extensions-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md index 44411d6334..a5c3282fda 100644 --- a/src/orthogonal-factorization-systems/extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md @@ -35,7 +35,6 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.torsorial-type-families - ``` diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index cdc006f621..406dc27dec 100644 --- a/src/structured-types.lagda.md +++ b/src/structured-types.lagda.md @@ -18,6 +18,7 @@ open import structured-types.conjugation-pointed-types public open import structured-types.constant-pointed-maps public open import structured-types.contractible-pointed-types public open import structured-types.cyclic-types public +open import structured-types.dependent-extension-h-spaces public open import structured-types.dependent-products-h-spaces public open import structured-types.dependent-products-pointed-types public open import structured-types.dependent-products-wild-monoids public diff --git a/src/structured-types/dependent-extension-h-spaces.lagda.md b/src/structured-types/dependent-extension-h-spaces.lagda.md new file mode 100644 index 0000000000..8a9300b6d3 --- /dev/null +++ b/src/structured-types/dependent-extension-h-spaces.lagda.md @@ -0,0 +1,168 @@ +# Dependent extension H-spaces + +```agda +module structured-types.dependent-extension-h-spaces where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.unital-binary-operations +open import foundation.universe-levels + +open import orthogonal-factorization-systems.extensions-maps + +open import structured-types.h-spaces +open import structured-types.noncoherent-h-spaces +open import structured-types.pointed-dependent-functions +open import structured-types.pointed-homotopies +open import structured-types.pointed-types +``` + +
+ +## Idea + +Given a map `h : A → B` and a family of [H-spaces](structured-types.h-spaces.md) +`M i` indexed by `B`, the +{{#concept "dependent extension" Disambiguation="H-space" Agda=extension-Π-H-Space}} +`extension-Π h M` is an H-space consisting of +[dependent extensions](orthogonal-factorization-systems.extensions-maps.md) in +`M` along `h`. The multiplication is given pointwise, and along the restriction +of `h` by the +[binary action on identifications](foundation.action-on-identifications-binary-functions.md) +of the pointwise multiplication operation of `M`. + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (h : A → B) + (M : B → H-Space l3) + where + + type-extension-Π-H-Space : UU (l1 ⊔ l2 ⊔ l3) + type-extension-Π-H-Space = + extension-dependent-type' h (type-H-Space ∘ M) (unit-H-Space ∘ M ∘ h) + + unit-extension-Π-H-Space : type-extension-Π-H-Space + unit-extension-Π-H-Space = (unit-H-Space ∘ M , refl-htpy) + + pointed-type-extension-Π-H-Space : Pointed-Type (l1 ⊔ l2 ⊔ l3) + pointed-type-extension-Π-H-Space = + ( type-extension-Π-H-Space , unit-extension-Π-H-Space) + + mul-extension-Π-H-Space : + type-extension-Π-H-Space → type-extension-Π-H-Space → type-extension-Π-H-Space + pr1 (mul-extension-Π-H-Space (f , f∗) (g , g∗)) i = + mul-H-Space (M i) (f i) (g i) + pr2 (mul-extension-Π-H-Space (f , f∗) (g , g∗)) i = + ( ap-binary (mul-H-Space (M (h i))) (f∗ i) (g∗ i)) ∙ + ( left-unit-law-mul-H-Space (M (h i)) (unit-H-Space (M (h i)))) + + htpy-left-unit-law-mul-extension-Π-H-Space : + (f : type-extension-Π-H-Space) → + htpy-extension-dependent-type' + ( h) + ( unit-H-Space ∘ M ∘ h) + ( mul-extension-Π-H-Space unit-extension-Π-H-Space f) + ( f) + pr1 (htpy-left-unit-law-mul-extension-Π-H-Space (f , f∗)) i = + left-unit-law-mul-H-Space (M i) (f i) + pr2 (htpy-left-unit-law-mul-extension-Π-H-Space (f , f∗)) i = + inv-nat-htpy-id (left-unit-law-mul-H-Space (M (h i))) (f∗ i) + + left-unit-law-mul-extension-Π-H-Space : + (f : type-extension-Π-H-Space) → + mul-extension-Π-H-Space unit-extension-Π-H-Space f ＝ f + left-unit-law-mul-extension-Π-H-Space f = + eq-htpy-extension-dependent-type' + ( h) + ( unit-H-Space ∘ M ∘ h) + ( mul-extension-Π-H-Space unit-extension-Π-H-Space f) + ( f) + ( htpy-left-unit-law-mul-extension-Π-H-Space f) + + htpy-right-unit-law-mul-extension-Π-H-Space' : + (f : type-extension-Π-H-Space) → + htpy-extension-dependent-type' + ( h) + ( unit-H-Space ∘ M ∘ h) + ( mul-extension-Π-H-Space f unit-extension-Π-H-Space) + ( f) + pr1 (htpy-right-unit-law-mul-extension-Π-H-Space' (f , f∗)) i = + right-unit-law-mul-H-Space (M i) (f i) + pr2 (htpy-right-unit-law-mul-extension-Π-H-Space' (f , f∗)) i = + equational-reasoning + ( ( ap (λ f → mul-H-Space (M (h i)) f (unit-H-Space (M (h i)))) (f∗ i)) ∙ + ( refl)) ∙ + ( left-unit-law-mul-H-Space (M (h i)) (unit-H-Space (M (h i)))) + ＝ + ( ap (λ f → mul-H-Space (M (h i)) f (unit-H-Space (M (h i)))) (f∗ i)) ∙ + ( right-unit-law-mul-H-Space (M (h i)) (unit-H-Space (M (h i)))) + by ap-binary (_∙_) right-unit (coh-unit-laws-mul-H-Space (M (h i))) + ＝ + ( right-unit-law-mul-H-Space (M (h i)) (f (h i)) ∙ f∗ i) + by inv-nat-htpy-id (right-unit-law-mul-H-Space (M (h i))) (f∗ i) + + right-unit-law-mul-extension-Π-H-Space' : + (f : type-extension-Π-H-Space) → + mul-extension-Π-H-Space f unit-extension-Π-H-Space ＝ f + right-unit-law-mul-extension-Π-H-Space' f = + eq-htpy-extension-dependent-type' + ( h) + ( unit-H-Space ∘ M ∘ h) + ( mul-extension-Π-H-Space f unit-extension-Π-H-Space) + ( f) + ( htpy-right-unit-law-mul-extension-Π-H-Space' f) + + noncoherent-h-space-extension-Π-H-Space : Noncoherent-H-Space (l1 ⊔ l2 ⊔ l3) + noncoherent-h-space-extension-Π-H-Space = + ( pointed-type-extension-Π-H-Space , + mul-extension-Π-H-Space , + left-unit-law-mul-extension-Π-H-Space , + right-unit-law-mul-extension-Π-H-Space') + + extension-Π-H-Space : H-Space (l1 ⊔ l2 ⊔ l3) + extension-Π-H-Space = + h-space-Noncoherent-H-Space noncoherent-h-space-extension-Π-H-Space + + right-unit-law-mul-extension-Π-H-Space : + (f : type-extension-Π-H-Space) → + mul-extension-Π-H-Space f unit-extension-Π-H-Space ＝ f + right-unit-law-mul-extension-Π-H-Space = + right-unit-law-mul-H-Space extension-Π-H-Space + + is-unital-mul-extension-Π-H-Space : is-unital mul-extension-Π-H-Space + is-unital-mul-extension-Π-H-Space = is-unital-mul-H-Space extension-Π-H-Space + + coh-unit-laws-mul-extension-Π-H-Space : + coh-unit-laws + ( mul-extension-Π-H-Space) + ( unit-extension-Π-H-Space) + ( left-unit-law-mul-extension-Π-H-Space) + ( right-unit-law-mul-extension-Π-H-Space) + coh-unit-laws-mul-extension-Π-H-Space = + coh-unit-laws-mul-H-Space extension-Π-H-Space + + coherent-unit-laws-mul-extension-Π-H-Space : + coherent-unit-laws mul-extension-Π-H-Space unit-extension-Π-H-Space + coherent-unit-laws-mul-extension-Π-H-Space = + coherent-unit-laws-mul-H-Space extension-Π-H-Space + + is-coherently-unital-mul-extension-Π-H-Space : + is-coherently-unital mul-extension-Π-H-Space + is-coherently-unital-mul-extension-Π-H-Space = + is-coherently-unital-mul-H-Space extension-Π-H-Space + + coherent-unital-mul-extension-Π-H-Space : + coherent-unital-mul-Pointed-Type pointed-type-extension-Π-H-Space + coherent-unital-mul-extension-Π-H-Space = + coherent-unital-mul-H-Space extension-Π-H-Space +``` diff --git a/src/structured-types/pointed-dependent-function-h-spaces.lagda.md b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md index fe0ee49719..9030a702dd 100644 --- a/src/structured-types/pointed-dependent-function-h-spaces.lagda.md +++ b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md @@ -151,3 +151,8 @@ module _ coherent-unital-mul-pointed-Π-H-Space = coherent-unital-mul-H-Space pointed-Π-H-Space ``` + +## See also + +- Pointed dependent function H-spaces are a special case of + [dependent extension H-spaces](structured-types.dependent-extension-h-spaces.md) From 5ec567d3ee9e6ba8f5926a5b1d32b3aa3adec0c3 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 16:10:51 +0100 Subject: [PATCH 06/16] Extension H-spaces --- src/structured-types.lagda.md | 1 + .../dependent-extension-h-spaces.lagda.md | 10 +- .../extension-h-spaces.lagda.md | 102 ++++++++++++++++++ .../pointed-function-h-spaces.lagda.md | 5 + 4 files changed, 114 insertions(+), 4 deletions(-) create mode 100644 src/structured-types/extension-h-spaces.lagda.md diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index 406dc27dec..4dbc5333e7 100644 --- a/src/structured-types.lagda.md +++ b/src/structured-types.lagda.md @@ -28,6 +28,7 @@ open import structured-types.equivalences-pointed-arrows public open import structured-types.equivalences-retractive-types public open import structured-types.equivalences-types-equipped-with-automorphisms public open import structured-types.equivalences-types-equipped-with-endomorphisms public +open import structured-types.extension-h-spaces public open import structured-types.faithful-pointed-maps public open import structured-types.fibers-of-pointed-maps public open import structured-types.finite-multiplication-magmas public diff --git a/src/structured-types/dependent-extension-h-spaces.lagda.md b/src/structured-types/dependent-extension-h-spaces.lagda.md index 8a9300b6d3..17669b6176 100644 --- a/src/structured-types/dependent-extension-h-spaces.lagda.md +++ b/src/structured-types/dependent-extension-h-spaces.lagda.md @@ -31,11 +31,13 @@ open import structured-types.pointed-types Given a map `h : A → B` and a family of [H-spaces](structured-types.h-spaces.md) `M i` indexed by `B`, the -{{#concept "dependent extension" Disambiguation="H-space" Agda=extension-Π-H-Space}} +{{#concept "dependent extension H-space" Agda=extension-Π-H-Space}} `extension-Π h M` is an H-space consisting of -[dependent extensions](orthogonal-factorization-systems.extensions-maps.md) in -`M` along `h`. The multiplication is given pointwise, and along the restriction -of `h` by the +[dependent extensions](orthogonal-factorization-systems.extensions-dependent-maps.md) +of the family of units `η : (i : A) → M (h i)` in `M` along `h`. I.e., maps +`f : (i : B) → M i` [equipped](foundation.structure.md) with a +[homotopy](foundation-core.homotopies.md) `f ∘ h ~ η`. The multiplication is +given pointwise, and on the homotopy by the [binary action on identifications](foundation.action-on-identifications-binary-functions.md) of the pointwise multiplication operation of `M`. diff --git a/src/structured-types/extension-h-spaces.lagda.md b/src/structured-types/extension-h-spaces.lagda.md new file mode 100644 index 0000000000..7d4a38c912 --- /dev/null +++ b/src/structured-types/extension-h-spaces.lagda.md @@ -0,0 +1,102 @@ +# Extension H-spaces + +```agda +module structured-types.extension-h-spaces where +``` + +
Imports + +```agda +open import foundation.identity-types +open import foundation.unital-binary-operations +open import foundation.universe-levels + +open import structured-types.dependent-extension-h-spaces +open import structured-types.h-spaces +open import structured-types.pointed-types +``` + +
+ +## Idea + +Given a map `h : A → B` and an [H-space](structured-types.h-spaces.md) `M`, the +{{#concept "extension H-space" Agda=extension-H-Space}} `extension h M` is an +H-space consisting of +[extensions](orthogonal-factorization-systems.extensions-maps.md) of the +constant family of units `η : A → M` in `M` along `h`. I.e., maps `f : B → M` +[equipped](foundation.structure.md) with a +[homotopy](foundation-core.homotopies.md) `f ∘ h ~ η`. The multiplication is +given pointwise, and on the homotopy by the +[binary action on identifications](foundation.action-on-identifications-binary-functions.md) +of the multiplication operation of `M`. + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (h : A → B) (M : H-Space l3) + where + + extension-H-Space : H-Space (l1 ⊔ l2 ⊔ l3) + extension-H-Space = extension-Π-H-Space h (λ _ → M) + + pointed-type-extension-H-Space : Pointed-Type (l1 ⊔ l2 ⊔ l3) + pointed-type-extension-H-Space = + pointed-type-H-Space extension-H-Space + + type-extension-H-Space : UU (l1 ⊔ l2 ⊔ l3) + type-extension-H-Space = + type-H-Space extension-H-Space + + unit-extension-H-Space : type-extension-H-Space + unit-extension-H-Space = + unit-H-Space extension-H-Space + + mul-extension-H-Space : + type-extension-H-Space → + type-extension-H-Space → + type-extension-H-Space + mul-extension-H-Space = mul-H-Space extension-H-Space + + left-unit-law-mul-extension-H-Space : + (f : type-extension-H-Space) → + mul-extension-H-Space unit-extension-H-Space f ＝ f + left-unit-law-mul-extension-H-Space = + left-unit-law-mul-H-Space extension-H-Space + + right-unit-law-mul-extension-H-Space : + (f : type-extension-H-Space) → + mul-extension-H-Space f unit-extension-H-Space ＝ f + right-unit-law-mul-extension-H-Space = + right-unit-law-mul-H-Space extension-H-Space + + is-unital-mul-extension-H-Space : + is-unital mul-extension-H-Space + is-unital-mul-extension-H-Space = + is-unital-mul-H-Space extension-H-Space + + coh-unit-laws-mul-extension-H-Space : + coh-unit-laws + ( mul-extension-H-Space) + ( unit-extension-H-Space) + ( left-unit-law-mul-extension-H-Space) + ( right-unit-law-mul-extension-H-Space) + coh-unit-laws-mul-extension-H-Space = + coh-unit-laws-mul-H-Space extension-H-Space + + coherent-unit-laws-mul-extension-H-Space : + coherent-unit-laws mul-extension-H-Space unit-extension-H-Space + coherent-unit-laws-mul-extension-H-Space = + coherent-unit-laws-mul-H-Space extension-H-Space + + is-coherently-unital-mul-extension-H-Space : + is-coherently-unital mul-extension-H-Space + is-coherently-unital-mul-extension-H-Space = + is-coherently-unital-mul-H-Space extension-H-Space + + coherent-unital-mul-extension-H-Space : + coherent-unital-mul-Pointed-Type pointed-type-extension-H-Space + coherent-unital-mul-extension-H-Space = + coherent-unital-mul-H-Space extension-H-Space +``` diff --git a/src/structured-types/pointed-function-h-spaces.lagda.md b/src/structured-types/pointed-function-h-spaces.lagda.md index 04ee52c1f5..8116d210b2 100644 --- a/src/structured-types/pointed-function-h-spaces.lagda.md +++ b/src/structured-types/pointed-function-h-spaces.lagda.md @@ -100,3 +100,8 @@ module _ coherent-unital-mul-pointed-function-H-Space = coherent-unital-mul-H-Space pointed-function-H-Space ``` + +## See also + +- Pointed function H-spaces are a special case of + [extension H-spaces](structured-types.extension-h-spaces.md) From dffa8771eb0957a6cb83e73377f62740346669b1 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 16:12:50 +0100 Subject: [PATCH 07/16] pre-commit --- src/structured-types/dependent-extension-h-spaces.lagda.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/structured-types/dependent-extension-h-spaces.lagda.md b/src/structured-types/dependent-extension-h-spaces.lagda.md index 17669b6176..597f02d98e 100644 --- a/src/structured-types/dependent-extension-h-spaces.lagda.md +++ b/src/structured-types/dependent-extension-h-spaces.lagda.md @@ -61,7 +61,9 @@ module _ ( type-extension-Π-H-Space , unit-extension-Π-H-Space) mul-extension-Π-H-Space : - type-extension-Π-H-Space → type-extension-Π-H-Space → type-extension-Π-H-Space + type-extension-Π-H-Space → + type-extension-Π-H-Space → + type-extension-Π-H-Space pr1 (mul-extension-Π-H-Space (f , f∗) (g , g∗)) i = mul-H-Space (M i) (f i) (g i) pr2 (mul-extension-Π-H-Space (f , f∗) (g , g∗)) i = From 759ad8b841ff7236d26e05e38a56842c6f16f4d4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 8 Nov 2025 16:22:11 +0100 Subject: [PATCH 08/16] imports --- .../extensions-dependent-maps.lagda.md | 5 ----- .../extensions-maps.lagda.md | 19 ------------------- .../postcomposition-extensions-maps.lagda.md | 14 -------------- 3 files changed, 38 deletions(-) diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md index 769eb5c231..31d7f7737a 100644 --- a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md @@ -11,17 +11,12 @@ open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-pair-types -open import foundation.embeddings open import foundation.equivalences open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.homotopy-induction open import foundation.identity-types -open import foundation.monomorphisms -open import foundation.postcomposition-functions open import foundation.propositions open import foundation.sets open import foundation.structure-identity-principle diff --git a/src/orthogonal-factorization-systems/extensions-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md index a5c3282fda..65e07d6b1b 100644 --- a/src/orthogonal-factorization-systems/extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md @@ -9,32 +9,13 @@ open import orthogonal-factorization-systems.extensions-dependent-maps public
Imports ```agda -open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions -open import foundation.contractible-types open import foundation.dependent-pair-types -open import foundation.embeddings open import foundation.equivalences open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies -open import foundation.homotopy-induction open import foundation.identity-types -open import foundation.monomorphisms -open import foundation.postcomposition-functions -open import foundation.propositions -open import foundation.sets -open import foundation.structure-identity-principle -open import foundation.transport-along-identifications -open import foundation.truncated-types -open import foundation.truncation-levels -open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels -open import foundation.whiskering-homotopies-composition - -open import foundation-core.torsorial-type-families ```
diff --git a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md index a93aa4ab6c..8829061b8c 100644 --- a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md @@ -7,9 +7,7 @@ module orthogonal-factorization-systems.postcomposition-extensions-maps where
Imports ```agda -open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions -open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences @@ -17,25 +15,13 @@ open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-function-types -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopies -open import foundation.homotopy-induction -open import foundation.identity-types open import foundation.monomorphisms open import foundation.postcomposition-functions -open import foundation.propositions -open import foundation.sets -open import foundation.structure-identity-principle -open import foundation.transport-along-identifications open import foundation.truncated-maps -open import foundation.truncated-types open import foundation.truncation-levels -open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition -open import foundation-core.torsorial-type-families - open import orthogonal-factorization-systems.extensions-maps ``` From ecfd0d3095d5bb95e5be3a4bfada6fd3be87fd62 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 9 Nov 2025 19:11:52 +0100 Subject: [PATCH 09/16] edit --- src/structured-types/central-h-spaces.lagda.md | 2 +- src/structured-types/dependent-extension-h-spaces.lagda.md | 4 ++++ src/structured-types/extension-h-spaces.lagda.md | 4 ++++ .../pointed-dependent-function-h-spaces.lagda.md | 4 ++++ src/structured-types/pointed-function-h-spaces.lagda.md | 4 ++++ 5 files changed, 17 insertions(+), 1 deletion(-) diff --git a/src/structured-types/central-h-spaces.lagda.md b/src/structured-types/central-h-spaces.lagda.md index 02606c1864..f51a364c7a 100644 --- a/src/structured-types/central-h-spaces.lagda.md +++ b/src/structured-types/central-h-spaces.lagda.md @@ -26,7 +26,7 @@ pointed evaluation map `(A → A) →∗ A`. If the type `A` is [connected component](foundation.connected-components.md) of `(A ≃ A)` at the identity [equivalence](foundation-core.equivalences.md). An {{#concept "evaluative H-space" Agda=is-central-h-space}} is a pointed type such -that the map `ev_pt : (A ≃ A)_{(id)} → A` is an equivalence. +that the map `ev_pt : (A ≃ A)_(id) → A` is an equivalence. ## Definition diff --git a/src/structured-types/dependent-extension-h-spaces.lagda.md b/src/structured-types/dependent-extension-h-spaces.lagda.md index 597f02d98e..09b2cbfaeb 100644 --- a/src/structured-types/dependent-extension-h-spaces.lagda.md +++ b/src/structured-types/dependent-extension-h-spaces.lagda.md @@ -19,6 +19,7 @@ open import foundation.universe-levels open import orthogonal-factorization-systems.extensions-maps open import structured-types.h-spaces +open import structured-types.magmas open import structured-types.noncoherent-h-spaces open import structured-types.pointed-dependent-functions open import structured-types.pointed-homotopies @@ -169,4 +170,7 @@ module _ coherent-unital-mul-Pointed-Type pointed-type-extension-Π-H-Space coherent-unital-mul-extension-Π-H-Space = coherent-unital-mul-H-Space extension-Π-H-Space + + magma-extension-Π-H-Space : Magma (l1 ⊔ l2 ⊔ l3) + magma-extension-Π-H-Space = magma-H-Space extension-Π-H-Space ``` diff --git a/src/structured-types/extension-h-spaces.lagda.md b/src/structured-types/extension-h-spaces.lagda.md index 7d4a38c912..8212add74e 100644 --- a/src/structured-types/extension-h-spaces.lagda.md +++ b/src/structured-types/extension-h-spaces.lagda.md @@ -13,6 +13,7 @@ open import foundation.universe-levels open import structured-types.dependent-extension-h-spaces open import structured-types.h-spaces +open import structured-types.magmas open import structured-types.pointed-types ``` @@ -99,4 +100,7 @@ module _ coherent-unital-mul-Pointed-Type pointed-type-extension-H-Space coherent-unital-mul-extension-H-Space = coherent-unital-mul-H-Space extension-H-Space + + magma-extension-H-Space : Magma (l1 ⊔ l2 ⊔ l3) + magma-extension-H-Space = magma-H-Space extension-H-Space ``` diff --git a/src/structured-types/pointed-dependent-function-h-spaces.lagda.md b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md index 9030a702dd..11c05345aa 100644 --- a/src/structured-types/pointed-dependent-function-h-spaces.lagda.md +++ b/src/structured-types/pointed-dependent-function-h-spaces.lagda.md @@ -17,6 +17,7 @@ open import foundation.unital-binary-operations open import foundation.universe-levels open import structured-types.h-spaces +open import structured-types.magmas open import structured-types.noncoherent-h-spaces open import structured-types.pointed-dependent-functions open import structured-types.pointed-homotopies @@ -150,6 +151,9 @@ module _ coherent-unital-mul-Pointed-Type pointed-type-pointed-Π-H-Space coherent-unital-mul-pointed-Π-H-Space = coherent-unital-mul-H-Space pointed-Π-H-Space + + magma-pointed-Π-H-Space : Magma (l1 ⊔ l2) + magma-pointed-Π-H-Space = magma-H-Space pointed-Π-H-Space ``` ## See also diff --git a/src/structured-types/pointed-function-h-spaces.lagda.md b/src/structured-types/pointed-function-h-spaces.lagda.md index 8116d210b2..8e6f0b76bb 100644 --- a/src/structured-types/pointed-function-h-spaces.lagda.md +++ b/src/structured-types/pointed-function-h-spaces.lagda.md @@ -12,6 +12,7 @@ open import foundation.unital-binary-operations open import foundation.universe-levels open import structured-types.h-spaces +open import structured-types.magmas open import structured-types.pointed-dependent-function-h-spaces open import structured-types.pointed-types ``` @@ -99,6 +100,9 @@ module _ coherent-unital-mul-Pointed-Type pointed-type-pointed-function-H-Space coherent-unital-mul-pointed-function-H-Space = coherent-unital-mul-H-Space pointed-function-H-Space + + magma-pointed-function-H-Space : Magma (l1 ⊔ l2) + magma-pointed-function-H-Space = magma-H-Space pointed-function-H-Space ``` ## See also From 4b4d550feaa1a9420c55993a6eb3b569d6a1b822 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 11 Nov 2025 00:15:49 +0100 Subject: [PATCH 10/16] edit --- .../extensions-dependent-maps.lagda.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md index 31d7f7737a..9c7ee89eee 100644 --- a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md @@ -40,12 +40,12 @@ of a dependent map `f : (x : A) → P (i x)` along a map `i : A → B` is a map `g : (y : B) → P y` such that `g` restricts along `i` to `f`. ```text - A - | \ - i | \ f - | \ - ∨ g ∨ - b ∈ B -----> P b + A + | \ + i | \ f + | \ + ∨ g ∨ + B -----> P b ``` ## Definition From 1d36f4ebf539216391e09e20dfc524af7daaf75a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 11 Nov 2025 14:40:21 +0100 Subject: [PATCH 11/16] fix --- .../postcomposition-extensions-maps.lagda.md | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md index 8829061b8c..29afe972c3 100644 --- a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md @@ -94,7 +94,7 @@ module _ ( λ j → is-emb-is-equiv ( is-equiv-map-Π-is-fiberwise-equiv - ( λ x → H (i x) (j (f x))))) + (λ x → H (i x) (j (f x))))) emb-postcomp-extension : (f : A → B) (i : A → X) (g : X ↪ Y) → @@ -120,11 +120,7 @@ module _ ( λ j → is-trunc-map-map-Π k ( λ a → ap g) - ( λ a → - is-trunc-map-ap-is-trunc-map k g - ( is-trunc-map-succ-is-trunc-map k G) - ( i a) - ( j (f a)))) + ( λ a → is-trunc-map-ap-is-trunc-map k g G (i a) (j (f a)))) trunc-map-postcomp-extension : (f : A → B) (i : A → X) (g : trunc-map k X Y) → From efbb4ebb9707484b4b8ebfa70fb456d00b73c840 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 11 Nov 2025 15:58:45 +0100 Subject: [PATCH 12/16] more refactoring extensions of maps --- src/foundation/surjective-maps.lagda.md | 1 + src/orthogonal-factorization-systems.lagda.md | 1 + .../equality-extensions-maps.lagda.md | 196 ++++++++++++++++ .../extensions-dependent-maps.lagda.md | 220 +++++------------- .../extensions-maps.lagda.md | 11 +- .../dependent-extension-h-spaces.lagda.md | 11 +- 6 files changed, 266 insertions(+), 174 deletions(-) create mode 100644 src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 07d51e9b4e..9552b8f2e6 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -52,6 +52,7 @@ open import foundation-core.torsorial-type-families open import foundation-core.truncated-maps open import foundation-core.truncation-levels +open import orthogonal-factorization-systems.equality-extensions-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.postcomposition-extensions-maps ``` diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index 728cc834ab..e412d0e8ef 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -16,6 +16,7 @@ open import orthogonal-factorization-systems.closed-modalities public open import orthogonal-factorization-systems.continuation-modalities public open import orthogonal-factorization-systems.double-lifts-families-of-elements public open import orthogonal-factorization-systems.double-negation-sheaves public +open import orthogonal-factorization-systems.equality-extensions-maps public open import orthogonal-factorization-systems.extensions-dependent-maps public open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public diff --git a/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md new file mode 100644 index 0000000000..477499180d --- /dev/null +++ b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md @@ -0,0 +1,196 @@ +# Equality of extensions of maps + +```agda +module orthogonal-factorization-systems.equality-extensions-maps where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-dependent-functions +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-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.structure-identity-principle +open import foundation.transport-along-identifications +open import foundation.truncated-types +open import foundation.truncation-levels +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.torsorial-type-families + +open import orthogonal-factorization-systems.extensions-dependent-maps +``` + +
+ +## Idea + +We characterize equality of +[extensions](orthogonal-factorization-systems.extensions-maps.md) of +([dependent](orthogonal-factorization-systems.extensions-dependent-maps.md)) +maps. + +## Definition + +### Homotopies of extensions + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + {P : B → UU l3} (f : (x : A) → P (i x)) + where + + coherence-htpy-extension : + (e e' : extension-dependent-type i P f) → + map-extension-dependent-type e ~ map-extension-dependent-type e' → + UU (l1 ⊔ l3) + coherence-htpy-extension e e' K = + ( is-extension-dependent-type-map-extension-dependent-type e ∙h (K ·r i)) ~ + ( is-extension-dependent-type-map-extension-dependent-type e') + + htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3) + htpy-extension e e' = + Σ ( map-extension-dependent-type e ~ map-extension-dependent-type e') + ( coherence-htpy-extension e e') + + refl-htpy-extension : + (e : extension-dependent-type i P f) → htpy-extension e e + pr1 (refl-htpy-extension e) = refl-htpy + pr2 (refl-htpy-extension e) = right-unit-htpy +``` + +### Homotopies of extensions with homotopies going the other way + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + {P : B → UU l3} (f : (x : A) → P (i x)) + where + + coherence-htpy-extension' : + (e e' : extension-dependent-type' i P f) → + map-extension-dependent-type' e ~ map-extension-dependent-type' e' → + UU (l1 ⊔ l3) + coherence-htpy-extension' e e' K = + ( is-extension-dependent-type-map-extension-dependent-type' e) ~ + ( K ·r i ∙h is-extension-dependent-type-map-extension-dependent-type' e') + + htpy-extension' : + (e e' : extension-dependent-type' i P f) → UU (l1 ⊔ l2 ⊔ l3) + htpy-extension' e e' = + Σ ( map-extension-dependent-type' e ~ map-extension-dependent-type' e') + ( coherence-htpy-extension' e e') + + refl-htpy-extension' : + (e : extension-dependent-type' i P f) → htpy-extension' e e + pr1 (refl-htpy-extension' e) = refl-htpy + pr2 (refl-htpy-extension' e) = refl-htpy +``` + +## Properties + +### Homotopies characterize equality + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + {P : B → UU l3} (f : (x : A) → P (i x)) + where + + htpy-eq-extension : + (e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension i f e e' + htpy-eq-extension e .e refl = refl-htpy-extension i f e + + abstract + is-torsorial-htpy-extension : + (e : extension-dependent-type i P f) → is-torsorial (htpy-extension i f e) + is-torsorial-htpy-extension e = + is-torsorial-Eq-structure + ( is-torsorial-htpy (map-extension-dependent-type e)) + ( map-extension-dependent-type e , refl-htpy) + ( is-torsorial-htpy + ( is-extension-dependent-type-map-extension-dependent-type e ∙h + refl-htpy)) + + abstract + is-equiv-htpy-eq-extension : + (e e' : extension-dependent-type i P f) → + is-equiv (htpy-eq-extension e e') + is-equiv-htpy-eq-extension e = + fundamental-theorem-id + ( is-torsorial-htpy-extension e) + ( htpy-eq-extension e) + + extensionality-extension : + (e e' : extension-dependent-type i P f) → + (e ＝ e') ≃ htpy-extension i f e e' + pr1 (extensionality-extension e e') = htpy-eq-extension e e' + pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e' + + eq-htpy-extension : + (e e' : extension-dependent-type i P f) + (H : map-extension-dependent-type e ~ map-extension-dependent-type e') → + coherence-htpy-extension i f e e' H → e ＝ e' + eq-htpy-extension e e' H K = + map-inv-equiv (extensionality-extension e e') (H , K) +``` + +### Characterizing equality of extensions of dependent maps with homotopies going the other way + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) + {P : B → UU l3} (f : (x : A) → P (i x)) + where + + htpy-eq-extension' : + (e e' : extension-dependent-type' i P f) → + e ＝ e' → htpy-extension' i f e e' + htpy-eq-extension' e .e refl = + refl-htpy-extension' i f e + + abstract + is-torsorial-htpy-extension' : + (e : extension-dependent-type' i P f) → + is-torsorial (htpy-extension' i f e) + is-torsorial-htpy-extension' e = + is-torsorial-Eq-structure + ( is-torsorial-htpy (map-extension-dependent-type' e)) + ( map-extension-dependent-type' e , refl-htpy) + ( is-torsorial-htpy + ( is-extension-dependent-type-map-extension-dependent-type' e)) + + abstract + is-equiv-htpy-eq-extension' : + (e e' : extension-dependent-type' i P f) → + is-equiv (htpy-eq-extension' e e') + is-equiv-htpy-eq-extension' e = + fundamental-theorem-id + ( is-torsorial-htpy-extension' e) + ( htpy-eq-extension' e) + + extensionality-extension' : + (e e' : extension-dependent-type' i P f) → + (e ＝ e') ≃ (htpy-extension' i f e e') + pr1 (extensionality-extension' e e') = + htpy-eq-extension' e e' + pr2 (extensionality-extension' e e') = + is-equiv-htpy-eq-extension' e e' + + eq-htpy-extension' : + (e e' : extension-dependent-type' i P f) → + htpy-extension' i f e e' → e ＝ e' + eq-htpy-extension' e e' = + map-inv-equiv (extensionality-extension' e e') +``` diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md index 9c7ee89eee..77b9cd8117 100644 --- a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md @@ -40,12 +40,12 @@ of a dependent map `f : (x : A) → P (i x)` along a map `i : A → B` is a map `g : (y : B) → P y` such that `g` restricts along `i` to `f`. ```text - A - | \ - i | \ f - | \ - ∨ g ∨ - B -----> P b + A + | \ + i | \ f + | \ + ∨ g ∨ + b ∈ B -----> P b ``` ## Definition @@ -57,15 +57,16 @@ module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where - is-extension : + is-extension-dependent-type : {P : B → UU l3} → ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) - is-extension f g = (f ~ g ∘ i) + is-extension-dependent-type f g = (f ~ g ∘ i) extension-dependent-type : (P : B → UU l3) → ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) - extension-dependent-type P f = Σ ((y : B) → P y) (is-extension f) + extension-dependent-type P f = + Σ ((y : B) → P y) (is-extension-dependent-type f) total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3) total-extension-dependent-type P = @@ -76,12 +77,13 @@ module _ {P : B → UU l3} {f : (x : A) → P (i x)} where - map-extension : extension-dependent-type i P f → (y : B) → P y - map-extension = pr1 + map-extension-dependent-type : extension-dependent-type i P f → (y : B) → P y + map-extension-dependent-type = pr1 - is-extension-map-extension : - (E : extension-dependent-type i P f) → is-extension i f (map-extension E) - is-extension-map-extension = pr2 + is-extension-dependent-type-map-extension-dependent-type : + (E : extension-dependent-type i P f) → + is-extension-dependent-type i f (map-extension-dependent-type E) + is-extension-dependent-type-map-extension-dependent-type = pr2 ``` ### Extensions of dependent maps with homotopies going the other way @@ -91,15 +93,16 @@ module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where - is-extension' : + is-extension-dependent-type' : {P : B → UU l3} → ((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3) - is-extension' f g = (g ∘ i ~ f) + is-extension-dependent-type' f g = (g ∘ i ~ f) extension-dependent-type' : (P : B → UU l3) → ((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3) - extension-dependent-type' P f = Σ ((y : B) → P y) (is-extension' f) + extension-dependent-type' P f = + Σ ((y : B) → P y) (is-extension-dependent-type' f) total-extension-dependent-type' : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3) total-extension-dependent-type' P = @@ -110,12 +113,14 @@ module _ {P : B → UU l3} {f : (x : A) → P (i x)} where - map-extension' : extension-dependent-type' i P f → (y : B) → P y - map-extension' = pr1 + map-extension-dependent-type' : + extension-dependent-type' i P f → (y : B) → P y + map-extension-dependent-type' = pr1 - is-extension-map-extension' : - (E : extension-dependent-type' i P f) → is-extension' i f (map-extension' E) - is-extension-map-extension' = pr2 + is-extension-dependent-type-map-extension-dependent-type' : + (E : extension-dependent-type' i P f) → + is-extension-dependent-type' i f (map-extension-dependent-type' E) + is-extension-dependent-type-map-extension-dependent-type' = pr2 ``` ## Operations @@ -143,9 +148,11 @@ module _ {f : (x : A) → P (j (i x))} {g : (x : B) → P (j x)} {h : (x : C) → P x} where - is-extension-comp-vertical : - is-extension j g h → is-extension i f g → is-extension (j ∘ i) f h - is-extension-comp-vertical H G x = G x ∙ H (i x) + is-extension-dependent-type-comp-vertical : + is-extension-dependent-type j g h → + is-extension-dependent-type i f g → + is-extension-dependent-type (j ∘ i) f h + is-extension-dependent-type-comp-vertical H G x = G x ∙ H (i x) ``` ### Horizontal composition of extensions of dependent maps @@ -167,8 +174,9 @@ module _ where is-extension-dependent-type-comp-horizontal : - (I : is-extension f g i) → - is-extension g h j → is-extension f (λ x → tr P (I x) (h x)) (j ∘ i) + (I : is-extension-dependent-type f g i) → + is-extension-dependent-type g h j → + is-extension-dependent-type f (λ x → tr P (I x) (h x)) (j ∘ i) is-extension-dependent-type-comp-horizontal I J x = ap (tr P (I x)) (J x) ∙ apd j (I x) ``` @@ -190,10 +198,10 @@ module _ {i : A → B} {f : A → C} {g : B → C} where - is-extension-left-whisker : - (h : (x : C) → P x) (F : is-extension i f g) → - (is-extension i (λ x → tr P (F x) (h (f x))) (h ∘ g)) - is-extension-left-whisker h F = apd h ∘ F + is-extension-dependent-type-left-whisker : + (h : (x : C) → P x) (F : is-extension-dependent-type i f g) → + is-extension-dependent-type i (λ x → tr P (F x) (h (f x))) (h ∘ g) + is-extension-dependent-type-left-whisker h F = apd h ∘ F ``` ### Right whiskering of extensions of dependent maps @@ -213,132 +221,14 @@ module _ {i : A → B} {f : (x : A) → P (i x)} {g : (y : B) → P y} where - is-extension-right-whisker : - (F : is-extension i f g) (h : X → A) → is-extension (i ∘ h) (f ∘ h) g - is-extension-right-whisker F h = F ∘ h + is-extension-dependent-type-right-whisker : + (F : is-extension-dependent-type i f g) (h : X → A) → + is-extension-dependent-type (i ∘ h) (f ∘ h) g + is-extension-dependent-type-right-whisker F h = F ∘ h ``` ## Properties -### Characterizing equality of extensions of dependent maps - -```agda -module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) - {P : B → UU l3} - (f : (x : A) → P (i x)) - where - - coherence-htpy-extension : - (e e' : extension-dependent-type i P f) → - map-extension e ~ map-extension e' → UU (l1 ⊔ l3) - coherence-htpy-extension e e' K = - (is-extension-map-extension e ∙h (K ·r i)) ~ is-extension-map-extension e' - - htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3) - htpy-extension e e' = - Σ ( map-extension e ~ map-extension e') - ( coherence-htpy-extension e e') - - refl-htpy-extension : - (e : extension-dependent-type i P f) → htpy-extension e e - pr1 (refl-htpy-extension e) = refl-htpy - pr2 (refl-htpy-extension e) = right-unit-htpy - - htpy-eq-extension : - (e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension e e' - htpy-eq-extension e .e refl = refl-htpy-extension e - - is-torsorial-htpy-extension : - (e : extension-dependent-type i P f) → is-torsorial (htpy-extension e) - is-torsorial-htpy-extension e = - is-torsorial-Eq-structure - ( is-torsorial-htpy (map-extension e)) - ( map-extension e , refl-htpy) - ( is-torsorial-htpy (is-extension-map-extension e ∙h refl-htpy)) - - is-equiv-htpy-eq-extension : - (e e' : extension-dependent-type i P f) → is-equiv (htpy-eq-extension e e') - is-equiv-htpy-eq-extension e = - fundamental-theorem-id - ( is-torsorial-htpy-extension e) - ( htpy-eq-extension e) - - extensionality-extension : - (e e' : extension-dependent-type i P f) → (e ＝ e') ≃ (htpy-extension e e') - pr1 (extensionality-extension e e') = htpy-eq-extension e e' - pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e' - - eq-htpy-extension : - (e e' : extension-dependent-type i P f) - (H : map-extension e ~ map-extension e') → - coherence-htpy-extension e e' H → e ＝ e' - eq-htpy-extension e e' H K = - map-inv-equiv (extensionality-extension e e') (H , K) -``` - -```agda -module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) - {P : B → UU l3} - (f : (x : A) → P (i x)) - where - - coherence-htpy-extension-dependent-type' : - (e e' : extension-dependent-type' i P f) → - map-extension' e ~ map-extension' e' → UU (l1 ⊔ l3) - coherence-htpy-extension-dependent-type' e e' K = - is-extension-map-extension' e ~ (K ·r i) ∙h is-extension-map-extension' e' - - htpy-extension-dependent-type' : - (e e' : extension-dependent-type' i P f) → UU (l1 ⊔ l2 ⊔ l3) - htpy-extension-dependent-type' e e' = - Σ ( map-extension' e ~ map-extension' e') - ( coherence-htpy-extension-dependent-type' e e') - - refl-htpy-extension-dependent-type' : - (e : extension-dependent-type' i P f) → htpy-extension-dependent-type' e e - pr1 (refl-htpy-extension-dependent-type' e) = refl-htpy - pr2 (refl-htpy-extension-dependent-type' e) = refl-htpy - - htpy-eq-extension-dependent-type' : - (e e' : extension-dependent-type' i P f) → - e ＝ e' → htpy-extension-dependent-type' e e' - htpy-eq-extension-dependent-type' e .e refl = - refl-htpy-extension-dependent-type' e - - is-torsorial-htpy-extension-dependent-type' : - (e : extension-dependent-type' i P f) → - is-torsorial (htpy-extension-dependent-type' e) - is-torsorial-htpy-extension-dependent-type' e = - is-torsorial-Eq-structure - ( is-torsorial-htpy (map-extension' e)) - ( map-extension' e , refl-htpy) - ( is-torsorial-htpy (is-extension-map-extension' e)) - - is-equiv-htpy-eq-extension-dependent-type' : - (e e' : extension-dependent-type' i P f) → - is-equiv (htpy-eq-extension-dependent-type' e e') - is-equiv-htpy-eq-extension-dependent-type' e = - fundamental-theorem-id - ( is-torsorial-htpy-extension-dependent-type' e) - ( htpy-eq-extension-dependent-type' e) - - extensionality-extension-dependent-type' : - (e e' : extension-dependent-type' i P f) → - (e ＝ e') ≃ (htpy-extension-dependent-type' e e') - pr1 (extensionality-extension-dependent-type' e e') = - htpy-eq-extension-dependent-type' e e' - pr2 (extensionality-extension-dependent-type' e e') = - is-equiv-htpy-eq-extension-dependent-type' e e' - - eq-htpy-extension-dependent-type' : - (e e' : extension-dependent-type' i P f) → - htpy-extension-dependent-type' e e' → e ＝ e' - eq-htpy-extension-dependent-type' e e' = - map-inv-equiv (extensionality-extension-dependent-type' e e') -``` - ### The total type of extensions is equivalent to `(y : B) → P y` ```agda @@ -368,9 +258,9 @@ module _ is-trunc-is-extension-dependent-type : {P : B → UU l3} (f : (x : A) → P (i x)) → ((x : A) → is-trunc (succ-𝕋 k) (P (i x))) → - (g : (x : B) → P x) → is-trunc k (is-extension i f g) + (g : (x : B) → P x) → is-trunc k (is-extension-dependent-type i f g) is-trunc-is-extension-dependent-type f is-trunc-P g = - is-trunc-Π k λ x → is-trunc-P x (f x) (g (i x)) + is-trunc-Π k (λ x → is-trunc-P x (f x) (g (i x))) is-trunc-extension-dependent-type : {P : B → UU l3} (f : (x : A) → P (i x)) → @@ -395,18 +285,18 @@ module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where - is-contr-is-extension : + is-contr-is-extension-dependent-type : {P : B → UU l3} (f : (x : A) → P (i x)) → ((x : A) → is-prop (P (i x))) → - (g : (x : B) → P x) → is-contr (is-extension i f g) - is-contr-is-extension f is-prop-P g = - is-contr-Π λ x → is-prop-P x (f x) (g (i x)) + (g : (x : B) → P x) → is-contr (is-extension-dependent-type i f g) + is-contr-is-extension-dependent-type f is-prop-P g = + is-contr-Π (λ x → is-prop-P x (f x) (g (i x))) - is-prop-is-extension : + is-prop-is-extension-dependent-type : {P : B → UU l3} (f : (x : A) → P (i x)) → ((x : A) → is-set (P (i x))) → - (g : (x : B) → P x) → is-prop (is-extension i f g) - is-prop-is-extension f is-set-P g = + (g : (x : B) → P x) → is-prop (is-extension-dependent-type i f g) + is-prop-is-extension-dependent-type f is-set-P g = is-prop-Π (λ x → is-set-P x (f x) (g (i x))) ``` @@ -419,11 +309,11 @@ module _ {l1 l2 : Level} {A : UU l1} {P : A → UU l2} (f : (x : A) → P x) where - is-extension-self : is-extension id f f - is-extension-self = refl-htpy + is-extension-dependent-type-self : is-extension-dependent-type id f f + is-extension-dependent-type-self = refl-htpy extension-self : extension-dependent-type id P f - extension-self = (f , is-extension-self) + extension-self = (f , is-extension-dependent-type-self) ``` ## See also diff --git a/src/orthogonal-factorization-systems/extensions-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md index 65e07d6b1b..d64ca343fe 100644 --- a/src/orthogonal-factorization-systems/extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md @@ -2,8 +2,6 @@ ```agda module orthogonal-factorization-systems.extensions-maps where - -open import orthogonal-factorization-systems.extensions-dependent-maps public ```
Imports @@ -16,6 +14,8 @@ open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels + +open import orthogonal-factorization-systems.extensions-dependent-maps ```
@@ -45,6 +45,9 @@ module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B) where + is-extension : {X : UU l3} → (A → X) → (B → X) → UU (l1 ⊔ l3) + is-extension = is-extension-dependent-type i + extension : {X : UU l3} → (A → X) → UU (l1 ⊔ l2 ⊔ l3) extension {X} = extension-dependent-type i (λ _ → X) @@ -66,7 +69,7 @@ module _ is-extension-comp-horizontal : (I : is-extension f g i) → is-extension g h j → is-extension f h (j ∘ i) - is-extension-comp-horizontal I J x = (J x) ∙ ap j (I x) + is-extension-comp-horizontal I J x = J x ∙ ap j (I x) ``` ## Properties @@ -100,7 +103,7 @@ module _ is-extension-along-self = refl-htpy extension-along-self : extension f f - extension-along-self = id , is-extension-along-self + extension-along-self = (id , is-extension-along-self) ``` ## See also diff --git a/src/structured-types/dependent-extension-h-spaces.lagda.md b/src/structured-types/dependent-extension-h-spaces.lagda.md index 09b2cbfaeb..645f3c64b6 100644 --- a/src/structured-types/dependent-extension-h-spaces.lagda.md +++ b/src/structured-types/dependent-extension-h-spaces.lagda.md @@ -16,7 +16,8 @@ open import foundation.identity-types open import foundation.unital-binary-operations open import foundation.universe-levels -open import orthogonal-factorization-systems.extensions-maps +open import orthogonal-factorization-systems.equality-extensions-maps +open import orthogonal-factorization-systems.extensions-dependent-maps open import structured-types.h-spaces open import structured-types.magmas @@ -73,7 +74,7 @@ module _ htpy-left-unit-law-mul-extension-Π-H-Space : (f : type-extension-Π-H-Space) → - htpy-extension-dependent-type' + htpy-extension' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space unit-extension-Π-H-Space f) @@ -87,7 +88,7 @@ module _ (f : type-extension-Π-H-Space) → mul-extension-Π-H-Space unit-extension-Π-H-Space f ＝ f left-unit-law-mul-extension-Π-H-Space f = - eq-htpy-extension-dependent-type' + eq-htpy-extension' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space unit-extension-Π-H-Space f) @@ -96,7 +97,7 @@ module _ htpy-right-unit-law-mul-extension-Π-H-Space' : (f : type-extension-Π-H-Space) → - htpy-extension-dependent-type' + htpy-extension' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space f unit-extension-Π-H-Space) @@ -120,7 +121,7 @@ module _ (f : type-extension-Π-H-Space) → mul-extension-Π-H-Space f unit-extension-Π-H-Space ＝ f right-unit-law-mul-extension-Π-H-Space' f = - eq-htpy-extension-dependent-type' + eq-htpy-extension' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space f unit-extension-Π-H-Space) From d7875582bc65d11d29b6f0c24191021c41353672 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 11 Nov 2025 16:04:58 +0100 Subject: [PATCH 13/16] fix --- .../types-local-at-maps.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md index 1ebbc9e3de..6d9f82230b 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -41,6 +41,7 @@ open import foundation.universal-property-empty-type open import foundation.universal-property-equivalences open import foundation.universe-levels +open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps ``` From 356e51428d65e941cd357d7f6b5b2cae08b91494 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 11 Nov 2025 18:24:06 +0100 Subject: [PATCH 14/16] fix --- .../equality-extensions-maps.lagda.md | 12 ++++++------ .../extensions-dependent-maps.lagda.md | 8 ++++---- .../extensions-maps.lagda.md | 12 ++++++++++++ ...rty-localizations-at-global-subuniverses.lagda.md | 1 + 4 files changed, 23 insertions(+), 10 deletions(-) diff --git a/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md index 477499180d..1f19bccc7c 100644 --- a/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md @@ -56,8 +56,8 @@ module _ map-extension-dependent-type e ~ map-extension-dependent-type e' → UU (l1 ⊔ l3) coherence-htpy-extension e e' K = - ( is-extension-dependent-type-map-extension-dependent-type e ∙h (K ·r i)) ~ - ( is-extension-dependent-type-map-extension-dependent-type e') + ( is-extension-map-extension-dependent-type e ∙h (K ·r i)) ~ + ( is-extension-map-extension-dependent-type e') htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3) htpy-extension e e' = @@ -83,8 +83,8 @@ module _ map-extension-dependent-type' e ~ map-extension-dependent-type' e' → UU (l1 ⊔ l3) coherence-htpy-extension' e e' K = - ( is-extension-dependent-type-map-extension-dependent-type' e) ~ - ( K ·r i ∙h is-extension-dependent-type-map-extension-dependent-type' e') + ( is-extension-map-extension-dependent-type' e) ~ + ( K ·r i ∙h is-extension-map-extension-dependent-type' e') htpy-extension' : (e e' : extension-dependent-type' i P f) → UU (l1 ⊔ l2 ⊔ l3) @@ -120,7 +120,7 @@ module _ ( is-torsorial-htpy (map-extension-dependent-type e)) ( map-extension-dependent-type e , refl-htpy) ( is-torsorial-htpy - ( is-extension-dependent-type-map-extension-dependent-type e ∙h + ( is-extension-map-extension-dependent-type e ∙h refl-htpy)) abstract @@ -169,7 +169,7 @@ module _ ( is-torsorial-htpy (map-extension-dependent-type' e)) ( map-extension-dependent-type' e , refl-htpy) ( is-torsorial-htpy - ( is-extension-dependent-type-map-extension-dependent-type' e)) + ( is-extension-map-extension-dependent-type' e)) abstract is-equiv-htpy-eq-extension' : diff --git a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md index 77b9cd8117..94c40d57b7 100644 --- a/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-dependent-maps.lagda.md @@ -80,10 +80,10 @@ module _ map-extension-dependent-type : extension-dependent-type i P f → (y : B) → P y map-extension-dependent-type = pr1 - is-extension-dependent-type-map-extension-dependent-type : + is-extension-map-extension-dependent-type : (E : extension-dependent-type i P f) → is-extension-dependent-type i f (map-extension-dependent-type E) - is-extension-dependent-type-map-extension-dependent-type = pr2 + is-extension-map-extension-dependent-type = pr2 ``` ### Extensions of dependent maps with homotopies going the other way @@ -117,10 +117,10 @@ module _ extension-dependent-type' i P f → (y : B) → P y map-extension-dependent-type' = pr1 - is-extension-dependent-type-map-extension-dependent-type' : + is-extension-map-extension-dependent-type' : (E : extension-dependent-type' i P f) → is-extension-dependent-type' i f (map-extension-dependent-type' E) - is-extension-dependent-type-map-extension-dependent-type' = pr2 + is-extension-map-extension-dependent-type' = pr2 ``` ## Operations diff --git a/src/orthogonal-factorization-systems/extensions-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-maps.lagda.md index d64ca343fe..339ce6adac 100644 --- a/src/orthogonal-factorization-systems/extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-maps.lagda.md @@ -54,6 +54,18 @@ module _ total-extension : (X : UU l3) → UU (l1 ⊔ l2 ⊔ l3) total-extension X = total-extension-dependent-type i (λ _ → X) + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B} + {X : UU l3} {f : A → X} + where + + map-extension : extension i f → B → X + map-extension = pr1 + + is-extension-map-extension : + (E : extension i f) → is-extension i f (map-extension E) + is-extension-map-extension = pr2 ``` ## Operations diff --git a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md index a3c2143af4..74825118eb 100644 --- a/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/universal-property-localizations-at-global-subuniverses.lagda.md @@ -28,6 +28,7 @@ open import foundation.unit-type open import foundation.univalence open import foundation.universe-levels +open import orthogonal-factorization-systems.extensions-dependent-maps open import orthogonal-factorization-systems.extensions-maps open import orthogonal-factorization-systems.types-local-at-maps ``` From 49c198c76e9307373253c5e82f5b82fb55f38a8a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 11 Nov 2025 18:33:32 +0100 Subject: [PATCH 15/16] edit --- src/foundation/surjective-maps.lagda.md | 4 ++-- .../equality-extensions-maps.lagda.md | 9 ++++----- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 9552b8f2e6..af5aa60f28 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -833,8 +833,8 @@ module _ ( g ∘ i) ( postcomp-extension f i g (j , N)) ( h , L) - ( M) - ( λ a → + ( M , + λ a → ( ap ( concat' (g (i a)) (M (f a))) ( is-section-map-inv-is-equiv diff --git a/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md index 1f19bccc7c..4faeac4c23 100644 --- a/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/equality-extensions-maps.lagda.md @@ -139,11 +139,10 @@ module _ pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e' eq-htpy-extension : - (e e' : extension-dependent-type i P f) - (H : map-extension-dependent-type e ~ map-extension-dependent-type e') → - coherence-htpy-extension i f e e' H → e ＝ e' - eq-htpy-extension e e' H K = - map-inv-equiv (extensionality-extension e e') (H , K) + (e e' : extension-dependent-type i P f) → + htpy-extension i f e e' → e ＝ e' + eq-htpy-extension e e' = + map-inv-equiv (extensionality-extension e e') ``` ### Characterizing equality of extensions of dependent maps with homotopies going the other way From ddf5699c7946c82d2934e4e8c83224d444bdf927 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 12 Nov 2025 22:01:33 +0100 Subject: [PATCH 16/16] fix merge --- .../dependent-extension-h-spaces.lagda.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/structured-types/dependent-extension-h-spaces.lagda.md b/src/structured-types/dependent-extension-h-spaces.lagda.md index 645f3c64b6..5bb0f3b4ac 100644 --- a/src/structured-types/dependent-extension-h-spaces.lagda.md +++ b/src/structured-types/dependent-extension-h-spaces.lagda.md @@ -16,7 +16,7 @@ open import foundation.identity-types open import foundation.unital-binary-operations open import foundation.universe-levels -open import orthogonal-factorization-systems.equality-extensions-maps +open import orthogonal-factorization-systems.equality-extensions-dependent-maps open import orthogonal-factorization-systems.extensions-dependent-maps open import structured-types.h-spaces @@ -53,7 +53,7 @@ module _ type-extension-Π-H-Space : UU (l1 ⊔ l2 ⊔ l3) type-extension-Π-H-Space = - extension-dependent-type' h (type-H-Space ∘ M) (unit-H-Space ∘ M ∘ h) + extension-dependent-map' h (type-H-Space ∘ M) (unit-H-Space ∘ M ∘ h) unit-extension-Π-H-Space : type-extension-Π-H-Space unit-extension-Π-H-Space = (unit-H-Space ∘ M , refl-htpy) @@ -74,7 +74,7 @@ module _ htpy-left-unit-law-mul-extension-Π-H-Space : (f : type-extension-Π-H-Space) → - htpy-extension' + htpy-extension-dependent-map' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space unit-extension-Π-H-Space f) @@ -88,7 +88,7 @@ module _ (f : type-extension-Π-H-Space) → mul-extension-Π-H-Space unit-extension-Π-H-Space f ＝ f left-unit-law-mul-extension-Π-H-Space f = - eq-htpy-extension' + eq-htpy-extension-dependent-map' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space unit-extension-Π-H-Space f) @@ -97,7 +97,7 @@ module _ htpy-right-unit-law-mul-extension-Π-H-Space' : (f : type-extension-Π-H-Space) → - htpy-extension' + htpy-extension-dependent-map' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space f unit-extension-Π-H-Space) @@ -121,7 +121,7 @@ module _ (f : type-extension-Π-H-Space) → mul-extension-Π-H-Space f unit-extension-Π-H-Space ＝ f right-unit-law-mul-extension-Π-H-Space' f = - eq-htpy-extension' + eq-htpy-extension-dependent-map' ( h) ( unit-H-Space ∘ M ∘ h) ( mul-extension-Π-H-Space f unit-extension-Π-H-Space)