From fa1673b3416e5b7e8ffe774063df28c9036bae79 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:30:43 +0200 Subject: [PATCH 01/19] rename "local maps" to "maps local at maps" --- src/orthogonal-factorization-systems.lagda.md | 2 +- .../local-families-of-types.lagda.md | 2 +- .../local-types.lagda.md | 2 +- ...ocal-maps.lagda.md => maps-local-at-maps.lagda.md} | 11 +++-------- .../null-maps.lagda.md | 2 +- .../null-types.lagda.md | 2 +- 6 files changed, 8 insertions(+), 13 deletions(-) rename src/orthogonal-factorization-systems/{local-maps.lagda.md => maps-local-at-maps.lagda.md} (92%) diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index 59412d4838..43406110dc 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -34,11 +34,11 @@ open import orthogonal-factorization-systems.lifting-structures-on-squares publi open import orthogonal-factorization-systems.lifts-families-of-elements public open import orthogonal-factorization-systems.lifts-of-maps public open import orthogonal-factorization-systems.local-families-of-types public -open import orthogonal-factorization-systems.local-maps public open import orthogonal-factorization-systems.local-types public open import orthogonal-factorization-systems.localizations-maps public open import orthogonal-factorization-systems.localizations-subuniverses public open import orthogonal-factorization-systems.locally-small-modal-operators public +open import orthogonal-factorization-systems.maps-local-at-maps public open import orthogonal-factorization-systems.mere-lifting-properties public open import orthogonal-factorization-systems.modal-induction public open import orthogonal-factorization-systems.modal-operators public diff --git a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md b/src/orthogonal-factorization-systems/local-families-of-types.lagda.md index eb8d398b33..65190f6342 100644 --- a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md +++ b/src/orthogonal-factorization-systems/local-families-of-types.lagda.md @@ -54,6 +54,6 @@ This remains to be formalized. ## See also -- [Local maps](orthogonal-factorization-systems.local-maps.md) +- [Local maps](orthogonal-factorization-systems.maps-local-at-maps.md) - [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md) - [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/local-types.lagda.md index 0f957651be..80c70292c3 100644 --- a/src/orthogonal-factorization-systems/local-types.lagda.md +++ b/src/orthogonal-factorization-systems/local-types.lagda.md @@ -358,6 +358,6 @@ is-contr-is-local A is-local-A = ## See also -- [Local maps](orthogonal-factorization-systems.local-maps.md) +- [Local maps](orthogonal-factorization-systems.maps-local-at-maps.md) - [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md) - [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/local-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md similarity index 92% rename from src/orthogonal-factorization-systems/local-maps.lagda.md rename to src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md index f19c0c87ee..d6a21041ac 100644 --- a/src/orthogonal-factorization-systems/local-maps.lagda.md +++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md @@ -1,7 +1,7 @@ -# Local maps +# Maps local at maps ```agda -module orthogonal-factorization-systems.local-maps where +module orthogonal-factorization-systems.maps-local-at-maps where ```
Imports @@ -46,9 +46,6 @@ A map `g : X → Y` is said to be all its [fibers](foundation-core.fibers-of-maps.md) are [`f`-local types](orthogonal-factorization-systems.local-types.md). -Equivalently, the map `g` is `f`-local if and only if `f` is -[orthogonal](orthogonal-factorization-systems.orthogonal-maps.md) to `g`. - ## Definition ```agda @@ -86,7 +83,7 @@ module _ is-local-equiv f (equiv-fiber-terminal-map u) H ``` -### A map is `f`-local if and only if it is `f`-orthogonal +### A map is `f`-local if it is `f`-orthogonal ```agda module _ @@ -112,8 +109,6 @@ module _ ( G)) ``` -The converse remains to be formalized. - ## See also - [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md) diff --git a/src/orthogonal-factorization-systems/null-maps.lagda.md b/src/orthogonal-factorization-systems/null-maps.lagda.md index 2863c0ff12..377685ddd0 100644 --- a/src/orthogonal-factorization-systems/null-maps.lagda.md +++ b/src/orthogonal-factorization-systems/null-maps.lagda.md @@ -30,8 +30,8 @@ open import foundation.unit-type open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universe-levels -open import orthogonal-factorization-systems.local-maps open import orthogonal-factorization-systems.local-types +open import orthogonal-factorization-systems.maps-local-at-maps open import orthogonal-factorization-systems.null-families-of-types open import orthogonal-factorization-systems.null-types open import orthogonal-factorization-systems.orthogonal-maps diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md index 6e50e36ba6..ec6db3ea44 100644 --- a/src/orthogonal-factorization-systems/null-types.lagda.md +++ b/src/orthogonal-factorization-systems/null-types.lagda.md @@ -29,8 +29,8 @@ open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universal-property-unit-type open import foundation.universe-levels -open import orthogonal-factorization-systems.local-maps open import orthogonal-factorization-systems.local-types +open import orthogonal-factorization-systems.maps-local-at-maps open import orthogonal-factorization-systems.orthogonal-maps ``` From 69c3cb1c577bc6cf0908e6bc3fa9ac0a1946925c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:35:28 +0200 Subject: [PATCH 02/19] rename files --- .../double-negation-modality.lagda.md | 2 +- ...property-family-of-fibers-of-maps.lagda.md | 7 +++-- src/orthogonal-factorization-systems.lagda.md | 3 -- .../extensions-of-maps.lagda.md | 2 +- .../fiberwise-orthogonal-maps.lagda.md | 2 +- .../identity-modality.lagda.md | 2 +- .../local-families-of-types.lagda.md | 6 ++-- ...agda.md => localizations-at-maps.lagda.md} | 12 +++---- ...=> localizations-at-subuniverses.lagda.md} | 10 +++--- .../maps-local-at-maps.lagda.md | 31 ++++++++++++++++--- .../null-maps.lagda.md | 2 +- .../null-types.lagda.md | 2 +- .../orthogonal-maps.lagda.md | 2 +- .../raise-modalities.lagda.md | 2 +- .../reflective-modalities.lagda.md | 2 +- .../reflective-subuniverses.lagda.md | 13 ++++---- .../separated-types.lagda.md | 4 +-- .../types-colocal-at-maps.lagda.md | 4 +-- ....lagda.md => types-local-at-maps.lagda.md} | 6 ++-- .../uniquely-eliminating-modalities.lagda.md | 9 +++--- .../zero-modality.lagda.md | 2 +- 21 files changed, 74 insertions(+), 51 deletions(-) rename src/orthogonal-factorization-systems/{localizations-maps.lagda.md => localizations-at-maps.lagda.md} (84%) rename src/orthogonal-factorization-systems/{localizations-subuniverses.lagda.md => localizations-at-subuniverses.lagda.md} (91%) rename src/orthogonal-factorization-systems/{local-types.lagda.md => types-local-at-maps.lagda.md} (98%) diff --git a/src/foundation/double-negation-modality.lagda.md b/src/foundation/double-negation-modality.lagda.md index d313b548d3..afb96ab73d 100644 --- a/src/foundation/double-negation-modality.lagda.md +++ b/src/foundation/double-negation-modality.lagda.md @@ -14,8 +14,8 @@ open import foundation-core.function-types open import foundation-core.propositions open import foundation-core.transport-along-identifications -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.types-local-at-maps open import orthogonal-factorization-systems.uniquely-eliminating-modalities ``` diff --git a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md index 36da197f0c..a9d2691df4 100644 --- a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md +++ b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md @@ -407,9 +407,10 @@ module _ ### A type family `C` over `B` satisfies the universal property of the family of fibers of a map `f : A → B` if and only if the constant map `C b → (fiber f b → C b)` is an equivalence for every `b : B` In other words, the dependent type `C` is -`f`-[local](orthogonal-factorization-systems.local-types.md) if its fiber over -`b` is `fiber f b`-[null](orthogonal-factorization-systems.null-types.md) for -every `b : B`. +`f`-[local](orthogonal-factorization-systems.types-local-at-maps.md) if its +fiber over `b` is +`fiber f b`-[null](orthogonal-factorization-systems.null-types.md) for every +`b : B`. This condition simplifies, for example, the proof that [connected maps](foundation.connected-maps.md) satisfy a dependent universal diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index 43406110dc..6169dfd317 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -34,9 +34,6 @@ open import orthogonal-factorization-systems.lifting-structures-on-squares publi open import orthogonal-factorization-systems.lifts-families-of-elements public open import orthogonal-factorization-systems.lifts-of-maps public open import orthogonal-factorization-systems.local-families-of-types public -open import orthogonal-factorization-systems.local-types public -open import orthogonal-factorization-systems.localizations-maps public -open import orthogonal-factorization-systems.localizations-subuniverses public open import orthogonal-factorization-systems.locally-small-modal-operators public open import orthogonal-factorization-systems.maps-local-at-maps public open import orthogonal-factorization-systems.mere-lifting-properties public diff --git a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md index 02e43793b1..1c04e75a4b 100644 --- a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md @@ -38,7 +38,7 @@ open import foundation.whiskering-homotopies-composition open import foundation-core.torsorial-type-families -open import orthogonal-factorization-systems.local-types +open import orthogonal-factorization-systems.types-local-at-maps ```
diff --git a/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md index 0a17ec3748..2cc4966422 100644 --- a/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/fiberwise-orthogonal-maps.lagda.md @@ -45,10 +45,10 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import orthogonal-factorization-systems.lifting-structures-on-squares -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.null-maps open import orthogonal-factorization-systems.orthogonal-maps open import orthogonal-factorization-systems.pullback-hom +open import orthogonal-factorization-systems.types-local-at-maps ``` diff --git a/src/orthogonal-factorization-systems/identity-modality.lagda.md b/src/orthogonal-factorization-systems/identity-modality.lagda.md index ddd8624de0..34bcadc7b1 100644 --- a/src/orthogonal-factorization-systems/identity-modality.lagda.md +++ b/src/orthogonal-factorization-systems/identity-modality.lagda.md @@ -11,8 +11,8 @@ open import foundation.equivalences open import foundation.function-types open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.types-local-at-maps open import orthogonal-factorization-systems.uniquely-eliminating-modalities ``` diff --git a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md b/src/orthogonal-factorization-systems/local-families-of-types.lagda.md index 65190f6342..a1a1fb98c4 100644 --- a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md +++ b/src/orthogonal-factorization-systems/local-families-of-types.lagda.md @@ -13,8 +13,8 @@ open import foundation.precomposition-functions open import foundation.propositions open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.orthogonal-maps +open import orthogonal-factorization-systems.types-local-at-maps ``` @@ -55,5 +55,5 @@ This remains to be formalized. ## See also - [Local maps](orthogonal-factorization-systems.maps-local-at-maps.md) -- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md) -- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) +- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md) +- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/localizations-maps.lagda.md b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md similarity index 84% rename from src/orthogonal-factorization-systems/localizations-maps.lagda.md rename to src/orthogonal-factorization-systems/localizations-at-maps.lagda.md index 265f973ff8..d2b5e52a20 100644 --- a/src/orthogonal-factorization-systems/localizations-maps.lagda.md +++ b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md @@ -1,7 +1,7 @@ # Localizations at maps ```agda -module orthogonal-factorization-systems.localizations-maps where +module orthogonal-factorization-systems.localizations-at-maps where ```
Imports @@ -11,8 +11,8 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types -open import orthogonal-factorization-systems.localizations-subuniverses +open import orthogonal-factorization-systems.types-local-at-maps +open import orthogonal-factorization-systems.localizations-at-subuniverses ```
@@ -21,9 +21,9 @@ open import orthogonal-factorization-systems.localizations-subuniverses Let `f` be a map of type `A → B` and let `X` be a type. The **localization** of `X` at `f`, or **`f`-localization**, is an -`f`[-local](orthogonal-factorization-systems.local-types.md) type `Y` together -with a map `η : X → Y` with the property that every type that is `f`-local is -also `η`-local. +`f`[-local](orthogonal-factorization-systems.types-local-at-maps.md) type `Y` +together with a map `η : X → Y` with the property that every type that is +`f`-local is also `η`-local. ## Definition diff --git a/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md b/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md similarity index 91% rename from src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md rename to src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md index 9da1074c37..1c3db24900 100644 --- a/src/orthogonal-factorization-systems/localizations-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/localizations-at-subuniverses.lagda.md @@ -1,7 +1,7 @@ # Localizations at subuniverses ```agda -module orthogonal-factorization-systems.localizations-subuniverses where +module orthogonal-factorization-systems.localizations-at-subuniverses where ```
Imports @@ -12,7 +12,7 @@ open import foundation.dependent-pair-types open import foundation.subuniverses open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types +open import orthogonal-factorization-systems.types-local-at-maps ```
@@ -22,8 +22,8 @@ open import orthogonal-factorization-systems.local-types Let `P` be a [subuniverse](foundation.subuniverses.md). Given a type `X`, its **localization** at `P`, or **`P`-localization**, is a type `Y` in `P` and a map `η : X → Y` such that every type in `P` is -`η`[-local](orthogonal-factorization-systems.local-types.md). I.e. for every `Z` -in `P`, the [precomposition map](foundation-core.function-types.md) +`η`[-local](orthogonal-factorization-systems.types-local-at-maps.md). I.e. for +every `Z` in `P`, the [precomposition map](foundation-core.function-types.md) ```text _∘ η : (Y → Z) → (X → Z) @@ -112,7 +112,7 @@ This is Proposition 5.1.2 in _Classifying Types_, and remains to be formalized. ## See also -- [Localizations at maps](orthogonal-factorization-systems.localizations-maps.md) +- [Localizations at maps](orthogonal-factorization-systems.localizations-at-maps.md) ## References diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md index d6a21041ac..da7f65f3c8 100644 --- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md @@ -30,9 +30,9 @@ open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universe-levels open import orthogonal-factorization-systems.local-families-of-types -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.orthogonal-maps open import orthogonal-factorization-systems.pullback-hom +open import orthogonal-factorization-systems.types-local-at-maps ``` @@ -44,7 +44,7 @@ A map `g : X → Y` is said to be `f : A → B`, or {{#concept "`f`-local" Disambiguation="maps of types" Agda=is-local-map}}, if all its [fibers](foundation-core.fibers-of-maps.md) are -[`f`-local types](orthogonal-factorization-systems.local-types.md). +[`f`-local types](orthogonal-factorization-systems.types-local-at-maps.md). ## Definition @@ -109,7 +109,30 @@ module _ ( G)) ``` +### `f`-local maps are closed under base change + +Maps in `𝒫` are closed under base change. + +```agda +module _ + {α : Level → Level} (𝒫 : global-subuniverse α) + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + (f : A → B) (g : C → D) + where + + is-in-global-subuniverse-map-base-change : + is-in-global-subuniverse-map 𝒫 f → + cartesian-hom-arrow g f → + is-in-global-subuniverse-map 𝒫 g + is-in-global-subuniverse-map-base-change F α d = + is-closed-under-equiv-global-subuniverse 𝒫 (l1 ⊔ l2) (l3 ⊔ l4) + ( fiber f (map-codomain-cartesian-hom-arrow g f α d)) + ( fiber g d) + ( inv-equiv (equiv-fibers-cartesian-hom-arrow g f α d)) + ( F (map-codomain-cartesian-hom-arrow g f α d)) +``` + ## See also -- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md) -- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) +- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md) +- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/null-maps.lagda.md b/src/orthogonal-factorization-systems/null-maps.lagda.md index 377685ddd0..af001e1fc2 100644 --- a/src/orthogonal-factorization-systems/null-maps.lagda.md +++ b/src/orthogonal-factorization-systems/null-maps.lagda.md @@ -30,11 +30,11 @@ open import foundation.unit-type open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.maps-local-at-maps open import orthogonal-factorization-systems.null-families-of-types open import orthogonal-factorization-systems.null-types open import orthogonal-factorization-systems.orthogonal-maps +open import orthogonal-factorization-systems.types-local-at-maps ``` diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md index ec6db3ea44..1e75914240 100644 --- a/src/orthogonal-factorization-systems/null-types.lagda.md +++ b/src/orthogonal-factorization-systems/null-types.lagda.md @@ -29,9 +29,9 @@ open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universal-property-unit-type open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.maps-local-at-maps open import orthogonal-factorization-systems.orthogonal-maps +open import orthogonal-factorization-systems.types-local-at-maps ``` diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index 38071154f6..bec501ea4d 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -49,8 +49,8 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import orthogonal-factorization-systems.lifting-structures-on-squares -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.pullback-hom +open import orthogonal-factorization-systems.types-local-at-maps ``` diff --git a/src/orthogonal-factorization-systems/raise-modalities.lagda.md b/src/orthogonal-factorization-systems/raise-modalities.lagda.md index 2b0597b2fa..1f7569b41d 100644 --- a/src/orthogonal-factorization-systems/raise-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/raise-modalities.lagda.md @@ -11,8 +11,8 @@ open import foundation.function-types open import foundation.raising-universe-levels open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.types-local-at-maps open import orthogonal-factorization-systems.uniquely-eliminating-modalities ``` diff --git a/src/orthogonal-factorization-systems/reflective-modalities.lagda.md b/src/orthogonal-factorization-systems/reflective-modalities.lagda.md index c071673c5f..46c235675f 100644 --- a/src/orthogonal-factorization-systems/reflective-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-modalities.lagda.md @@ -40,4 +40,4 @@ reflective-modality l = ## See also -- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) +- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md index 12bfb73be0..0820e4ea84 100644 --- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md @@ -19,11 +19,11 @@ open import foundation.retractions open import foundation.subuniverses open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types -open import orthogonal-factorization-systems.localizations-subuniverses +open import orthogonal-factorization-systems.localizations-at-subuniverses open import orthogonal-factorization-systems.modal-induction open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.modal-subuniverse-induction +open import orthogonal-factorization-systems.types-local-at-maps ``` @@ -34,9 +34,10 @@ A **reflective subuniverse** is a [subuniverse](foundation.subuniverses.md) `P` together with a reflecting operator `○ : UU → UU` that take values in `P`, and a [modal unit](orthogonal-factorization-systems.modal-operators.md) `A → ○ A` for all [small types](foundation-core.small-types.md) `A`, with the property that -the types in `P` are [local](orthogonal-factorization-systems.local-types.md) at -the modal unit for every `A`. Hence the modal types with respect to `○` are -precisely the types in the reflective subuniverse. +the types in `P` are +[local](orthogonal-factorization-systems.types-local-at-maps.md) at the modal +unit for every `A`. Hence the modal types with respect to `○` are precisely the +types in the reflective subuniverse. ## Definitions @@ -236,7 +237,7 @@ module _ ## See also - [Σ-closed reflective subuniverses](orthogonal-factorization-systems.sigma-closed-reflective-subuniverses.md) -- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) +- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md) ## References diff --git a/src/orthogonal-factorization-systems/separated-types.lagda.md b/src/orthogonal-factorization-systems/separated-types.lagda.md index 995088d422..61c892b3fa 100644 --- a/src/orthogonal-factorization-systems/separated-types.lagda.md +++ b/src/orthogonal-factorization-systems/separated-types.lagda.md @@ -10,7 +10,7 @@ module orthogonal-factorization-systems.separated-types where open import foundation.identity-types open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types +open import orthogonal-factorization-systems.types-local-at-maps ``` @@ -19,7 +19,7 @@ open import orthogonal-factorization-systems.local-types A type `A` is said to be **separated** with respect to a map `f`, or **`f`-separated**, if its [identity types](foundation-core.identity-types.md) -are [`f`-local](orthogonal-factorization-systems.local-types.md). +are [`f`-local](orthogonal-factorization-systems.types-local-at-maps.md). ## Definition diff --git a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md index e474f0d6af..7292a82aa0 100644 --- a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md @@ -57,8 +57,8 @@ Equivalently, `A` is colocal if `f`. The notion of `f`-colocal types is dual to -[`f`-local types](orthogonal-factorization-systems.local-types.md), which is a -type such that the +[`f`-local types](orthogonal-factorization-systems.types-local-at-maps.md), +which is a type such that the [precomposition map](foundation-core.precomposition-functions.md) ```text diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md similarity index 98% rename from src/orthogonal-factorization-systems/local-types.lagda.md rename to src/orthogonal-factorization-systems/types-local-at-maps.lagda.md index 80c70292c3..7cce8145bb 100644 --- a/src/orthogonal-factorization-systems/local-types.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -1,7 +1,7 @@ # Local types ```agda -module orthogonal-factorization-systems.local-types where +module orthogonal-factorization-systems.types-local-at-maps where ```
Imports @@ -359,5 +359,5 @@ is-contr-is-local A is-local-A = ## See also - [Local maps](orthogonal-factorization-systems.maps-local-at-maps.md) -- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-maps.md) -- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) +- [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md) +- [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-at-subuniverses.md) diff --git a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md index 2857183224..a24fcd2162 100644 --- a/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/uniquely-eliminating-modalities.lagda.md @@ -20,8 +20,8 @@ open import foundation.propositions open import foundation.univalence open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.types-local-at-maps ```
@@ -31,9 +31,10 @@ open import orthogonal-factorization-systems.modal-operators A **uniquely eliminating modality** is a _higher mode of logic_ defined in terms of a monadic [modal operator](orthogonal-factorization-systems.modal-operators.md) `○` -satisfying a certain [locality](orthogonal-factorization-systems.local-types.md) -condition. Namely, that dependent precomposition by the modal unit `unit-○` is -an equivalence for type families over types in the image of the operator: +satisfying a certain +[locality](orthogonal-factorization-systems.types-local-at-maps.md) condition. +Namely, that dependent precomposition by the modal unit `unit-○` is an +equivalence for type families over types in the image of the operator: ```text - ∘ unit-○ : Π (x : ○ X) (○ (P x)) ≃ Π (x : X) (○ (P (unit-○ x))) diff --git a/src/orthogonal-factorization-systems/zero-modality.lagda.md b/src/orthogonal-factorization-systems/zero-modality.lagda.md index 855dba60bc..6395eb912e 100644 --- a/src/orthogonal-factorization-systems/zero-modality.lagda.md +++ b/src/orthogonal-factorization-systems/zero-modality.lagda.md @@ -10,8 +10,8 @@ module orthogonal-factorization-systems.zero-modality where open import foundation.unit-type open import foundation.universe-levels -open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.types-local-at-maps open import orthogonal-factorization-systems.uniquely-eliminating-modalities ``` From a7db80cef67099fcac43eb8f2e0e979fe3f2201f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:41:24 +0200 Subject: [PATCH 03/19] rename more files --- src/orthogonal-factorization-systems.lagda.md | 2 +- ...arated-types.lagda.md => types-separated-at-maps.lagda.md} | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) rename src/orthogonal-factorization-systems/{separated-types.lagda.md => types-separated-at-maps.lagda.md} (90%) diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index 6169dfd317..2e065951eb 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -52,7 +52,7 @@ open import orthogonal-factorization-systems.raise-modalities public open import orthogonal-factorization-systems.reflective-modalities public open import orthogonal-factorization-systems.reflective-subuniverses public open import orthogonal-factorization-systems.regular-cd-structures public -open import orthogonal-factorization-systems.separated-types public +open import orthogonal-factorization-systems.types-separated-at-maps public open import orthogonal-factorization-systems.sigma-closed-modalities public open import orthogonal-factorization-systems.sigma-closed-reflective-modalities public open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses public diff --git a/src/orthogonal-factorization-systems/separated-types.lagda.md b/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md similarity index 90% rename from src/orthogonal-factorization-systems/separated-types.lagda.md rename to src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md index 61c892b3fa..d47b4396a1 100644 --- a/src/orthogonal-factorization-systems/separated-types.lagda.md +++ b/src/orthogonal-factorization-systems/types-separated-at-maps.lagda.md @@ -1,7 +1,7 @@ -# Separated types +# Types separated at maps ```agda -module orthogonal-factorization-systems.separated-types where +module orthogonal-factorization-systems.types-separated-at-maps where ```
Imports From 7a457b6b1df679410acaac899bf6f543ec246ddc Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:41:29 +0200 Subject: [PATCH 04/19] pre-commit --- .../localizations-at-maps.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md index d2b5e52a20..1144d685d4 100644 --- a/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/localizations-at-maps.lagda.md @@ -11,8 +11,8 @@ open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.universe-levels -open import orthogonal-factorization-systems.types-local-at-maps open import orthogonal-factorization-systems.localizations-at-subuniverses +open import orthogonal-factorization-systems.types-local-at-maps ```
From 12de16bf098d316aa6c2b7d2ebd6c8171261adf6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:41:42 +0200 Subject: [PATCH 05/19] pre-commit --- src/orthogonal-factorization-systems.lagda.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index 2e065951eb..53e2408e5e 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -34,6 +34,8 @@ open import orthogonal-factorization-systems.lifting-structures-on-squares publi open import orthogonal-factorization-systems.lifts-families-of-elements public open import orthogonal-factorization-systems.lifts-of-maps public open import orthogonal-factorization-systems.local-families-of-types public +open import orthogonal-factorization-systems.localizations-at-maps public +open import orthogonal-factorization-systems.localizations-at-subuniverses public open import orthogonal-factorization-systems.locally-small-modal-operators public open import orthogonal-factorization-systems.maps-local-at-maps public open import orthogonal-factorization-systems.mere-lifting-properties public @@ -52,12 +54,13 @@ open import orthogonal-factorization-systems.raise-modalities public open import orthogonal-factorization-systems.reflective-modalities public open import orthogonal-factorization-systems.reflective-subuniverses public open import orthogonal-factorization-systems.regular-cd-structures public -open import orthogonal-factorization-systems.types-separated-at-maps public open import orthogonal-factorization-systems.sigma-closed-modalities public open import orthogonal-factorization-systems.sigma-closed-reflective-modalities public open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses public open import orthogonal-factorization-systems.stable-orthogonal-factorization-systems public open import orthogonal-factorization-systems.types-colocal-at-maps public +open import orthogonal-factorization-systems.types-local-at-maps public +open import orthogonal-factorization-systems.types-separated-at-maps public open import orthogonal-factorization-systems.uniquely-eliminating-modalities public open import orthogonal-factorization-systems.wide-function-classes public open import orthogonal-factorization-systems.wide-global-function-classes public From 6cc90b805f7e213220dc068aab59bb516a7ed4ac Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:43:04 +0200 Subject: [PATCH 06/19] rename more files --- src/foundation.lagda.md | 2 +- ...g-extension-fundamental-theorem-of-identity-types.lagda.md | 4 ++-- ...ypes.lagda.md => types-separated-at-subuniverses.lagda.md} | 4 ++-- .../higher-modalities.lagda.md | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) rename src/foundation/{separated-types.lagda.md => types-separated-at-subuniverses.lagda.md} (93%) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index b892a43bab..8fd21d45c8 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -342,7 +342,6 @@ open import foundation.retracts-of-maps public open import foundation.retracts-of-types public open import foundation.russells-paradox public open import foundation.sections public -open import foundation.separated-types public open import foundation.sequences public open import foundation.sequential-limits public open import foundation.set-presented-types public @@ -423,6 +422,7 @@ open import foundation.type-arithmetic-empty-type public open import foundation.type-arithmetic-unit-type public open import foundation.type-duality public open import foundation.type-theoretic-principle-of-choice public +open import foundation.types-separated-at-subuniverses public open import foundation.unions-subtypes public open import foundation.uniqueness-image public open import foundation.uniqueness-quantification public diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index 4de8f33103..cd95331a10 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -26,12 +26,12 @@ open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.maps-in-subuniverses open import foundation.propositional-truncations -open import foundation.separated-types open import foundation.subuniverses open import foundation.surjective-maps open import foundation.truncated-maps open import foundation.truncated-types open import foundation.truncation-levels +open import foundation.types-separated-at-subuniverses open import foundation.universe-levels ``` @@ -51,7 +51,7 @@ asserts that for any [subuniverse](foundation.subuniverses.md) `P`, and any i.e., a family of maps with [fibers](foundation-core.fibers-of-maps.md) in `P`. 2. The [total space](foundation.dependent-pair-types.md) `Σ A B` is - [`P`-separated](foundation.separated-types.md), i.e., its + [`P`-separated](foundation.types-separated-at-subuniverses.md), i.e., its [identity types](foundation-core.identity-types.md) are in `P`. In other words, the extended fundamental theorem of diff --git a/src/foundation/separated-types.lagda.md b/src/foundation/types-separated-at-subuniverses.lagda.md similarity index 93% rename from src/foundation/separated-types.lagda.md rename to src/foundation/types-separated-at-subuniverses.lagda.md index 205ee03495..cfbe263171 100644 --- a/src/foundation/separated-types.lagda.md +++ b/src/foundation/types-separated-at-subuniverses.lagda.md @@ -1,7 +1,7 @@ -# Separated types +# Types separated at subuniverses ```agda -module foundation.separated-types where +module foundation.types-separated-at-subuniverses where ```
Imports diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md index ac69913f80..8f7e808141 100644 --- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md @@ -47,8 +47,8 @@ defining map (propositionally). Lastly, higher modalities must also be **identity closed** in the sense that for every type `X` the identity types `(x' ＝ y')` are modal for all terms `x' y' : ○ X`. In other words, `○ X` is -[`○`-separated](foundation.separated-types.md). Because of this, higher -modalities in their most general form only make sense for +[`○`-separated](foundation.types-separated-at-subuniverses.md). Because of this, +higher modalities in their most general form only make sense for [locally small modal operators](orthogonal-factorization-systems.locally-small-modal-operators.md). ## Definition From f15e905ab6c212638662a76298d79281f177da33 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:46:47 +0200 Subject: [PATCH 07/19] remove term "homogenous equivalence" --- src/foundation/global-subuniverses.lagda.md | 10 +++++----- .../global-function-classes.lagda.md | 5 +++-- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/foundation/global-subuniverses.lagda.md b/src/foundation/global-subuniverses.lagda.md index 97fa1d116c..e000dc080e 100644 --- a/src/foundation/global-subuniverses.lagda.md +++ b/src/foundation/global-subuniverses.lagda.md @@ -116,7 +116,7 @@ module _ ## Properties -### Global subuniverses are closed under homogenous equivalences +### Global subuniverses are closed under equivalences between types in a single universe This is true for any family of subuniverses indexed by universe levels. @@ -126,14 +126,14 @@ module _ {l : Level} {X Y : UU l} where - is-in-global-subuniverse-homogenous-equiv : + is-in-global-subuniverse-equiv-Level : X ≃ Y → is-in-global-subuniverse P X → is-in-global-subuniverse P Y - is-in-global-subuniverse-homogenous-equiv = + is-in-global-subuniverse-equiv-Level = is-in-subuniverse-equiv (subuniverse-global-subuniverse P l) - is-in-global-subuniverse-homogenous-equiv' : + is-in-global-subuniverse-equiv-Level' : X ≃ Y → is-in-global-subuniverse P Y → is-in-global-subuniverse P X - is-in-global-subuniverse-homogenous-equiv' = + is-in-global-subuniverse-equiv-Level' = is-in-subuniverse-equiv' (subuniverse-global-subuniverse P l) ``` diff --git a/src/orthogonal-factorization-systems/global-function-classes.lagda.md b/src/orthogonal-factorization-systems/global-function-classes.lagda.md index d400eeea18..b02a191e53 100644 --- a/src/orthogonal-factorization-systems/global-function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/global-function-classes.lagda.md @@ -26,9 +26,10 @@ open import orthogonal-factorization-systems.function-classes A **global function class** is a global [subtype](foundation.subtypes.md) of function types that is closed under composition with -[equivalences](foundation-core.equivalences.md). +[equivalences](foundation-core.equivalences.md) between types in arbitrary +universes. -Note that composition with homogenous equivalences follows from +Note that composition with equivalences within a single universe follows from [univalence](foundation.univalence.md), so this condition should hold for the correct universe polymorphic definition. From 8c2351952a62be28542f5b2e4db0ac3f5bf9969f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 3 Oct 2024 23:47:40 +0200 Subject: [PATCH 08/19] a link universes --- .../global-function-classes.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/orthogonal-factorization-systems/global-function-classes.lagda.md b/src/orthogonal-factorization-systems/global-function-classes.lagda.md index b02a191e53..b11fa84d13 100644 --- a/src/orthogonal-factorization-systems/global-function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/global-function-classes.lagda.md @@ -27,7 +27,7 @@ open import orthogonal-factorization-systems.function-classes A **global function class** is a global [subtype](foundation.subtypes.md) of function types that is closed under composition with [equivalences](foundation-core.equivalences.md) between types in arbitrary -universes. +[universes](foundation.universe-levels.md). Note that composition with equivalences within a single universe follows from [univalence](foundation.univalence.md), so this condition should hold for the From e80d6762f5b405a47147ce095b0270424198d849 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 4 Oct 2024 00:03:37 +0200 Subject: [PATCH 09/19] some wording improvements --- .../higher-modalities.lagda.md | 17 +-- .../reflective-subuniverses.lagda.md | 112 +++++++++--------- .../sigma-closed-modalities.lagda.md | 4 +- 3 files changed, 68 insertions(+), 65 deletions(-) diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md index 8f7e808141..15d064f720 100644 --- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md @@ -33,22 +33,23 @@ open import orthogonal-factorization-systems.uniquely-eliminating-modalities ## Idea -A **higher modality** is a _higher mode of logic_ defined in terms of a monadic +A {{#concept "higher modality" Disambiguation="on types" Agda=higher-modality}} +is a _higher mode of logic_ defined in terms of an monadic [modal operator](orthogonal-factorization-systems.modal-operators.md) `○` satisfying a certain induction principle. -The induction principle states that for every type `X` and family -`P : ○ X → UU`, to define a dependent map `(x' : ○ X) → ○ (P x')` it suffices to -define it on the image of the modal unit, i.e. `(x : X) → ○ (P (unit-○ x))`. -Moreover, it satisfies a computation principle stating that when evaluating a -map defined in this manner on the image of the modal unit, one recovers the -defining map (propositionally). +The induction principle states that for every type `X` and family `P : ○ X → 𝒰`, +to define a dependent map `(x' : ○ X) → ○ (P x')` it suffices to define it on +the image of the modal unit, i.e. `(x : X) → ○ (P (unit-○ x))`. Moreover, it +satisfies a computation principle stating that when evaluating a map defined in +this manner on the image of the modal unit, one recovers the defining map +(propositionally). Lastly, higher modalities must also be **identity closed** in the sense that for every type `X` the identity types `(x' ＝ y')` are modal for all terms `x' y' : ○ X`. In other words, `○ X` is [`○`-separated](foundation.types-separated-at-subuniverses.md). Because of this, -higher modalities in their most general form only make sense for +(small) higher modalities in their most general form only make sense for [locally small modal operators](orthogonal-factorization-systems.locally-small-modal-operators.md). ## Definition diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md index 0820e4ea84..7869f98193 100644 --- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md @@ -30,14 +30,16 @@ open import orthogonal-factorization-systems.types-local-at-maps ## Idea -A **reflective subuniverse** is a [subuniverse](foundation.subuniverses.md) `P` -together with a reflecting operator `○ : UU → UU` that take values in `P`, and a -[modal unit](orthogonal-factorization-systems.modal-operators.md) `A → ○ A` for -all [small types](foundation-core.small-types.md) `A`, with the property that -the types in `P` are -[local](orthogonal-factorization-systems.types-local-at-maps.md) at the modal -unit for every `A`. Hence the modal types with respect to `○` are precisely the -types in the reflective subuniverse. +A +{{#concept "reflective subuniverse" Disambiguation="of types" Agda=reflective-subuniverse}}, +or +{{#concept "localization" Disambiguation="subuniverse" Agda=reflective-subuniverse}}, +is a [subuniverse](foundation.subuniverses.md) `𝒫` together with a reflecting +operator on the [universe](foundation.universe-levels.md) `L : 𝒰 → 𝒫`, and a +family of unit maps `η : A → LA` for all small types `A`, with the property that +the types in `𝒫` are +[local](orthogonal-factorization-systems.types-local-at-maps.md) at the unit for +every `A`. ## Definitions @@ -45,41 +47,41 @@ types in the reflective subuniverse. ```agda is-reflective-subuniverse : - {l1 l2 : Level} (P : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2) -is-reflective-subuniverse {l1} P = + {l1 l2 : Level} (𝒫 : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2) +is-reflective-subuniverse {l1} 𝒫 = Σ ( operator-modality l1 l1) - ( λ ○ → - Σ ( unit-modality ○) - ( λ unit-○ → - ( (X : UU l1) → is-in-subuniverse P (○ X)) × - ( (X Y : UU l1) → is-in-subuniverse P X → is-local (unit-○ {Y}) X))) + ( λ L → + Σ ( unit-modality L) + ( λ η → + ( (X : UU l1) → is-in-subuniverse 𝒫 (L X)) × + ( (X Y : UU l1) → is-in-subuniverse 𝒫 X → is-local (η {Y}) X))) ``` ```agda module _ - {l1 l2 : Level} (P : subuniverse l1 l2) - (is-reflective-P : is-reflective-subuniverse P) + {l1 l2 : Level} (𝒫 : subuniverse l1 l2) + (is-reflective-𝒫 : is-reflective-subuniverse 𝒫) where operator-is-reflective-subuniverse : operator-modality l1 l1 - operator-is-reflective-subuniverse = pr1 is-reflective-P + operator-is-reflective-subuniverse = pr1 is-reflective-𝒫 unit-is-reflective-subuniverse : unit-modality (operator-is-reflective-subuniverse) - unit-is-reflective-subuniverse = pr1 (pr2 is-reflective-P) + unit-is-reflective-subuniverse = pr1 (pr2 is-reflective-𝒫) is-in-subuniverse-operator-type-is-reflective-subuniverse : (X : UU l1) → - is-in-subuniverse P (operator-is-reflective-subuniverse X) + is-in-subuniverse 𝒫 (operator-is-reflective-subuniverse X) is-in-subuniverse-operator-type-is-reflective-subuniverse = - pr1 (pr2 (pr2 is-reflective-P)) + pr1 (pr2 (pr2 is-reflective-𝒫)) is-local-is-in-subuniverse-is-reflective-subuniverse : (X Y : UU l1) → - is-in-subuniverse P X → + is-in-subuniverse 𝒫 X → is-local (unit-is-reflective-subuniverse {Y}) X is-local-is-in-subuniverse-is-reflective-subuniverse = - pr2 (pr2 (pr2 is-reflective-P)) + pr2 (pr2 (pr2 is-reflective-𝒫)) ``` ### The type of reflective subuniverses @@ -92,11 +94,11 @@ reflective-subuniverse l1 l2 = ```agda module _ - {l1 l2 : Level} (P : reflective-subuniverse l1 l2) + {l1 l2 : Level} (𝒫 : reflective-subuniverse l1 l2) where subuniverse-reflective-subuniverse : subuniverse l1 l2 - subuniverse-reflective-subuniverse = pr1 P + subuniverse-reflective-subuniverse = pr1 𝒫 is-in-reflective-subuniverse : UU l1 → UU l2 is-in-reflective-subuniverse = @@ -109,7 +111,7 @@ module _ is-reflective-subuniverse-reflective-subuniverse : is-reflective-subuniverse (subuniverse-reflective-subuniverse) - is-reflective-subuniverse-reflective-subuniverse = pr2 P + is-reflective-subuniverse-reflective-subuniverse = pr2 𝒫 operator-reflective-subuniverse : operator-modality l1 l1 operator-reflective-subuniverse = @@ -150,87 +152,87 @@ module _ ```agda module _ - {l1 l2 : Level} (P : subuniverse l1 l2) - (is-reflective-P : is-reflective-subuniverse P) + {l1 l2 : Level} (𝒫 : subuniverse l1 l2) + (is-reflective-𝒫 : is-reflective-subuniverse 𝒫) where has-all-localizations-is-reflective-subuniverse : - (A : UU l1) → subuniverse-localization P A + (A : UU l1) → subuniverse-localization 𝒫 A pr1 (has-all-localizations-is-reflective-subuniverse A) = - operator-is-reflective-subuniverse P is-reflective-P A + operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 A pr1 (pr2 (has-all-localizations-is-reflective-subuniverse A)) = is-in-subuniverse-operator-type-is-reflective-subuniverse - P is-reflective-P A + 𝒫 is-reflective-𝒫 A pr1 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) = - unit-is-reflective-subuniverse P is-reflective-P + unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫 pr2 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) X is-in-subuniverse-X = is-local-is-in-subuniverse-is-reflective-subuniverse - P is-reflective-P X A is-in-subuniverse-X + 𝒫 is-reflective-𝒫 X A is-in-subuniverse-X module _ - {l1 l2 : Level} (P : subuniverse l1 l2) - (L : (A : UU l1) → subuniverse-localization P A) + {l1 l2 : Level} (𝒫 : subuniverse l1 l2) + (L : (A : UU l1) → subuniverse-localization 𝒫 A) where is-reflective-has-all-localizations-subuniverse : - is-reflective-subuniverse P + is-reflective-subuniverse 𝒫 pr1 is-reflective-has-all-localizations-subuniverse A = - type-subuniverse-localization P (L A) + type-subuniverse-localization 𝒫 (L A) pr1 (pr2 is-reflective-has-all-localizations-subuniverse) {A} = - unit-subuniverse-localization P (L A) + unit-subuniverse-localization 𝒫 (L A) pr1 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse)) A = - is-in-subuniverse-subuniverse-localization P (L A) + is-in-subuniverse-subuniverse-localization 𝒫 (L A) pr2 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse)) A B is-in-subuniverse-A = is-local-at-unit-is-in-subuniverse-subuniverse-localization - P (L B) A is-in-subuniverse-A + 𝒫 (L B) A is-in-subuniverse-A ``` ## Recursion for reflective subuniverses ```agda module _ - {l1 l2 : Level} (P : subuniverse l1 l2) - (is-reflective-P : is-reflective-subuniverse P) + {l1 l2 : Level} (𝒫 : subuniverse l1 l2) + (is-reflective-𝒫 : is-reflective-subuniverse 𝒫) where rec-modality-is-reflective-subuniverse : - rec-modality (unit-is-reflective-subuniverse P is-reflective-P) + rec-modality (unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫) rec-modality-is-reflective-subuniverse {X} {Y} = map-inv-is-equiv ( is-local-is-in-subuniverse-is-reflective-subuniverse - ( P) - ( is-reflective-P) - ( operator-is-reflective-subuniverse P is-reflective-P Y) + ( 𝒫) + ( is-reflective-𝒫) + ( operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 Y) ( X) ( is-in-subuniverse-operator-type-is-reflective-subuniverse - ( P) - ( is-reflective-P) + ( 𝒫) + ( is-reflective-𝒫) ( Y))) map-is-reflective-subuniverse : {X Y : UU l1} → (X → Y) → - operator-is-reflective-subuniverse P is-reflective-P X → - operator-is-reflective-subuniverse P is-reflective-P Y + operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 X → + operator-is-reflective-subuniverse 𝒫 is-reflective-𝒫 Y map-is-reflective-subuniverse = ap-map-rec-modality - ( unit-is-reflective-subuniverse P is-reflective-P) + ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫) ( rec-modality-is-reflective-subuniverse) strong-rec-subuniverse-is-reflective-subuniverse : strong-rec-subuniverse-modality - ( unit-is-reflective-subuniverse P is-reflective-P) + ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫) strong-rec-subuniverse-is-reflective-subuniverse = strong-rec-subuniverse-rec-modality - ( unit-is-reflective-subuniverse P is-reflective-P) + ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫) ( rec-modality-is-reflective-subuniverse) rec-subuniverse-is-reflective-subuniverse : - rec-subuniverse-modality (unit-is-reflective-subuniverse P is-reflective-P) + rec-subuniverse-modality (unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫) rec-subuniverse-is-reflective-subuniverse = rec-subuniverse-rec-modality - ( unit-is-reflective-subuniverse P is-reflective-P) + ( unit-is-reflective-subuniverse 𝒫 is-reflective-𝒫) ( rec-modality-is-reflective-subuniverse) ``` diff --git a/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md b/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md index efb9bfd560..20370cd516 100644 --- a/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/sigma-closed-modalities.lagda.md @@ -21,8 +21,8 @@ open import orthogonal-factorization-systems.modal-operators A [modal operator](orthogonal-factorization-systems.modal-operators.md) with unit is **Σ-closed** if its [subuniverse](foundation.subuniverses.md) of modal -types is [Σ-closed](foundation.sigma-closed-subuniverses.md). I.e. if `Σ A B` is -modal whenever `B` is a family of modal types over modal base `A`. +types is [Σ-closed](foundation.sigma-closed-subuniverses.md). I.e., if `Σ A B` +is modal whenever `B` is a family of modal types over modal base `A`. ## Definition From 127084a460107a843480f7feb38c2d440233c768 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 4 Oct 2024 00:06:36 +0200 Subject: [PATCH 10/19] rename another file --- src/orthogonal-factorization-systems.lagda.md | 2 +- ....lagda.md => families-of-types-local-at-maps.lagda.md} | 8 ++++---- .../maps-local-at-maps.lagda.md | 2 +- .../types-local-at-maps.lagda.md | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) rename src/orthogonal-factorization-systems/{local-families-of-types.lagda.md => families-of-types-local-at-maps.lagda.md} (85%) diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index 53e2408e5e..7b75c56b74 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -22,6 +22,7 @@ open import orthogonal-factorization-systems.factorization-operations-global-fun open import orthogonal-factorization-systems.factorizations-of-maps public open import orthogonal-factorization-systems.factorizations-of-maps-function-classes public open import orthogonal-factorization-systems.factorizations-of-maps-global-function-classes public +open import orthogonal-factorization-systems.families-of-types-local-at-maps public open import orthogonal-factorization-systems.fiberwise-orthogonal-maps public open import orthogonal-factorization-systems.function-classes public open import orthogonal-factorization-systems.functoriality-higher-modalities public @@ -33,7 +34,6 @@ open import orthogonal-factorization-systems.lifting-operations public open import orthogonal-factorization-systems.lifting-structures-on-squares public open import orthogonal-factorization-systems.lifts-families-of-elements public open import orthogonal-factorization-systems.lifts-of-maps public -open import orthogonal-factorization-systems.local-families-of-types public open import orthogonal-factorization-systems.localizations-at-maps public open import orthogonal-factorization-systems.localizations-at-subuniverses public open import orthogonal-factorization-systems.locally-small-modal-operators public diff --git a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md b/src/orthogonal-factorization-systems/families-of-types-local-at-maps.lagda.md similarity index 85% rename from src/orthogonal-factorization-systems/local-families-of-types.lagda.md rename to src/orthogonal-factorization-systems/families-of-types-local-at-maps.lagda.md index a1a1fb98c4..0d79431a42 100644 --- a/src/orthogonal-factorization-systems/local-families-of-types.lagda.md +++ b/src/orthogonal-factorization-systems/families-of-types-local-at-maps.lagda.md @@ -1,7 +1,7 @@ -# Local families of types +# Families of types local at a map ```agda -module orthogonal-factorization-systems.local-families-of-types where +module orthogonal-factorization-systems.families-of-types-local-at-maps where ```
Imports @@ -22,8 +22,8 @@ open import orthogonal-factorization-systems.types-local-at-maps ## Idea A family of types `B : A → UU l` is said to be -{{#concept "local" Disambiguation="family of types" Agda=is-local-family}} at -`f : X → Y`, or **`f`-local**, if every +{{#concept "local" Disambiguation="family of types at a map" Agda=is-local-family}} +at a map `f : X → Y`, or **`f`-local**, if every [fiber](foundation-core.fibers-of-maps.md) is. ## Definition diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md index da7f65f3c8..11c130af1b 100644 --- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md @@ -29,7 +29,7 @@ open import foundation.unit-type open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universe-levels -open import orthogonal-factorization-systems.local-families-of-types +open import orthogonal-factorization-systems.families-of-types-local-at-maps open import orthogonal-factorization-systems.orthogonal-maps open import orthogonal-factorization-systems.pullback-hom open import orthogonal-factorization-systems.types-local-at-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 7cce8145bb..759b43800e 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -56,7 +56,7 @@ We reserve the name `is-local` for when `A` does not vary over `Y`, and specify with `is-local-dependent-type` when it does. Note that a local dependent type is not the same as a -[local family](orthogonal-factorization-systems.local-families-of-types.md). +[local family](orthogonal-factorization-systems.families-of-types-local-at-maps.md). While a local family is a type family `P` on some other indexing type `A`, such that each fiber is local as a nondependent type over `Y`, a local dependent type is a local type that additionally may vary over `Y`. Concretely, a local From a0bf14e0c91bed587b9613b2f18bc8a23a859554 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 4 Oct 2024 00:12:27 +0200 Subject: [PATCH 11/19] fix a header --- .../types-local-at-maps.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 759b43800e..aa278e7176 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -1,4 +1,4 @@ -# Local types +# Types local at maps ```agda module orthogonal-factorization-systems.types-local-at-maps where From 2f6e339cb366efbf8f1e3586a86d5b694b401ddc Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 4 Oct 2024 00:37:30 +0200 Subject: [PATCH 12/19] simplify a proof --- .../types-local-at-maps.lagda.md | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) 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 aa278e7176..777b70dcbd 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -344,15 +344,9 @@ module _ is-contr-is-local : {l : Level} (A : UU l) → is-local (λ (_ : empty) → star) A → is-contr A is-contr-is-local A is-local-A = - is-contr-is-equiv + is-contr-equiv ( empty → A) - ( λ a _ → a) - ( is-equiv-comp - ( λ a' _ → a' star) - ( λ a _ → - map-inv-is-equiv (is-equiv-map-left-unit-law-Π (λ _ → A)) a star) - ( is-equiv-map-inv-is-equiv (is-equiv-map-left-unit-law-Π (λ _ → A))) - ( is-local-A)) + ( (precomp (λ _ → star) A , is-local-A) ∘e inv-left-unit-law-Π (λ _ → A)) ( universal-property-empty' A) ``` From ce42d541df7020d34f5476ddacbe7d270cce9671 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 4 Oct 2024 18:40:20 +0200 Subject: [PATCH 13/19] fill holes --- .../maps-local-at-maps.lagda.md | 43 +++++++++++++------ .../types-local-at-maps.lagda.md | 20 +++++++++ 2 files changed, 49 insertions(+), 14 deletions(-) diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md index 11c130af1b..ac69503101 100644 --- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md @@ -19,12 +19,14 @@ open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-fibers-of-maps +open import foundation.global-subuniverses open import foundation.homotopies open import foundation.identity-types open import foundation.postcomposition-functions open import foundation.precomposition-functions open import foundation.propositions open import foundation.pullbacks +open import foundation.retracts-of-maps open import foundation.unit-type open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universe-levels @@ -111,25 +113,38 @@ module _ ### `f`-local maps are closed under base change -Maps in `𝒫` are closed under base change. +Maps local at `f` are closed under base change. ```agda module _ - {α : Level → Level} (𝒫 : global-subuniverse α) - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} - (f : A → B) (g : C → D) + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} + {f : A → B} {g : C → D} {g' : E → F} where - is-in-global-subuniverse-map-base-change : - is-in-global-subuniverse-map 𝒫 f → - cartesian-hom-arrow g f → - is-in-global-subuniverse-map 𝒫 g - is-in-global-subuniverse-map-base-change F α d = - is-closed-under-equiv-global-subuniverse 𝒫 (l1 ⊔ l2) (l3 ⊔ l4) - ( fiber f (map-codomain-cartesian-hom-arrow g f α d)) - ( fiber g d) - ( inv-equiv (equiv-fibers-cartesian-hom-arrow g f α d)) - ( F (map-codomain-cartesian-hom-arrow g f α d)) + is-local-map-base-change : + is-local-map f g → cartesian-hom-arrow g' g → is-local-map f g' + is-local-map-base-change G α d = + is-local-equiv f + ( equiv-fibers-cartesian-hom-arrow g' g α d) + ( G (map-codomain-cartesian-hom-arrow g' g α d)) +``` + +### `f`-local maps are closed under retracts + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} + {f : A → B} {g : C → D} {g' : E → F} + where + + is-local-retract-map : + is-local-map f g → g' retract-of-map g → is-local-map f g' + is-local-retract-map G R d = + is-local-retract + ( retract-fiber-retract-map g' g R d) + ( G (map-codomain-inclusion-retract-map g' g R d)) ``` ## See also 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 777b70dcbd..1b753c4353 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -165,6 +165,26 @@ module _ is-local-inv-equiv e = is-local-dependent-type-inv-fam-equiv f (λ _ → e) ``` +### Local types are closed under retracts + +```agda +module _ + {l1 l2 l3 l4 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} + {f : X → Y} + where + + is-local-retract : A retract-of B → is-local f B → is-local f A + is-local-retract R = + is-equiv-retract-map-is-equiv' + ( precomp f A) + ( precomp f B) + ( retract-postcomp Y R) + ( retract-postcomp X R) + ( refl-htpy) + ( refl-htpy) +``` + ### Locality is preserved by homotopies ```agda From cad7828ac168660c23cf4e85aac9419454930463 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 4 Oct 2024 19:40:19 +0200 Subject: [PATCH 14/19] a typo I found --- src/foundation/functoriality-cartesian-product-types.lagda.md | 2 +- .../types-local-at-maps.lagda.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/foundation/functoriality-cartesian-product-types.lagda.md b/src/foundation/functoriality-cartesian-product-types.lagda.md index 6b853ac770..db43a033d8 100644 --- a/src/foundation/functoriality-cartesian-product-types.lagda.md +++ b/src/foundation/functoriality-cartesian-product-types.lagda.md @@ -32,7 +32,7 @@ The **functorial action** of the `f : A → B` and `g : C → D` and returns a map ```text - f × g : A × B → C × D` + f × g : A × B → C × D ``` between the cartesian product types. This functorial action is _bifunctorial_ in 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 1b753c4353..6b4c1b5c99 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -295,7 +295,7 @@ module _ is-equiv-is-local-domains' (pr1 is-local-X) ``` -### Propositions are `f`-local if `_∘ f` has a converse +### Propositions are `f`-local if `- ∘ f` has a converse ```agda module _ From 95c4f0abe2b3c2d66a1e106a8cfbead18a4db08c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 4 Oct 2024 21:32:26 +0200 Subject: [PATCH 15/19] precomposition at a dependent pair type --- ...recomposition-dependent-functions.lagda.md | 37 +++++++++++++++++++ .../precomposition-functions.lagda.md | 33 +++++++++++++++++ ...sal-property-dependent-pair-types.lagda.md | 7 ++++ 3 files changed, 77 insertions(+) diff --git a/src/foundation/precomposition-dependent-functions.lagda.md b/src/foundation/precomposition-dependent-functions.lagda.md index 0e1b1294b1..b0eec54a25 100644 --- a/src/foundation/precomposition-dependent-functions.lagda.md +++ b/src/foundation/precomposition-dependent-functions.lagda.md @@ -10,6 +10,7 @@ open import foundation-core.precomposition-dependent-functions public ```agda open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types open import foundation.dependent-universal-property-equivalences open import foundation.function-extensionality open import foundation.universe-levels @@ -17,10 +18,12 @@ open import foundation.universe-levels open import foundation-core.commuting-squares-of-maps open import foundation-core.equivalences open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.truncated-maps open import foundation-core.truncation-levels +open import foundation-core.type-theoretic-principle-of-choice ```
@@ -120,3 +123,37 @@ is-trunc-map-succ-precomp-Π {k = k} {f = f} {C = C} H = ( funext (g ∘ f) (h ∘ f)) ( H g h)) ``` + +### The dependent precomposition map at a dependent pair type + +Given a map `f : X → Y` and a family `B : (y : Y) → A y → 𝒰` we have an +equivalence of maps + +```text + precomp-Π f (λ y → Σ (A y) (B y)) + ((y : Y) → Σ (A y) (B y)) -----------------------------> ((x : X) → Σ (A (f x)) (B (f x))) + | | + ~ | | ~ + ∨ ∨ + Σ (a : (y : Y) → A y) ((y : Y) → B y (a y)) --------> Σ (a : (x : X) → A (f x)) ((x : X) → B (f x) (a x)). + map-Σ (precomp-Π f A) (λ a → precomp-Π f (λ y → B y (a y))) +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + {X : UU l1} {Y : UU l2} {A : Y → UU l3} {B : (y : Y) → A y → UU l4} + {f : X → Y} + where + + coherence-precomp-Π-Σ : + coherence-square-maps + ( precomp-Π f (λ y → Σ (A y) (B y))) + ( map-distributive-Π-Σ) + ( map-distributive-Π-Σ) + ( map-Σ + ( λ a → (x : X) → B (f x) (a x)) + ( precomp-Π f A) + ( λ a → precomp-Π f (λ y → B y (a y)))) + coherence-precomp-Π-Σ = refl-htpy +``` diff --git a/src/foundation/precomposition-functions.lagda.md b/src/foundation/precomposition-functions.lagda.md index 720c665b0e..602beb37d6 100644 --- a/src/foundation/precomposition-functions.lagda.md +++ b/src/foundation/precomposition-functions.lagda.md @@ -26,6 +26,7 @@ open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.retractions +open import foundation-core.type-theoretic-principle-of-choice ```
@@ -213,3 +214,35 @@ module _ ( precomp-Π f (eq-value g h)) ( compute-htpy-eq-ap-precomp) ``` + +### The precomposition map at a dependent pair type + +Given a map `f : X → Y` and a family `B : A → 𝒰` we have an equivalence of maps + +```text + precomp f (Σ A B) + (Y → Σ A B) ------------------------------> (X → Σ A B) + | | + ~ | | ~ + ∨ ∨ + Σ (a : Y → A) ((y : Y) → B (a y)) --------> Σ (a : X → A) ((x : X) → B (a x)). + map-Σ (precomp f A) (λ a → precomp f (B ∘ a)) +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : A → UU l4} + {f : X → Y} + where + + coherence-precomp-Σ : + coherence-square-maps + ( precomp f (Σ A B)) + ( map-distributive-Π-Σ) + ( map-distributive-Π-Σ) + ( map-Σ + ( λ a → (x : X) → B (a x)) + ( precomp f A) + ( λ a → precomp-Π f (B ∘ a))) + coherence-precomp-Σ = coherence-precomp-Π-Σ +``` diff --git a/src/foundation/universal-property-dependent-pair-types.lagda.md b/src/foundation/universal-property-dependent-pair-types.lagda.md index 1d5d970795..54b12615b2 100644 --- a/src/foundation/universal-property-dependent-pair-types.lagda.md +++ b/src/foundation/universal-property-dependent-pair-types.lagda.md @@ -15,6 +15,8 @@ open import foundation-core.equivalences open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.retractions +open import foundation-core.sections ``` @@ -93,3 +95,8 @@ equiv-ev-pair³ {X = X} {Y = Y} {Z = Z} {U = U} {V = V} {W = W} = ( equiv-ev-pair) ( λ k → equiv-ev-pair²) ``` + +## See also + +- For the universal mapping-into property of dependent pair types, see the + [type theoretic principle of choice](foundation-core.type-theoretic-principle-of-choice.md) From f01308b2c0311678a19aa2a291f2e66e7fc1daa8 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 5 Oct 2024 17:29:47 +0200 Subject: [PATCH 16/19] Truncatedness of the base of a truncated dependent sum --- .../contractible-types.lagda.md | 18 ++++++++++++++ src/foundation-core/propositions.lagda.md | 19 +++++++++++++++ src/foundation-core/truncated-types.lagda.md | 19 +++++++++++++++ src/foundation/contractible-types.lagda.md | 8 +++---- src/foundation/inhabited-types.lagda.md | 24 +++++++++++++++++++ 5 files changed, 83 insertions(+), 5 deletions(-) diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md index 5e457cbe84..8b303ff4dd 100644 --- a/src/foundation-core/contractible-types.lagda.md +++ b/src/foundation-core/contractible-types.lagda.md @@ -133,6 +133,24 @@ module _ is-equiv-is-contr _ is-contr-A is-contr-B ``` +### Contractibility of the base of a contractible dependent sum + +Given a type `A` and a type family over it `B`, then if the dependent sum +`Σ A B` is contractible, it follows that if there is a section `(x : A) → B x` +then `A` is contractible. + +```agda +module _ + {l1 l2 : Level} (A : UU l1) (B : A → UU l2) + where + + abstract + is-contr-base-is-contr-Σ' : + ((x : A) → B x) → is-contr (Σ A B) → is-contr A + is-contr-base-is-contr-Σ' s = + is-contr-retract-of (Σ A B) ((λ a → a , s a) , pr1 , refl-htpy) +``` + ### Contractibility of cartesian product types Given two types `A` and `B`, the following are equivalent: diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md index 041ce6881d..005680a831 100644 --- a/src/foundation-core/propositions.lagda.md +++ b/src/foundation-core/propositions.lagda.md @@ -183,6 +183,25 @@ pr2 (Σ-Prop P Q) = ( λ p → is-prop-type-Prop (Q p)) ``` +### If `Σ A B` is a proposition and there is a section `(x : A) → B x` then `A` is a proposition + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (s : (x : A) → B x) + where + + is-proof-irrelevant-base-is-proof-irrelevant-Σ' : + is-proof-irrelevant (Σ A B) → is-proof-irrelevant A + is-proof-irrelevant-base-is-proof-irrelevant-Σ' H a = + is-contr-base-is-contr-Σ' A B s (H (a , s a)) + + is-prop-base-is-prop-Σ' : is-prop (Σ A B) → is-prop A + is-prop-base-is-prop-Σ' H = + is-prop-is-proof-irrelevant + ( is-proof-irrelevant-base-is-proof-irrelevant-Σ' + ( is-proof-irrelevant-is-prop H)) +``` + ### Propositions are closed under cartesian product types ```agda diff --git a/src/foundation-core/truncated-types.lagda.md b/src/foundation-core/truncated-types.lagda.md index ef0e87f4a0..fb88b4c3df 100644 --- a/src/foundation-core/truncated-types.lagda.md +++ b/src/foundation-core/truncated-types.lagda.md @@ -7,6 +7,7 @@ module foundation-core.truncated-types where
Imports ```agda +open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types @@ -217,6 +218,24 @@ fiber-Truncated-Type A B f b = Σ-Truncated-Type A (λ a → Id-Truncated-Type' B (f a) b) ``` +### Truncatedness of the base of a truncated dependent sum + +```agda +abstract + is-trunc-base-is-trunc-Σ' : + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : A → UU l2} → + ((x : A) → B x) → is-trunc k (Σ A B) → is-trunc k A + is-trunc-base-is-trunc-Σ' {k = neg-two-𝕋} {A} {B} = + is-contr-base-is-contr-Σ' A B + is-trunc-base-is-trunc-Σ' {k = succ-𝕋 k} s is-trunc-ΣAB x y = + is-trunc-base-is-trunc-Σ' + ( apd s) + ( is-trunc-equiv' k + ( (x , s x) ＝ (y , s y)) + ( equiv-pair-eq-Σ (x , s x) (y , s y)) + ( is-trunc-ΣAB (x , s x) (y , s y))) +``` + ### Products of truncated types are truncated ```agda diff --git a/src/foundation/contractible-types.lagda.md b/src/foundation/contractible-types.lagda.md index 21aa96f701..bfb117148d 100644 --- a/src/foundation/contractible-types.lagda.md +++ b/src/foundation/contractible-types.lagda.md @@ -157,11 +157,9 @@ module _ is-contr-Σ-is-prop : ((x : A) → is-prop (B x)) → ((x : A) → B x → a ＝ x) → is-contr (Σ A B) - pr1 (is-contr-Σ-is-prop p f) = pair a b - pr2 (is-contr-Σ-is-prop p f) (pair x y) = - eq-type-subtype - ( λ x' → pair (B x') (p x')) - ( f x y) + pr1 (is-contr-Σ-is-prop p f) = a , b + pr2 (is-contr-Σ-is-prop p f) (x , y) = + eq-type-subtype (λ x' → B x' , p x') (f x y) ``` ### The diagonal of contractible types diff --git a/src/foundation/inhabited-types.lagda.md b/src/foundation/inhabited-types.lagda.md index 28e0da41c8..93682e4ba5 100644 --- a/src/foundation/inhabited-types.lagda.md +++ b/src/foundation/inhabited-types.lagda.md @@ -7,9 +7,11 @@ module foundation.inhabited-types where
Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types +open import foundation.function-extensionality open import foundation.functoriality-propositional-truncation open import foundation.fundamental-theorem-of-identity-types open import foundation.propositional-truncations @@ -18,6 +20,7 @@ open import foundation.univalence open import foundation.universe-levels open import foundation-core.equivalences +open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.torsorial-type-families @@ -220,6 +223,27 @@ is-contr-is-inhabited-is-prop {A = A} p h = ( λ a → a , eq-is-prop' p a) ``` +### Contractibility of the base of a dependent sum + +Given a type `A` and a type family over it `B`, then if the dependent sum +`Σ A B` is contractible, it follows that if there merely exists a section +`(x : A) → B x`, then `A` is contractible. + +```agda +module _ + {l1 l2 : Level} (A : UU l1) (B : A → UU l2) + where + + abstract + is-contr-base-is-contr-Σ : + is-inhabited ((x : A) → B x) → is-contr (Σ A B) → is-contr A + is-contr-base-is-contr-Σ s is-contr-ΣAB = + rec-trunc-Prop + ( is-contr-Prop A) + ( λ s → is-contr-base-is-contr-Σ' A B s is-contr-ΣAB) + ( s) +``` + ## See also - The notion of _nonempty types_ is treated in From 9bf6b1d1d92dae3c9a8b427050cc4cb56b41f54d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 5 Oct 2024 17:29:56 +0200 Subject: [PATCH 17/19] =?UTF-8?q?The=20fibers=20of=20`map-=CE=A3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...unctoriality-dependent-pair-types.lagda.md | 96 ++++++++++++++++++- 1 file changed, 94 insertions(+), 2 deletions(-) diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md index 768597d72c..34d796290b 100644 --- a/src/foundation-core/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation-core/functoriality-dependent-pair-types.lagda.md @@ -7,7 +7,10 @@ module foundation-core.functoriality-dependent-pair-types where
Imports ```agda +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.contractible-maps @@ -21,7 +24,7 @@ open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.retractions open import foundation-core.retracts-of-types -open import foundation-core.transport-along-identifications +open import foundation-core.sections ```
@@ -305,6 +308,78 @@ module _ is-equiv-fiber-map-Σ-map-base-fiber t ``` +### The fibers of `map-Σ` + +We compute the fibers of `map-Σ` first in terms of `fiber'` and then in terms of +`fiber`. + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} (D : B → UU l4) + (f : A → B) (g : (x : A) → C x → D (f x)) (t : Σ B D) + where + + fiber-map-Σ' : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + fiber-map-Σ' = + Σ (fiber' f (pr1 t)) (λ s → fiber' (g (pr1 s)) (tr D (pr2 s) (pr2 t))) + + map-fiber-map-Σ' : fiber' (map-Σ D f g) t → fiber-map-Σ' + map-fiber-map-Σ' ((a , c) , refl) = (a , refl) , (c , refl) + + map-inv-fiber-map-Σ' : fiber-map-Σ' → fiber' (map-Σ D f g) t + map-inv-fiber-map-Σ' ((a , p) , (c , q)) = ((a , c) , eq-pair-Σ p q) + + abstract + is-section-map-inv-fiber-map-Σ' : + is-section map-fiber-map-Σ' map-inv-fiber-map-Σ' + is-section-map-inv-fiber-map-Σ' ((a , refl) , (c , refl)) = refl + + abstract + is-retraction-map-inv-fiber-map-Σ' : + is-retraction map-fiber-map-Σ' map-inv-fiber-map-Σ' + is-retraction-map-inv-fiber-map-Σ' ((a , c) , refl) = refl + + is-equiv-map-fiber-map-Σ' : is-equiv map-fiber-map-Σ' + is-equiv-map-fiber-map-Σ' = + is-equiv-is-invertible + map-inv-fiber-map-Σ' + is-section-map-inv-fiber-map-Σ' + is-retraction-map-inv-fiber-map-Σ' + + compute-fiber-map-Σ' : fiber' (map-Σ D f g) t ≃ fiber-map-Σ' + compute-fiber-map-Σ' = (map-fiber-map-Σ' , is-equiv-map-fiber-map-Σ') + + fiber-map-Σ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + fiber-map-Σ = + Σ (fiber f (pr1 t)) (λ s → fiber (g (pr1 s)) (inv-tr D (pr2 s) (pr2 t))) + + map-fiber-map-Σ : fiber (map-Σ D f g) t → fiber-map-Σ + map-fiber-map-Σ ((a , c) , refl) = (a , refl) , (c , refl) + + map-inv-fiber-map-Σ : fiber-map-Σ → fiber (map-Σ D f g) t + map-inv-fiber-map-Σ ((a , refl) , c , refl) = ((a , c) , refl) + + abstract + is-section-map-inv-fiber-map-Σ : + is-section map-fiber-map-Σ map-inv-fiber-map-Σ + is-section-map-inv-fiber-map-Σ ((a , refl) , (c , refl)) = refl + + abstract + is-retraction-map-inv-fiber-map-Σ : + is-retraction map-fiber-map-Σ map-inv-fiber-map-Σ + is-retraction-map-inv-fiber-map-Σ ((a , c) , refl) = refl + + is-equiv-map-fiber-map-Σ : is-equiv map-fiber-map-Σ + is-equiv-map-fiber-map-Σ = + is-equiv-is-invertible + map-inv-fiber-map-Σ + is-section-map-inv-fiber-map-Σ + is-retraction-map-inv-fiber-map-Σ + + compute-fiber-map-Σ : fiber (map-Σ D f g) t ≃ fiber-map-Σ + compute-fiber-map-Σ = (map-fiber-map-Σ , is-equiv-map-fiber-map-Σ) +``` + ### If `f : A → B` is a contractible map, then so is `map-Σ-map-base f C` ```agda @@ -455,10 +530,27 @@ module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where - compute-map-Σ-id : map-Σ B id (λ x → id) ~ id + compute-map-Σ-id : map-Σ B id (λ _ → id) ~ id compute-map-Σ-id = refl-htpy ``` +### `map-Σ` preserves composition of maps + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} + {A' : A → UU l4} {B' : B → UU l5} {C' : C → UU l6} + {f : A → B} {f' : (x : A) → A' x → B' (f x)} + {g : B → C} {g' : (y : B) → B' y → C' (g y)} + where + + preserves-comp-map-Σ : + map-Σ C' (g ∘ f) (λ x x' → g' (f x) (f' x x')) ~ + map-Σ C' g g' ∘ map-Σ B' f f' + preserves-comp-map-Σ = refl-htpy +``` + ## See also - Arithmetical laws involving dependent pair types are recorded in From bd935a4a902997cd91b3e3a7b1799754a8cba792 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 8 Oct 2024 21:47:41 +0200 Subject: [PATCH 18/19] rename to `separated-types-subuniverses` --- src/foundation.lagda.md | 2 +- ...g-extension-fundamental-theorem-of-identity-types.lagda.md | 4 ++-- ...iverses.lagda.md => separated-types-subuniverses.lagda.md} | 2 +- .../higher-modalities.lagda.md | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) rename src/foundation/{types-separated-at-subuniverses.lagda.md => separated-types-subuniverses.lagda.md} (96%) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 8fd21d45c8..ce75ebf9dd 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -422,7 +422,7 @@ open import foundation.type-arithmetic-empty-type public open import foundation.type-arithmetic-unit-type public open import foundation.type-duality public open import foundation.type-theoretic-principle-of-choice public -open import foundation.types-separated-at-subuniverses public +open import foundation.separated-types-subuniverses public open import foundation.unions-subtypes public open import foundation.uniqueness-image public open import foundation.uniqueness-quantification public diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index cd95331a10..e7b9cd4b70 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -31,7 +31,7 @@ open import foundation.surjective-maps open import foundation.truncated-maps open import foundation.truncated-types open import foundation.truncation-levels -open import foundation.types-separated-at-subuniverses +open import foundation.separated-types-subuniverses open import foundation.universe-levels ``` @@ -51,7 +51,7 @@ asserts that for any [subuniverse](foundation.subuniverses.md) `P`, and any i.e., a family of maps with [fibers](foundation-core.fibers-of-maps.md) in `P`. 2. The [total space](foundation.dependent-pair-types.md) `Σ A B` is - [`P`-separated](foundation.types-separated-at-subuniverses.md), i.e., its + [`P`-separated](foundation.separated-types-subuniverses.md), i.e., its [identity types](foundation-core.identity-types.md) are in `P`. In other words, the extended fundamental theorem of diff --git a/src/foundation/types-separated-at-subuniverses.lagda.md b/src/foundation/separated-types-subuniverses.lagda.md similarity index 96% rename from src/foundation/types-separated-at-subuniverses.lagda.md rename to src/foundation/separated-types-subuniverses.lagda.md index cfbe263171..cc812fa34d 100644 --- a/src/foundation/types-separated-at-subuniverses.lagda.md +++ b/src/foundation/separated-types-subuniverses.lagda.md @@ -1,7 +1,7 @@ # Types separated at subuniverses ```agda -module foundation.types-separated-at-subuniverses where +module foundation.separated-types-subuniverses where ```
Imports diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md index 15d064f720..4ad1fb0f7c 100644 --- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md @@ -48,7 +48,7 @@ this manner on the image of the modal unit, one recovers the defining map Lastly, higher modalities must also be **identity closed** in the sense that for every type `X` the identity types `(x' ＝ y')` are modal for all terms `x' y' : ○ X`. In other words, `○ X` is -[`○`-separated](foundation.types-separated-at-subuniverses.md). Because of this, +[`○`-separated](foundation.separated-types-subuniverses.md). Because of this, (small) higher modalities in their most general form only make sense for [locally small modal operators](orthogonal-factorization-systems.locally-small-modal-operators.md). From 1e7793bb32eb9ee5854b3fcde6297ce72c44754b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 8 Oct 2024 21:50:24 +0200 Subject: [PATCH 19/19] pre-commit --- src/foundation.lagda.md | 2 +- ...urg-extension-fundamental-theorem-of-identity-types.lagda.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index ce75ebf9dd..7ebd5c9d45 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -342,6 +342,7 @@ open import foundation.retracts-of-maps public open import foundation.retracts-of-types public open import foundation.russells-paradox public open import foundation.sections public +open import foundation.separated-types-subuniverses public open import foundation.sequences public open import foundation.sequential-limits public open import foundation.set-presented-types public @@ -422,7 +423,6 @@ open import foundation.type-arithmetic-empty-type public open import foundation.type-arithmetic-unit-type public open import foundation.type-duality public open import foundation.type-theoretic-principle-of-choice public -open import foundation.separated-types-subuniverses public open import foundation.unions-subtypes public open import foundation.uniqueness-image public open import foundation.uniqueness-quantification public diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md index e7b9cd4b70..912f7c20ac 100644 --- a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md @@ -26,12 +26,12 @@ open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.maps-in-subuniverses open import foundation.propositional-truncations +open import foundation.separated-types-subuniverses open import foundation.subuniverses open import foundation.surjective-maps open import foundation.truncated-maps open import foundation.truncated-types open import foundation.truncation-levels -open import foundation.separated-types-subuniverses open import foundation.universe-levels ```