diff --git a/.vscode/extensions.json b/.vscode/extensions.json index 4aa2074cc5..33c4abcc66 100644 --- a/.vscode/extensions.json +++ b/.vscode/extensions.json @@ -8,6 +8,8 @@ "fredrikbakke.agda-syntax", "github.vscode-pull-request-github", "ms-python.python", - "ms-python.vscode-pylance" + "ms-python.vscode-pylance", + "oderwat.indent-rainbow", + "brunnerh.insert-unicode" ] } diff --git a/.vscode/settings.json b/.vscode/settings.json index 70f8720278..c8c2fc7303 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,7 +1,20 @@ { + "json.schemaDownload.enable": true, + // UI settings "breadcrumbs.enabled": false, + "indentRainbow.indicatorStyle": "light", + "indentRainbow.updateDelay": 0, + + "task.problemMatchers.neverPrompt": { + "shell": true + }, + + "editor.unicodeHighlight.ambiguousCharacters": false, + "editor.unicodeHighlight.invisibleCharacters": true, + + // File nesting for agda auxillary files "explorer.fileNesting.enabled": true, "explorer.fileNesting.expand": false, "explorer.fileNesting.patterns": { @@ -11,6 +24,8 @@ }, // Snippet setup + "editor.inlineSuggest.enabled": true, + "editor.acceptSuggestionOnEnter": "off", "editor.snippetSuggestions": "top", "editor.wordBasedSuggestions": false, "javascript.suggest.names": false, @@ -23,6 +38,8 @@ "files.insertFinalNewline": true, "files.trimFinalNewlines": true, "files.trimTrailingWhitespace": true, + + // File specific "files.associations": { "*.agda": "agda", "*.lagda.md": "literate agda markdown" @@ -32,10 +49,11 @@ "editor.tabSize": 2, "editor.rulers": [80], "editor.quickSuggestions": { - "other": "inline" + "other": "on" }, "editor.autoClosingBrackets": "never" }, + "[css]": { "editor.quickSuggestions": { "other": true @@ -44,10 +62,12 @@ "gitlens.codeLens.scopes": ["document"], "editor.tabSize": 2 }, + "[javascript]": { "editor.maxTokenizationLineLength": 2500, "editor.tabSize": 2 }, + "[json][jsonc]": { "editor.quickSuggestions": { "strings": true @@ -55,14 +75,25 @@ "editor.suggest.insertMode": "replace", "gitlens.codeLens.scopes": ["document"] }, - "[markdown][literate agda markdown]": { + + "[literate agda markdown]": { "editor.tabSize": 2, "editor.rulers": [80], "editor.quickSuggestions": { - "other": "inline" + "other": "on" }, "editor.autoClosingBrackets": "never" }, + + "[markdown]": { + "editor.tabSize": 2, + "editor.rulers": [80], + "editor.quickSuggestions": { + "other": "on" + }, + "editor.autoClosingBrackets": "never" + }, + "[python]": { "editor.tabSize": 4, "editor.defaultFormatter": "ms-python.python" diff --git a/.vscode/tasks.json b/.vscode/tasks.json index b46cb0f5cd..9962d1e72c 100644 --- a/.vscode/tasks.json +++ b/.vscode/tasks.json @@ -17,12 +17,24 @@ "args": ["pre-commit"], "problemMatcher": [] }, + { + "label": "remove-unused-imports", + "detail": "Search for and remove unused imports", + "type": "shell", + "command": "python", + "args": ["${workspaceFolder}/scripts/remove_unused_imports.py"], + "problemMatcher": [], + "hide": true + }, { "label": "unused-imports", "detail": "Search for and remove unused imports. Very slow!", "type": "shell", - "command": "python scripts/remove_unused_imports.py && python scripts/demote_foundation_imports.py", - "problemMatcher": [] + "command": "python", + "args": ["${workspaceFolder}/scripts/demote_foundation_imports.py"], + "problemMatcher": [], + "dependsOn": "remove-unused-imports" } - ] + ], + "statusbar.default.hide": false } diff --git a/DESIGN-PRINCIPLES.md b/DESIGN-PRINCIPLES.md index 829eb8b107..fa6ec73c0b 100644 --- a/DESIGN-PRINCIPLES.md +++ b/DESIGN-PRINCIPLES.md @@ -34,16 +34,14 @@ makes use of several postulates. Note that there is some redundancy in the postulates we assume. For example, the [univalence axiom implies function extensionality](https://unimath.github.io/agda-unimath/foundation.univalence-implies-function-extensionality.html), -but we still assume function extensionality separately. Furthermore, The -interval type is contractible, so there is no need at all to postulate it. The -circle can be constructed as the type of `ℤ`-torsors, and the replacement axiom -can be used to prove there is a circle in `UU lzero`. Adittionally, the -replacement axiom can be proven by the join construction, which only uses -pushouts. Finally, the Agda built-in types do not change the semantics of the -theory, they only give convenience to the user of the library. - -We also note that the higher inductive types in the `agda-unimath` library only -have computation rules up to identification. +but we still assume function extensionality separately. Furthermore, +[the interval type is contractible](synthetic-homotopy-theory.interval-type.md), +and the higher inductive types in the `agda-unimath` library only have +computation rules up to identification, so there is no need at all to postulate +it. The circle can be constructed as the type of `ℤ`-torsors, and the +replacement axiom can be used to prove there is a circle in `UU lzero`. +Additionally, the replacement axiom can be proven by the join construction, +which only uses pushouts. With these postulates, the `agda-unimath` library is a library for constructive univalent mathematics. Mathematics for which the law of excluded middle or the diff --git a/src/category-theory/yoneda-lemma-precategories.lagda.md b/src/category-theory/yoneda-lemma-precategories.lagda.md index e813ef6033..f4225afd35 100644 --- a/src/category-theory/yoneda-lemma-precategories.lagda.md +++ b/src/category-theory/yoneda-lemma-precategories.lagda.md @@ -1,4 +1,4 @@ -# Yoneda lemma for precategories +# The Yoneda lemma for precategories ```agda module category-theory.yoneda-lemma-precategories where diff --git a/src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md b/src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md index 0a8fbdb39e..cd021def78 100644 --- a/src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md @@ -1,4 +1,4 @@ -# The groups ℤ/kℤ +# The groups `ℤ/kℤ` ```agda module elementary-number-theory.groups-of-modular-arithmetic where diff --git a/src/elementary-number-theory/powers-of-two.lagda.md b/src/elementary-number-theory/powers-of-two.lagda.md index ca73b53c07..ea4ff09ee9 100644 --- a/src/elementary-number-theory/powers-of-two.lagda.md +++ b/src/elementary-number-theory/powers-of-two.lagda.md @@ -1,4 +1,4 @@ -# Powers of Two +# Powers of two ```agda module elementary-number-theory.powers-of-two where diff --git a/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md b/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md index 263e61843e..881fdf9f1b 100644 --- a/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/well-ordering-principle-standard-finite-types.lagda.md @@ -1,4 +1,4 @@ -# The Well-Ordering Principle of the standard finite types +# The well-ordering principle of the standard finite types ```agda module elementary-number-theory.well-ordering-principle-standard-finite-types where @@ -47,7 +47,7 @@ open import univalent-combinatorics.standard-finite-types ## Idea The standard finite types inherit a well-ordering principle from the natural -numbers +numbers. ## Properties @@ -187,7 +187,7 @@ well-ordering-principle-∃-Fin k P H = ( is-decidable-decidable-subtype P)) ``` -### Hilbert's epsilon operator for decidable subtypes of standard finite types +### Hilbert's `ε`-operator for decidable subtypes of standard finite types ```agda ε-operator-decidable-subtype-Fin : diff --git a/src/finite-group-theory/abstract-quaternion-group.lagda.md b/src/finite-group-theory/abstract-quaternion-group.lagda.md index b2e559adfe..1561fb5510 100644 --- a/src/finite-group-theory/abstract-quaternion-group.lagda.md +++ b/src/finite-group-theory/abstract-quaternion-group.lagda.md @@ -1,4 +1,4 @@ -# The abstract quaternion group of order 8 +# The abstract quaternion group of order `8` ```agda module finite-group-theory.abstract-quaternion-group where diff --git a/src/finite-group-theory/concrete-quaternion-group.lagda.md b/src/finite-group-theory/concrete-quaternion-group.lagda.md index 8cf9ae46c3..e6839fd7e9 100644 --- a/src/finite-group-theory/concrete-quaternion-group.lagda.md +++ b/src/finite-group-theory/concrete-quaternion-group.lagda.md @@ -82,53 +82,53 @@ equiv-face-cube k X Y e d a = ( inclusion-complement-point-UU-Fin k ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d'))) -cube-with-labelled-faces : +cube-with-labeled-faces : (k : ℕ) → UU (lsuc lzero) -cube-with-labelled-faces k = +cube-with-labeled-faces k = Σ ( cube (succ-ℕ k)) ( λ X → (d : dim-cube (succ-ℕ k) X) (a : axis-cube (succ-ℕ k) X d) → labelling-cube k (face-cube k X d a)) -cube-cube-with-labelled-faces : - (k : ℕ) → cube-with-labelled-faces k → cube (succ-ℕ k) -cube-cube-with-labelled-faces k X = pr1 X +cube-cube-with-labeled-faces : + (k : ℕ) → cube-with-labeled-faces k → cube (succ-ℕ k) +cube-cube-with-labeled-faces k X = pr1 X -labelling-faces-cube-with-labelled-faces : - (k : ℕ) (X : cube-with-labelled-faces k) - (d : dim-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X)) - (a : axis-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X) d) → - labelling-cube k (face-cube k (cube-cube-with-labelled-faces k X) d a) -labelling-faces-cube-with-labelled-faces k X = pr2 X +labelling-faces-cube-with-labeled-faces : + (k : ℕ) (X : cube-with-labeled-faces k) + (d : dim-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X)) + (a : axis-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X) d) → + labelling-cube k (face-cube k (cube-cube-with-labeled-faces k X) d a) +labelling-faces-cube-with-labeled-faces k X = pr2 X {- -standard-cube-with-labelled-faces : - (k : ℕ) → cube-with-labelled-faces k -standard-cube-with-labelled-faces k = +standard-cube-with-labeled-faces : + (k : ℕ) → cube-with-labeled-faces k +standard-cube-with-labeled-faces k = pair ( standard-cube (succ-ℕ k)) ( λ d a → {!!}) -} -equiv-cube-with-labelled-faces : - {k : ℕ} (X Y : cube-with-labelled-faces k) → UU lzero -equiv-cube-with-labelled-faces {k} X Y = +equiv-cube-with-labeled-faces : + {k : ℕ} (X Y : cube-with-labeled-faces k) → UU lzero +equiv-cube-with-labeled-faces {k} X Y = Σ ( equiv-cube (succ-ℕ k) - ( cube-cube-with-labelled-faces k X) - ( cube-cube-with-labelled-faces k Y)) - ( λ e → ( d : dim-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X)) - ( a : axis-cube (succ-ℕ k) (cube-cube-with-labelled-faces k X) d) → + ( cube-cube-with-labeled-faces k X) + ( cube-cube-with-labeled-faces k Y)) + ( λ e → ( d : dim-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X)) + ( a : axis-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X) d) → htpy-equiv-cube k ( standard-cube k) ( face-cube k - ( cube-cube-with-labelled-faces k Y) + ( cube-cube-with-labeled-faces k Y) ( map-dim-equiv-cube (succ-ℕ k) - ( cube-cube-with-labelled-faces k X) - ( cube-cube-with-labelled-faces k Y) + ( cube-cube-with-labeled-faces k X) + ( cube-cube-with-labeled-faces k Y) ( e) ( d)) ( map-axis-equiv-cube (succ-ℕ k) - ( cube-cube-with-labelled-faces k X) - ( cube-cube-with-labelled-faces k Y) + ( cube-cube-with-labeled-faces k X) + ( cube-cube-with-labeled-faces k Y) e d a)) ( comp-equiv-cube k ( standard-cube k) @@ -137,14 +137,14 @@ equiv-cube-with-labelled-faces {k} X Y = ( map-dim-equiv-cube (succ-ℕ k) (pr1 X) (pr1 Y) e d) ( map-axis-equiv-cube (succ-ℕ k) (pr1 X) (pr1 Y) e d a)) ( equiv-face-cube k (pr1 X) (pr1 Y) e d a) - ( labelling-faces-cube-with-labelled-faces k X d a)) - ( labelling-faces-cube-with-labelled-faces k Y + ( labelling-faces-cube-with-labeled-faces k X d a)) + ( labelling-faces-cube-with-labeled-faces k Y ( map-dim-equiv-cube (succ-ℕ k) - ( cube-cube-with-labelled-faces k X) - ( cube-cube-with-labelled-faces k Y) + ( cube-cube-with-labeled-faces k X) + ( cube-cube-with-labeled-faces k Y) e d) ( map-axis-equiv-cube (succ-ℕ k) - ( cube-cube-with-labelled-faces k X) - ( cube-cube-with-labelled-faces k Y) + ( cube-cube-with-labeled-faces k X) + ( cube-cube-with-labeled-faces k Y) e d a))) ``` diff --git a/src/finite-group-theory/groups-of-order-2.lagda.md b/src/finite-group-theory/groups-of-order-2.lagda.md index 6265b2b07a..68093c0e66 100644 --- a/src/finite-group-theory/groups-of-order-2.lagda.md +++ b/src/finite-group-theory/groups-of-order-2.lagda.md @@ -1,4 +1,4 @@ -# Groups of order 2 +# Groups of order `2` ```agda {-# OPTIONS --lossy-unification #-} diff --git a/src/finite-group-theory/tetrahedra-in-3-space.lagda.md b/src/finite-group-theory/tetrahedra-in-3-space.lagda.md index 825282fc70..13679635fa 100644 --- a/src/finite-group-theory/tetrahedra-in-3-space.lagda.md +++ b/src/finite-group-theory/tetrahedra-in-3-space.lagda.md @@ -1,4 +1,4 @@ -# Tetrahedra in 3-dimensional space +# Tetrahedra in `3`-dimensional space ```agda module finite-group-theory.tetrahedra-in-3-space where diff --git a/src/foundation-core/1-types.lagda.md b/src/foundation-core/1-types.lagda.md index ddc5b7a9ab..f38795650c 100644 --- a/src/foundation-core/1-types.lagda.md +++ b/src/foundation-core/1-types.lagda.md @@ -1,4 +1,4 @@ -# 1-Types +# `1`-Types ```agda module foundation-core.1-types where diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md index fd7a4fe7ff..edbc7d158b 100644 --- a/src/foundation-core/homotopies.lagda.md +++ b/src/foundation-core/homotopies.lagda.md @@ -31,6 +31,7 @@ module _ eq-value : X → UU l2 eq-value x = (f x ＝ g x) + {-# INLINE eq-value #-} map-compute-path-over-eq-value : {x y : X} (p : x ＝ y) (q : eq-value x) (r : eq-value y) → diff --git a/src/foundation-core/path-split-maps.lagda.md b/src/foundation-core/path-split-maps.lagda.md index 56a34e9152..c594e7037f 100644 --- a/src/foundation-core/path-split-maps.lagda.md +++ b/src/foundation-core/path-split-maps.lagda.md @@ -22,10 +22,13 @@ open import foundation-core.sections ## Idea -A map `f : A → B` is said to be path split if it has a section and its action on -identity types `Id x y → Id (f x) (f y)` has a section for each `x y : A`. By -the fundamental theorem for identity types, it follows that a map is path-split -if and only if it is an equivalence. +A map `f : A → B` is said to be **path split** if it has a +[section](foundation-core.sections.md) and its action on +[identity types](foundation-core.identity-types.md) `Id x y → Id (f x) (f y)` +has a section for each `x y : A`. By the +[fundamental theorem of identity types](foundation-core.fundamental-theorem-of-identity-types.md), +it follows that a map is path-split if and only if it is an +[equivalence](foundation-core.equivalences.md). ## Definition @@ -90,3 +93,13 @@ module _ [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md). - For the notion of maps with contractible fibers see [`foundation.contractible-maps`](foundation.contractible-maps.md). + +## References + +- Univalent Foundations Project, _Homotopy Type Theory – Univalent Foundations + of Mathematics_ (2013) (, + [arXiv:1308.0729](https://arxiv.org/abs/1308.0729), + [DOI:10.48550](https://doi.org/10.48550/arXiv.1308.0729)) +- Mike Shulman, _Universal properties without function extensionality_ + (November 2014) + ([HoTT Blog](https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/)) diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md index 159ddfde16..f3d747ffd1 100644 --- a/src/foundation-core/propositions.lagda.md +++ b/src/foundation-core/propositions.lagda.md @@ -277,7 +277,7 @@ abstract is-prop-function-type : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-prop B → is-prop (A → B) - is-prop-function-type H = is-prop-Π (λ x → H) + is-prop-function-type H = is-prop-Π (λ _ → H) type-function-Prop : {l1 l2 : Level} → UU l1 → Prop l2 → UU (l1 ⊔ l2) diff --git a/src/foundation-core/universal-property-truncation.lagda.md b/src/foundation-core/universal-property-truncation.lagda.md index 264893bda5..8acb122ef9 100644 --- a/src/foundation-core/universal-property-truncation.lagda.md +++ b/src/foundation-core/universal-property-truncation.lagda.md @@ -28,10 +28,10 @@ open import foundation-core.truncation-levels ## Idea -We say that a map `f : A → B` into a `k`-truncated type `B` is a `k`-truncation -of `A` -- or that it satisfies the universal property of the `k`-truncation of -`A` -- if any map `g : A → C` into a `k`-truncated type `C` extends uniquely -along `f` to a map `B → C`. +We say that a map `f : A → B` into a `k`-truncated type `B` is a +**`k`-truncation** of `A` -- or that it **satisfies the universal property of +the `k`-truncation** of `A` -- if any map `g : A → C` into a `k`-truncated type +`C` extends uniquely along `f` to a map `B → C`. ## Definition @@ -99,7 +99,7 @@ dependent-universal-property-truncation l {k} B f = abstract is-truncation-id : {l1 : Level} {k : 𝕋} {A : UU l1} (H : is-trunc k A) → - {l : Level} → is-truncation l (pair A H) id + {l : Level} → is-truncation l (A , H) id is-truncation-id H B = is-equiv-precomp-is-equiv id is-equiv-id (type-Truncated-Type B) @@ -204,5 +204,5 @@ module _ ( map-inv-is-equiv ( dependent-universal-property-truncation-is-truncation H ( fib-Truncated-Type C B g)) - ( λ a → pair (h a) (inv (K a)))) + ( λ a → h a , inv (K a))) ``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 7618c795e2..63281c26c7 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -82,6 +82,7 @@ open import foundation.discrete-sigma-decompositions public open import foundation.discrete-types public open import foundation.disjunction public open import foundation.double-negation public +open import foundation.double-negation-modality public open import foundation.double-powersets public open import foundation.dubuc-penon-compact-types public open import foundation.effective-maps-equivalence-relations public @@ -252,6 +253,7 @@ open import foundation.truncated-types public open import foundation.truncation-equivalences public open import foundation.truncation-images-of-maps public open import foundation.truncation-levels public +open import foundation.truncation-modalities public open import foundation.truncations public open import foundation.tuples-of-types public open import foundation.type-arithmetic-booleans public diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md index c5444621bf..b52ec830be 100644 --- a/src/foundation/0-connected-types.lagda.md +++ b/src/foundation/0-connected-types.lagda.md @@ -1,4 +1,4 @@ -# 0-Connected types +# `0`-Connected types ```agda module foundation.0-connected-types where diff --git a/src/foundation/0-images-of-maps.lagda.md b/src/foundation/0-images-of-maps.lagda.md index 611cf6cdc0..7bc34f1213 100644 --- a/src/foundation/0-images-of-maps.lagda.md +++ b/src/foundation/0-images-of-maps.lagda.md @@ -1,4 +1,4 @@ -# 0-Images of maps +# `0`-Images of maps ```agda module foundation.0-images-of-maps where diff --git a/src/foundation/0-maps.lagda.md b/src/foundation/0-maps.lagda.md index 7515655e6a..a49905c877 100644 --- a/src/foundation/0-maps.lagda.md +++ b/src/foundation/0-maps.lagda.md @@ -1,4 +1,4 @@ -# 0-Maps +# `0`-Maps ```agda module foundation.0-maps where diff --git a/src/foundation/1-types.lagda.md b/src/foundation/1-types.lagda.md index dda1ff537f..818c5c150e 100644 --- a/src/foundation/1-types.lagda.md +++ b/src/foundation/1-types.lagda.md @@ -1,4 +1,4 @@ -# 1-Types +# `1`-Types ```agda module foundation.1-types where diff --git a/src/foundation/2-types.lagda.md b/src/foundation/2-types.lagda.md index 1c2182a2eb..38ceb424c1 100644 --- a/src/foundation/2-types.lagda.md +++ b/src/foundation/2-types.lagda.md @@ -1,4 +1,4 @@ -# 2-Types +# `2`-Types ```agda module foundation.2-types where diff --git a/src/foundation/commuting-3-simplices-of-homotopies.lagda.md b/src/foundation/commuting-3-simplices-of-homotopies.lagda.md index ea13bcc60e..a8526a4385 100644 --- a/src/foundation/commuting-3-simplices-of-homotopies.lagda.md +++ b/src/foundation/commuting-3-simplices-of-homotopies.lagda.md @@ -1,4 +1,4 @@ -# Commuting 3-simplices of homotopies +# Commuting `3`-simplices of homotopies ```agda {-# OPTIONS --safe #-} diff --git a/src/foundation/commuting-3-simplices-of-maps.lagda.md b/src/foundation/commuting-3-simplices-of-maps.lagda.md index 610a6d7ca7..fb0fe06cd6 100644 --- a/src/foundation/commuting-3-simplices-of-maps.lagda.md +++ b/src/foundation/commuting-3-simplices-of-maps.lagda.md @@ -1,4 +1,4 @@ -# Commuting 3-simplices of maps +# Commuting `3`-simplices of maps ```agda {-# OPTIONS --safe #-} diff --git a/src/foundation/commuting-squares-of-identifications.lagda.md b/src/foundation/commuting-squares-of-identifications.lagda.md index 1bf389320e..268f0de8b7 100644 --- a/src/foundation/commuting-squares-of-identifications.lagda.md +++ b/src/foundation/commuting-squares-of-identifications.lagda.md @@ -31,9 +31,9 @@ A square of identifications bottom ``` -is said to _commute_ if there is an identification -`left ∙ bottom ＝ top ∙ right`. Such an identification may be called a -_coherence_ of the square. +is said to **commute** if there is an identification +`left ∙ bottom ＝ top ∙ right`. Such an identification is called a **coherence** +of the square. ## Definition diff --git a/src/foundation/dependent-binomial-theorem.lagda.md b/src/foundation/dependent-binomial-theorem.lagda.md index ed58754757..4c322b638d 100644 --- a/src/foundation/dependent-binomial-theorem.lagda.md +++ b/src/foundation/dependent-binomial-theorem.lagda.md @@ -1,4 +1,4 @@ -# The dependent binomial theorem for types (Distributivity of dependent function types over coproduct types) +# The dependent binomial theorem for types (distributivity of dependent function types over coproduct types) ```agda module foundation.dependent-binomial-theorem where diff --git a/src/foundation/dependent-paths.lagda.md b/src/foundation/dependent-paths.lagda.md index 9af20ccccf..c31068e535 100644 --- a/src/foundation/dependent-paths.lagda.md +++ b/src/foundation/dependent-paths.lagda.md @@ -1,9 +1,5 @@ # Dependent paths -We characterize dependent paths in the family of depedent paths; define the -groupoidal operators on dependent paths; define the cohrences paths: prove the -operators are equivalences. - ```agda module foundation.dependent-paths where ``` @@ -23,6 +19,14 @@ open import foundation-core.homotopies +## Idea + +We characterize dependent paths in the family of depedent paths; define the +groupoidal operators on dependent paths; define the cohrences paths: prove the +operators are equivalences. + +## Properites + We characterize dependent paths in the family `λ t → path-over B t b0 b1`. ```agda diff --git a/src/foundation/discrete-sigma-decompositions.lagda.md b/src/foundation/discrete-sigma-decompositions.lagda.md index 4055e60dce..e2e7b31740 100644 --- a/src/foundation/discrete-sigma-decompositions.lagda.md +++ b/src/foundation/discrete-sigma-decompositions.lagda.md @@ -1,4 +1,4 @@ -# Discrete Σ-Decompositions +# Discrete Σ-decompositions ```agda module foundation.discrete-sigma-decompositions where diff --git a/src/foundation/double-negation-modality.lagda.md b/src/foundation/double-negation-modality.lagda.md new file mode 100644 index 0000000000..2037c15e0d --- /dev/null +++ b/src/foundation/double-negation-modality.lagda.md @@ -0,0 +1,72 @@ +# The double negation modality + +```agda +module foundation.double-negation-modality where +``` + +
Imports + +```agda +open import foundation.double-negation +open import foundation.functions +open import foundation.universe-levels + +open import foundation-core.identity-types +open import foundation-core.propositions + +open import orthogonal-factorization-systems.local-types +open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.uniquely-eliminating-modalities +``` + +
+ +## Idea + +The [double negation](foundation.double-negation.md) operation `¬¬` is a +[modality](orthogonal-factorization-systems.higher-modalities.md). + +## Definition + +```agda +operator-double-negation-modality : + (l : Level) → operator-modality l l +operator-double-negation-modality _ = ¬¬ + +unit-double-negation-modality : + {l : Level} → unit-modality (operator-double-negation-modality l) +unit-double-negation-modality = intro-double-negation +``` + +## Properties + +### The double negation modality is a uniquely eliminating modality + +```agda +is-uniquely-eliminating-modality-double-negation-modality : + {l : Level} → + is-uniquely-eliminating-modality (unit-double-negation-modality {l}) +is-uniquely-eliminating-modality-double-negation-modality {l} A P = + is-local-family-is-prop + ( unit-double-negation-modality) + ( operator-double-negation-modality l ∘ P) + ( λ _ → is-prop-double-negation) + ( λ f z g → + double-negation-extend + ( λ (a : A) → + tr + ( ¬¬ ∘ P) + ( eq-is-prop is-prop-double-negation) + ( f a)) + ( z) + ( g)) +``` + +This proof follows Example 1.9 in _Modalities in homotopy type theory_. + +## References + +- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type + theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020 + ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526), + [doi:10.23638](https://doi.org/10.23638/LMCS-16%281%3A2%292020)) diff --git a/src/foundation/double-negation.lagda.md b/src/foundation/double-negation.lagda.md index 645301205d..7fea292347 100644 --- a/src/foundation/double-negation.lagda.md +++ b/src/foundation/double-negation.lagda.md @@ -57,22 +57,26 @@ double-negation-Prop' A = neg-Prop' (¬ A) double-negation-Prop : {l : Level} (P : Prop l) → Prop l double-negation-Prop P = double-negation-Prop' (type-Prop P) + +is-prop-double-negation : + {l : Level} {A : UU l} → is-prop (¬¬ A) +is-prop-double-negation = is-prop-neg ``` ### Double negations of classical laws ```agda -double-negation-double-negation-elim : {l : Level} {P : UU l} → ¬¬ (¬¬ P → P) +double-negation-double-negation-elim : + {l : Level} {P : UU l} → ¬¬ (¬¬ P → P) double-negation-double-negation-elim {P = P} f = ( λ (np : ¬ P) → f (λ (nnp : ¬¬ P) → ex-falso (nnp np))) - ( λ (p : P) → f (λ (nnp : ¬¬ P) → p)) + ( λ (p : P) → f (λ (nnp : ¬¬ P) → p)) double-negation-Peirces-law : - {l1 l2 : Level} {P : UU l1} {Q : UU l2} → - ¬¬ (((P → Q) → P) → P) -double-negation-Peirces-law {P = P} {Q} f = + {l1 l2 : Level} {P : UU l1} {Q : UU l2} → ¬¬ (((P → Q) → P) → P) +double-negation-Peirces-law {P = P} f = ( λ (np : ¬ P) → f (λ h → h (λ p → ex-falso (np p)))) - ( λ (p : P) → f (λ h → p)) + ( λ (p : P) → f (λ _ → p)) double-negation-linearity-implication : {l1 l2 : Level} {P : UU l1} {Q : UU l2} → @@ -80,8 +84,7 @@ double-negation-linearity-implication : double-negation-linearity-implication {P = P} {Q = Q} f = ( λ (np : ¬ P) → map-neg (inl {A = P → Q} {B = Q → P}) f (λ p → ex-falso (np p))) - ( λ (p : P) → - map-neg (inr {A = P → Q} {B = Q → P}) f (λ q → p)) + ( λ (p : P) → map-neg (inr {A = P → Q} {B = Q → P}) f (λ _ → p)) ``` ### Cases of double negation elimination @@ -125,7 +128,7 @@ double-negation-extend {P = P} {Q = Q} f = double-negation-elim-neg (¬ Q) ∘ (map-double-negation f) ``` -### A double negation of a type is logially equivalent to the double negation of its propositional truncation +### The double negation of a type is logically equivalent to the double negation of its propositional truncation ```agda abstract diff --git a/src/foundation/equivalences-maybe.lagda.md b/src/foundation/equivalences-maybe.lagda.md index 24360563fa..82a608655a 100644 --- a/src/foundation/equivalences-maybe.lagda.md +++ b/src/foundation/equivalences-maybe.lagda.md @@ -1,4 +1,4 @@ -# Equivalences on Maybe +# Equivalences on `Maybe` ```agda module foundation.equivalences-maybe where diff --git a/src/foundation/hilberts-epsilon-operators.lagda.md b/src/foundation/hilberts-epsilon-operators.lagda.md index 9ed96c4e0d..da62df48e8 100644 --- a/src/foundation/hilberts-epsilon-operators.lagda.md +++ b/src/foundation/hilberts-epsilon-operators.lagda.md @@ -1,4 +1,4 @@ -# Hilbert's ε-operators +# Hilbert's `ε`-operators ```agda module foundation.hilberts-epsilon-operators where @@ -19,8 +19,8 @@ open import foundation-core.equivalences ## Idea -Hilbert's ε-operator at a type `A` is a map `type-trunc-Prop A → A`. Contrary to -Hilbert, we will not assume that such an operator exists for each type `A`. +Hilbert's $ε$-operator at a type `A` is a map `type-trunc-Prop A → A`. Contrary +to Hilbert, we will not assume that such an operator exists for each type `A`. ## Definition @@ -31,7 +31,7 @@ Hilbert, we will not assume that such an operator exists for each type `A`. ## Properties -### The existence of Hilbert's ε-operators is invariant under equivalences +### The existence of Hilbert's `ε`-operators is invariant under equivalences ```agda ε-operator-equiv : diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index ade1454bcb..5f3d798848 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -184,5 +184,5 @@ module _ equiv-tr-refl : {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x : A} → equiv-tr B refl ＝ id-equiv {A = B x} -equiv-tr-refl B = eq-htpy-equiv λ x → refl +equiv-tr-refl B = eq-htpy-equiv (λ _ → refl) ``` diff --git a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md index a97ed1c165..00a5c2eb60 100644 --- a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md +++ b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md @@ -22,14 +22,12 @@ open import univalent-combinatorics.standard-finite-types -## Idea +## Statement -The lesser limited principle of omniscience asserts that for any sequence +The **lesser limited principle of omniscience** asserts that for any sequence `f : ℕ → Fin 2` containing at most one `1`, either `f n ＝ 0` for all even `n` or `f n ＝ 0` for all odd `n`. -## Definition - ```agda LLPO : UU lzero LLPO = @@ -42,3 +40,9 @@ LLPO = ( λ n → function-Prop (is-odd-ℕ n) (Id-Prop (Fin-Set 2) (f n) (zero-Fin 1)))) ``` + +## See also + +- [The principle of omniscience](foundation.principle-of-omniscience.md) +- [The limited principle of omniscience](foundation.limited-principle-of-omniscience.md) +- [The weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md) diff --git a/src/foundation/limited-principle-of-omniscience.lagda.md b/src/foundation/limited-principle-of-omniscience.lagda.md index fcf98e1c1f..522b3b2fae 100644 --- a/src/foundation/limited-principle-of-omniscience.lagda.md +++ b/src/foundation/limited-principle-of-omniscience.lagda.md @@ -1,4 +1,4 @@ -# The limited principle of omniscience (LPO) +# The limited principle of omniscience ```agda module foundation.limited-principle-of-omniscience where @@ -22,14 +22,12 @@ open import univalent-combinatorics.standard-finite-types -## Idea +## Statement -The **Limited Principle of Omniscience** asserts that for every sequence -`f : ℕ → Fin 2` either there exists an `n` such that `f n ＝ 1` or for all `n` +The **limited principle of omniscience** (LPO) asserts that for every sequence +`f : ℕ → Fin 2` there either exists an `n` such that `f n ＝ 1` or for all `n` we have `f n ＝ 0`. -## Definition - ```agda LPO : UU lzero LPO = @@ -38,3 +36,9 @@ LPO = ( ∃-Prop ℕ (λ n → f n ＝ one-Fin 1)) ( Π-Prop ℕ (λ n → Id-Prop (Fin-Set 2) (f n) (zero-Fin 1))) ``` + +## See also + +- [The principle of omniscience](foundation.principle-of-omniscience.md) +- [The lesser limited principle of omniscience](foundation.lesser-limited-principle-of-omniscience.md) +- [The weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md) diff --git a/src/foundation/locally-small-types.lagda.md b/src/foundation/locally-small-types.lagda.md index 8c545e6e7b..e91b06070b 100644 --- a/src/foundation/locally-small-types.lagda.md +++ b/src/foundation/locally-small-types.lagda.md @@ -9,6 +9,7 @@ module foundation.locally-small-types where ```agda open import foundation.dependent-pair-types open import foundation.function-extensionality +open import foundation.functions open import foundation.inhabited-subtypes open import foundation.subuniverses open import foundation.univalence @@ -73,14 +74,21 @@ pr1 (is-locally-small-Prop l A) = is-locally-small l A pr2 (is-locally-small-Prop l A) = is-prop-is-locally-small l A ``` +### Any type in `UU l` is `l`-locally small + +```agda +is-locally-small' : {l : Level} {A : UU l} → is-locally-small l A +is-locally-small' x y = is-small' +``` + ### Any small type is locally small ```agda is-locally-small-is-small : {l l1 : Level} {A : UU l1} → is-small l A → is-locally-small l A -pr1 (is-locally-small-is-small (pair X e) x y) = +pr1 (is-locally-small-is-small (X , e) x y) = map-equiv e x ＝ map-equiv e y -pr2 (is-locally-small-is-small (pair X e) x y) = equiv-ap e x y +pr2 (is-locally-small-is-small (X , e) x y) = equiv-ap e x y ``` ### Any proposition is locally small @@ -107,24 +115,24 @@ is-locally-small-Σ : {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} → is-locally-small l3 A → ((x : A) → is-locally-small l4 (B x)) → is-locally-small (l3 ⊔ l4) (Σ A B) -is-locally-small-Σ H K x y = +is-locally-small-Σ {B = B} H K x y = is-small-equiv ( Eq-Σ x y) ( equiv-pair-eq-Σ x y) ( is-small-Σ ( H (pr1 x) (pr1 y)) - ( λ p → K (pr1 y) (tr _ p (pr2 x)) (pr2 y))) + ( λ p → K (pr1 y) (tr B p (pr2 x)) (pr2 y))) Σ-Locally-Small-Type : {l1 l2 l3 l4 : Level} (A : Locally-Small-Type l1 l2) → (type-Locally-Small-Type A → Locally-Small-Type l3 l4) → Locally-Small-Type (l1 ⊔ l3) (l2 ⊔ l4) pr1 (Σ-Locally-Small-Type A B) = - Σ (type-Locally-Small-Type A) (λ a → type-Locally-Small-Type (B a)) + Σ (type-Locally-Small-Type A) (type-Locally-Small-Type ∘ B) pr2 (Σ-Locally-Small-Type A B) = is-locally-small-Σ ( is-locally-small-type-Locally-Small-Type A) - ( λ a → is-locally-small-type-Locally-Small-Type (B a)) + ( is-locally-small-type-Locally-Small-Type ∘ B) ``` ### The underlying type of a subtype of a locally small type is locally small @@ -135,7 +143,7 @@ is-locally-small-type-subtype : is-locally-small l3 A → is-locally-small l3 (type-subtype P) is-locally-small-type-subtype {l3 = l3} P H = is-locally-small-Σ H - (λ a → is-locally-small-is-prop l3 (is-prop-is-in-subtype P a)) + ( λ a → is-locally-small-is-prop l3 (is-prop-is-in-subtype P a)) type-subtype-Locally-Small-Type : {l1 l2 l3 : Level} (A : Locally-Small-Type l1 l2) → @@ -152,7 +160,7 @@ is-locally-small-Π : {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} → is-small l3 A → ((x : A) → is-locally-small l4 (B x)) → is-locally-small (l3 ⊔ l4) ((x : A) → B x) -is-locally-small-Π {l1} {l2} {l3} {l4} H K f g = +is-locally-small-Π H K f g = is-small-equiv ( f ~ g) ( equiv-funext) @@ -167,7 +175,7 @@ pr1 (Π-Locally-Small-Type A B) = pr2 (Π-Locally-Small-Type A B) = is-locally-small-Π ( is-small-type-Small-Type A) - ( λ a → is-locally-small-type-Locally-Small-Type (B a)) + ( is-locally-small-type-Locally-Small-Type ∘ B) ``` ### The type of types in any given subuniverse is locally small @@ -185,8 +193,8 @@ is-locally-small-type-subuniverse P = ```agda is-locally-small-Locally-Small-Type : {l1 l2 : Level} → is-locally-small l2 (Locally-Small-Type l1 l2) -is-locally-small-Locally-Small-Type {l1} {l2} = - is-locally-small-type-subuniverse ( is-locally-small-Prop l1) +is-locally-small-Locally-Small-Type {l1} = + is-locally-small-type-subuniverse (is-locally-small-Prop l1) ``` ### The type of truncated types is locally small @@ -213,7 +221,7 @@ is-locally-small-subtype : {l1 l2 l3 : Level} {A : UU l1} → is-small l2 A → is-locally-small (l2 ⊔ l3) (subtype l3 A) is-locally-small-subtype H = - is-locally-small-Π H (λ a → is-locally-small-type-Prop) + is-locally-small-Π H (λ _ → is-locally-small-type-Prop) ``` ### The type of inhabited subtypes of a small type is locally small @@ -227,3 +235,17 @@ is-locally-small-inhabited-subtype H = ( is-inhabited-subtype-Prop) ( is-locally-small-subtype H) ``` + +## See also + +- [The replacement axiom](foundation.replacement.md) + +## References + +- Egbert Rijke, Theorem 4.6 in _The join construction_, 2017 + ([arXiv:1701.07538](https://arxiv.org/abs/1701.07538), + [DOI:10.48550](https://doi.org/10.48550/arXiv.1701.07538)) +- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. + Grayson, Section 2.19 of _Symmetry_ + ([draft](https://unimath.github.io/SymmetryBook/book.pdf), + [GitHub](https://github.com/UniMath/SymmetryBook)) diff --git a/src/foundation/pi-decompositions.lagda.md b/src/foundation/pi-decompositions.lagda.md index 1caa7c727c..f2a25a6f13 100644 --- a/src/foundation/pi-decompositions.lagda.md +++ b/src/foundation/pi-decompositions.lagda.md @@ -245,7 +245,7 @@ module _ ## Properties -### Characterization of equality of Π-Decompositions +### Characterization of equality of Π-decompositions ```agda equiv-Π-Decomposition : diff --git a/src/foundation/powersets.lagda.md b/src/foundation/powersets.lagda.md index c5df1b24ca..1db729127f 100644 --- a/src/foundation/powersets.lagda.md +++ b/src/foundation/powersets.lagda.md @@ -16,6 +16,7 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.propositions +open import foundation-core.sets open import order-theory.large-posets open import order-theory.large-preorders @@ -25,9 +26,12 @@ open import order-theory.preorders -## Definitions +## Idea -### Powersets +The **powerset** of a type is the set of all +[subtypes](foundation-core.subtypes.md) with respect to a given universe level. + +## Definition ```agda powerset : @@ -35,6 +39,22 @@ powerset : powerset = subtype ``` +## Properties + +### The powerset is a set + +```agda +module _ + {l1 : Level} (A : UU l1) + where + + is-set-powerset : {l2 : Level} → is-set (powerset l2 A) + is-set-powerset = is-set-subtype + + powerset-Set : (l2 : Level) → Set (l1 ⊔ lsuc l2) + powerset-Set l2 = subtype-Set l2 A +``` + ### The powerset large preorder ```agda diff --git a/src/foundation/principle-of-omniscience.lagda.md b/src/foundation/principle-of-omniscience.lagda.md index 6053158bbf..e3a35258cb 100644 --- a/src/foundation/principle-of-omniscience.lagda.md +++ b/src/foundation/principle-of-omniscience.lagda.md @@ -19,8 +19,12 @@ open import foundation-core.propositions ## Idea -A type `X` is said to satisfy the principle of omniscience if every decidable -subtype of `X` is either inhabited or empty. +A type `X` is said to satisfy the **principle of omniscience** if every +[decidable subtype](foundation.decidable-subtypes.md) of `X` is either +[inhabited](foundation.inhabited-types.md) or +[empty](foundation-core.empty-types.md). + +## Definition ```agda is-omniscient-Prop : {l : Level} → UU l → Prop (lsuc lzero ⊔ l) @@ -32,3 +36,9 @@ is-omniscient-Prop X = is-omniscient : {l : Level} → UU l → UU (lsuc lzero ⊔ l) is-omniscient X = type-Prop (is-omniscient-Prop X) ``` + +## See also + +- [The limited principle of omniscience](foundation.limited-principle-of-omniscience.md) +- [The lesser limited principle of omniscience](foundation.lesser-limited-principle-of-omniscience.md) +- [The weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md) diff --git a/src/foundation/relaxed-sigma-decompositions.lagda.md b/src/foundation/relaxed-sigma-decompositions.lagda.md index d845f25bd9..5af06d2e2a 100644 --- a/src/foundation/relaxed-sigma-decompositions.lagda.md +++ b/src/foundation/relaxed-sigma-decompositions.lagda.md @@ -232,7 +232,7 @@ module _ ## Properties -### Characterization of equality of Relaxed-Σ-Decompositions +### Characterization of equality of relaxed-Σ-decompositions ```agda equiv-Relaxed-Σ-Decomposition : @@ -622,7 +622,7 @@ module _ (extensionality-displayed-Relaxed-Σ-Decomposition D) ``` -#### Equivalence between fibered double Relaxed-Σ-Decompositions and displayed double Relaxed-Σ-Decompositions +#### Equivalence between fibered double relaxed Σ-recompositions and displayed double relaxed Σ-decompositions ```agda module _ diff --git a/src/foundation/replacement.lagda.md b/src/foundation/replacement.lagda.md index 03a5b5719b..27f36890c4 100644 --- a/src/foundation/replacement.lagda.md +++ b/src/foundation/replacement.lagda.md @@ -18,21 +18,37 @@ open import foundation-core.small-types ## Idea -The type theoretic replacement axiom asserts that the image of a map `f : A → B` -from a small type `A` into a locally small type `B` is small. +The **type theoretic replacement axiom** asserts that the image of a map +`f : A → B` from a small type `A` into a locally small type `B` is small. -## Definition +## Statement ```agda Replacement : (l : Level) → UUω Replacement l = {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-small l A → is-locally-small l B → is-small l (im f) +``` + +## Postulate +```agda postulate replacement : {l : Level} → Replacement l +``` +```agda replacement-UU : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-locally-small l1 B → is-small l1 (im f) -replacement-UU {l1} {l2} {A} f = replacement f is-small' +replacement-UU f = replacement f is-small' ``` + +## References + +- Egbert Rijke, Theorem 4.6 in _The join construction_, 2017 + ([arXiv:1701.07538](https://arxiv.org/abs/1701.07538), + [DOI:10.48550](https://doi.org/10.48550/arXiv.1701.07538)) +- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. + Grayson, Section 2.19 of _Symmetry_ + ([newest version](https://unimath.github.io/SymmetryBook/book.pdf), + [GitHub](https://github.com/UniMath/SymmetryBook)) diff --git a/src/foundation/sigma-decompositions.lagda.md b/src/foundation/sigma-decompositions.lagda.md index 4bf9180da1..4787c5c126 100644 --- a/src/foundation/sigma-decompositions.lagda.md +++ b/src/foundation/sigma-decompositions.lagda.md @@ -33,13 +33,13 @@ open import foundation-core.identity-types ## Idea -A Σ-decomposition of a type `A` consists of a type `X` and a family of inhabited -types `Y x` indexed by `x : A` equipped with an equivalence `A ≃ Σ X Y`. The -type `X` is called the indexing type of the Σ-decomposition, the elements of -`Y x` are called the cotypes of the Σ-decomposition, and the equivalence -`A ≃ Σ X Y` is the matching correspondence of the Σ-decomposition +A **Σ-decomposition** of a type `A` consists of a type `X` and a family of +inhabited types `Y x` indexed by `x : A` equipped with an equivalence +`A ≃ Σ X Y`. The type `X` is called the indexing type of the Σ-decomposition, +the elements of `Y x` are called the cotypes of the Σ-decomposition, and the +equivalence `A ≃ Σ X Y` is the matching correspondence of the Σ-decomposition. -Note that types may have many Σ-decomposition. The type of Σ-decompositions of +Note that types may have many Σ-decompositions. The type of Σ-decompositions of the unit type, for instance, is equivalent to the type of all pointed connected types. Alternatively, we may think of the type of Σ-decompositions of the unit type as the type of higher groupoid structures on a point, i.e., the type of @@ -47,9 +47,8 @@ higher group structures. We may restrict to Σ-decompositions where the indexing type is in a given subuniverse, such as the subuniverse of sets or the subuniverse of finite sets. - -The type of set-indexed Σ-decompositions of a type `A` is equivalent to the type -of equivalence relations on `A`. +For instance, the type of set-indexed Σ-decompositions of a type `A` is +equivalent to the type of equivalence relations on `A`. ## Definitions @@ -347,7 +346,7 @@ module _ ## Properties -### Characterization of equality of Σ-Decompositions +### Characterization of equality of Σ-decompositions ```agda equiv-Σ-Decomposition : @@ -473,7 +472,7 @@ module _ map-equiv-tr-Σ-Decomposition = map-equiv equiv-tr-Σ-Decomposition ``` -### Characterization of equality of set-indexed Σ-Decompositions +### Characterization of equality of set-indexed Σ-decompositions ```agda equiv-Set-Indexed-Σ-Decomposition : @@ -807,7 +806,7 @@ module _ (extensionality-displayed-Σ-Decomposition D) ``` -#### Equivalence between fibered double Σ-Decompositions and displayed double Σ-Decompositions +#### Equivalence between fibered double Σ-decompositions and displayed double Σ-decompositions ```agda module _ diff --git a/src/foundation/slice.lagda.md b/src/foundation/slice.lagda.md index 4e1b4d9adb..88f7059f22 100644 --- a/src/foundation/slice.lagda.md +++ b/src/foundation/slice.lagda.md @@ -1,4 +1,4 @@ -# Morphisms of the slice category of types +# Morphisms in the slice category of types ```agda module foundation.slice where @@ -50,7 +50,7 @@ Slice : (l : Level) {l1 : Level} (A : UU l1) → UU (l1 ⊔ lsuc l) Slice l = type-polynomial-endofunctor (UU l) (λ X → X) ``` -### The morphisms of the slice category of types +### The morphisms in the slice category of types ```agda module _ diff --git a/src/foundation/structure.lagda.md b/src/foundation/structure.lagda.md index d411448fd3..0a442e833b 100644 --- a/src/foundation/structure.lagda.md +++ b/src/foundation/structure.lagda.md @@ -20,7 +20,7 @@ open import foundation-core.identity-types ## Idea -Given a type family `P` on the universe, a `P`-structured type consists of a +Given a type family `P` on the universe, a **`P`-structured type** consists of a type `A` equipped with an element of type `P A`. ## Definition diff --git a/src/foundation/subtypes.lagda.md b/src/foundation/subtypes.lagda.md index 5f18c2f188..a76d7d4623 100644 --- a/src/foundation/subtypes.lagda.md +++ b/src/foundation/subtypes.lagda.md @@ -144,12 +144,12 @@ module _ ```agda is-set-subtype : {l1 l2 : Level} {A : UU l1} → is-set (subtype l2 A) -is-set-subtype {l1} {l2} {A} P Q = +is-set-subtype P Q = is-prop-equiv ( extensionality-subtype P Q) ( is-prop-has-same-elements-subtype P Q) subtype-Set : {l1 : Level} (l2 : Level) → UU l1 → Set (l1 ⊔ lsuc l2) -pr1 (subtype-Set {l1} l2 A) = subtype l2 A -pr2 (subtype-Set {l1} l2 A) = is-set-subtype +pr1 (subtype-Set l2 A) = subtype l2 A +pr2 (subtype-Set l2 A) = is-set-subtype ``` diff --git a/src/foundation/subuniverses.lagda.md b/src/foundation/subuniverses.lagda.md index 02be574f64..bd890c7aed 100644 --- a/src/foundation/subuniverses.lagda.md +++ b/src/foundation/subuniverses.lagda.md @@ -1,4 +1,4 @@ -# Subuniverse +# Subuniverses ```agda module foundation.subuniverses where @@ -26,7 +26,7 @@ open import foundation-core.subtypes ## Idea -Subuniverses are subtypes of the universe. +**Subuniverses** are [subtypes](foundation-core.subtypes.md) of the universe. ## Definitions diff --git a/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md b/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md index 2cba62d7e5..68e25d86e3 100644 --- a/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md +++ b/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md @@ -1,4 +1,4 @@ -# Trivial relaxed Σ-Decompositions +# Trivial relaxed Σ-decompositions ```agda module foundation.trivial-relaxed-sigma-decompositions where diff --git a/src/foundation/trivial-sigma-decompositions.lagda.md b/src/foundation/trivial-sigma-decompositions.lagda.md index 3a0d8ec4a0..4fca2baec6 100644 --- a/src/foundation/trivial-sigma-decompositions.lagda.md +++ b/src/foundation/trivial-sigma-decompositions.lagda.md @@ -1,4 +1,4 @@ -# Trivial Σ-Decompositions +# Trivial Σ-decompositions ```agda module foundation.trivial-sigma-decompositions where diff --git a/src/foundation/truncation-modalities.lagda.md b/src/foundation/truncation-modalities.lagda.md new file mode 100644 index 0000000000..cfda848b4a --- /dev/null +++ b/src/foundation/truncation-modalities.lagda.md @@ -0,0 +1,50 @@ +# The truncation modalities + +```agda +module foundation.truncation-modalities where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.functions +open import foundation.truncations +open import foundation.universe-levels + +open import foundation-core.truncation-levels + +open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.uniquely-eliminating-modalities +``` + +
+ +## Idea + +The [truncation](foundation.truncations.md) operations are +[higher modalities](orthogonal-factorization-systems.higher-modalities.md). + +## Definition + +```agda +operator-trunc-modality : + (l : Level) (k : 𝕋) → operator-modality l l +operator-trunc-modality _ = type-trunc + +unit-trunc-modality : + {l : Level} {k : 𝕋} → unit-modality (operator-trunc-modality l k) +unit-trunc-modality = unit-trunc +``` + +## Properties + +### The truncation modalities are uniquely eliminating modalities + +```agda +is-uniquely-eliminating-modality-trunc-modality : + {l : Level} {k : 𝕋} → + is-uniquely-eliminating-modality (unit-trunc-modality {l} {k}) +is-uniquely-eliminating-modality-trunc-modality {k = k} A P = + dependent-universal-property-trunc (trunc k ∘ P) +``` diff --git a/src/foundation/truncations.lagda.md b/src/foundation/truncations.lagda.md index a341d939e2..a9e9b5d34b 100644 --- a/src/foundation/truncations.lagda.md +++ b/src/foundation/truncations.lagda.md @@ -33,7 +33,7 @@ open import foundation-core.universal-property-truncation ## Idea -We postulate the existence of truncations +We postulate the existence of truncations. ## Postulates @@ -66,7 +66,7 @@ pr2 (equiv-universal-property-trunc A B) = is-truncation-trunc B ## Properties -### The `n`-truncations satisfy the universal property +### The `n`-truncations satisfy the universal property of `n`-truncations ```agda universal-property-trunc : @@ -108,7 +108,7 @@ module _ pr2 (apply-universal-property-trunc B f) ``` -### The `n`-truncations satisfy the dependent universal property +### The `n`-truncations satisfy the dependent universal property of `n`-truncations ```agda module _ @@ -223,12 +223,12 @@ module _ module _ {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} (B : A → Truncated-Type l2 k) - ( C : total-truncated-fam-trunc B → Truncated-Type l3 k) - ( f : (x : A) (y : type-Truncated-Type (B x)) → - type-Truncated-Type - ( C ( pair - ( unit-trunc x) - ( map-equiv (compute-truncated-fam-trunc B x) y)))) + ( C : total-truncated-fam-trunc B → Truncated-Type l3 k) + ( f : + ( x : A) + ( y : type-Truncated-Type (B x)) → + type-Truncated-Type + ( C (unit-trunc x , map-equiv (compute-truncated-fam-trunc B x) y))) where dependent-universal-property-total-truncated-fam-trunc : @@ -237,7 +237,7 @@ module _ ( λ h → (x : A) (y : type-Truncated-Type (B x)) → Id - ( h (pair (unit-trunc x) (map-compute-truncated-fam-trunc B x y))) + ( h (unit-trunc x , map-compute-truncated-fam-trunc B x y)) ( f x y))) dependent-universal-property-total-truncated-fam-trunc = is-contr-equiv _ @@ -247,7 +247,7 @@ module _ Id ( g (unit-trunc x)) ( map-equiv-Π - ( λ u → type-Truncated-Type (C (pair (unit-trunc x) u))) + ( λ u → type-Truncated-Type (C (unit-trunc x , u))) ( compute-truncated-fam-trunc B x) ( λ u → id-equiv) ( f x))) @@ -255,41 +255,38 @@ module _ ( λ g → equiv-map-Π ( λ x → - ( inv-equiv equiv-funext) ∘e - ( equiv-Π - ( λ y → - Id - ( g (pair (unit-trunc x) y)) - ( map-equiv-Π - ( λ u → - type-Truncated-Type (C (pair (unit-trunc x) u))) + ( inv-equiv equiv-funext) ∘e + ( equiv-Π + ( λ y → + Id + ( g (unit-trunc x , y)) + ( map-equiv-Π + ( λ u → + type-Truncated-Type (C (unit-trunc x , u))) + ( compute-truncated-fam-trunc B x) + ( λ u → id-equiv) + ( f x) + ( y))) + ( compute-truncated-fam-trunc B x) + ( λ y → + equiv-concat' + ( g (unit-trunc x , map-compute-truncated-fam-trunc B x y)) + ( inv + ( compute-map-equiv-Π + ( λ u → type-Truncated-Type (C (unit-trunc x , u))) ( compute-truncated-fam-trunc B x) - ( λ u → id-equiv) + ( λ y → id-equiv) ( f x) - ( y))) - ( compute-truncated-fam-trunc B x) - ( λ y → - equiv-concat' - ( g ( pair - ( unit-trunc x) - ( map-compute-truncated-fam-trunc B x y))) - ( inv - ( compute-map-equiv-Π - ( λ u → - type-Truncated-Type (C (pair (unit-trunc x) u))) - ( compute-truncated-fam-trunc B x) - ( λ y → id-equiv) - ( λ y → f x y) - ( y)))))))) + ( y)))))))) ( unique-dependent-function-trunc ( λ y → truncated-type-succ-Truncated-Type k ( Π-Truncated-Type k ( truncated-fam-trunc B y) - ( λ u → C (pair y u)))) + ( λ u → C (y , u)))) ( λ y → map-equiv-Π - ( λ u → type-Truncated-Type (C (pair (unit-trunc y) u))) + ( λ u → type-Truncated-Type (C (unit-trunc y , u))) ( compute-truncated-fam-trunc B y) ( λ u → id-equiv) ( f y))) @@ -303,13 +300,13 @@ module _ (x : A) (y : type-Truncated-Type (B x)) → Id ( function-dependent-universal-property-total-truncated-fam-trunc - ( pair (unit-trunc x) (map-compute-truncated-fam-trunc B x y))) + ( unit-trunc x , map-compute-truncated-fam-trunc B x y)) ( f x y) htpy-dependent-universal-property-total-truncated-fam-trunc = pr2 (center dependent-universal-property-total-truncated-fam-trunc) ``` -### An n-truncated type is equivalent to its `n`-truncation +### An `n`-truncated type is equivalent to its `n`-truncation ```agda module _ @@ -338,13 +335,9 @@ module _ ( type-Truncated-Type A) ( trunc k (type-Truncated-Type A)) ( unit-trunc))) - ( pair - ( unit-trunc ∘ map-inv-unit-trunc) - ( unit-trunc ·l - isretr-map-inv-unit-trunc)) - ( pair - ( id) - ( refl-htpy))))) + ( unit-trunc ∘ map-inv-unit-trunc , + unit-trunc ·l isretr-map-inv-unit-trunc) + ( id , refl-htpy)))) is-equiv-unit-trunc : is-equiv unit-trunc is-equiv-unit-trunc = @@ -409,7 +402,7 @@ module _ ( λ b → truncated-type-succ-Truncated-Type k ( Eq-trunc-Truncated-Type b))) - ( pair (unit-trunc a) refl-Eq-trunc)) + ( unit-trunc a , refl-Eq-trunc)) ( λ y → function-dependent-universal-property-trunc ( λ q → @@ -419,16 +412,16 @@ module _ ( λ y → truncated-type-succ-Truncated-Type k ( Eq-trunc-Truncated-Type y))) - ( pair (unit-trunc a) refl-Eq-trunc) - ( pair (unit-trunc y) (map-compute-Eq-trunc y q))) + ( unit-trunc a , refl-Eq-trunc) + ( unit-trunc y , map-compute-Eq-trunc y q)) ( r y)) where r : (y : A) (p : a ＝ y) → Id { A = Σ (type-trunc (succ-𝕋 k) A) Eq-trunc} - ( pair (unit-trunc a) refl-Eq-trunc) - ( pair (unit-trunc y) (map-compute-Eq-trunc y (unit-trunc p))) + ( unit-trunc a , refl-Eq-trunc) + ( unit-trunc y , (map-compute-Eq-trunc y (unit-trunc p))) r .a refl = refl Eq-eq-trunc : (x : type-trunc (succ-𝕋 k) A) → (unit-trunc a ＝ x) → Eq-trunc x @@ -475,17 +468,17 @@ module _ map-trunc-Σ = map-universal-property-trunc ( trunc k (Σ A (λ x → type-trunc k (B x)))) - ( λ (pair a b) → unit-trunc (pair a (unit-trunc b))) + ( λ (a , b) → unit-trunc (a , unit-trunc b)) map-inv-trunc-Σ : type-trunc k (Σ A (λ x → type-trunc k (B x))) → type-trunc k (Σ A B) map-inv-trunc-Σ = map-universal-property-trunc ( trunc k (Σ A B)) - ( λ (pair a |b|) → + ( λ (a , |b|) → map-universal-property-trunc ( trunc k (Σ A B)) - ( λ b → unit-trunc (pair a b)) + ( λ b → unit-trunc (a , b)) ( |b|)) isretr-map-inv-trunc-Σ : @@ -497,21 +490,21 @@ module _ ( trunc k (Σ A B)) ( map-inv-trunc-Σ (map-trunc-Σ |ab|)) ( |ab|)) - ( λ (pair a b) → + ( λ (a , b) → ( ap ( map-inv-trunc-Σ) ( triangle-universal-property-trunc _ - ( λ (pair a' b') → unit-trunc (pair a' (unit-trunc b'))) - ( pair a b))) ∙ + ( λ (a' , b') → unit-trunc (a' , unit-trunc b')) + ( a , b))) ∙ ( triangle-universal-property-trunc _ - ( λ (pair a' |b'|) → + ( λ (a' , |b'|) → map-universal-property-trunc ( trunc k (Σ A B)) - ( λ b' → unit-trunc (pair a' b')) + ( λ b' → unit-trunc (a' , b')) ( |b'|)) - ( pair a (unit-trunc b)) ∙ + ( a , unit-trunc b) ∙ triangle-universal-property-trunc _ - ( λ b' → unit-trunc (pair a b')) + ( λ b' → unit-trunc (a , b')) ( b))) issec-map-inv-trunc-Σ : @@ -523,30 +516,30 @@ module _ ( trunc k (Σ A (λ x → type-trunc k (B x)))) ( map-trunc-Σ (map-inv-trunc-Σ |a|b||)) ( |a|b||)) - ( λ (pair a |b|) → + ( λ (a , |b|) → function-dependent-universal-property-trunc (λ |b'| → Id-Truncated-Type' ( trunc k (Σ A (λ x → type-trunc k (B x)))) - (map-trunc-Σ (map-inv-trunc-Σ (unit-trunc (pair a |b'|)))) - (unit-trunc (pair a |b'|))) + (map-trunc-Σ (map-inv-trunc-Σ (unit-trunc (a , |b'|)))) + (unit-trunc (a , |b'|))) (λ b → ap map-trunc-Σ (triangle-universal-property-trunc _ - ( λ (pair a' |b'|) → + ( λ (a' , |b'|) → map-universal-property-trunc ( trunc k (Σ A B)) - ( λ b' → unit-trunc (pair a' b')) + ( λ b' → unit-trunc (a' , b')) ( |b'|)) - ( pair a (unit-trunc b))) ∙ + ( a , unit-trunc b)) ∙ (ap map-trunc-Σ (triangle-universal-property-trunc ( trunc k (Σ A B)) - ( λ b' → unit-trunc (pair a b')) + ( λ b' → unit-trunc (a , b')) ( b)) ∙ triangle-universal-property-trunc _ - ( λ (pair a' b') → unit-trunc (pair a' (unit-trunc b'))) - ( pair a b))) + ( λ (a' , b') → unit-trunc (a' , unit-trunc b')) + ( a , b))) ( |b|)) equiv-trunc-Σ : diff --git a/src/foundation/unions-subtypes.lagda.md b/src/foundation/unions-subtypes.lagda.md index 51b0934d91..af9d81b182 100644 --- a/src/foundation/unions-subtypes.lagda.md +++ b/src/foundation/unions-subtypes.lagda.md @@ -1,4 +1,4 @@ -# Union of subtypes +# Unions of subtypes ```agda module foundation.unions-subtypes where diff --git a/src/foundation/unital-binary-operations.lagda.md b/src/foundation/unital-binary-operations.lagda.md index bcb9a54e2b..a4d3e9a4bd 100644 --- a/src/foundation/unital-binary-operations.lagda.md +++ b/src/foundation/unital-binary-operations.lagda.md @@ -19,10 +19,10 @@ open import foundation-core.identity-types ## Idea -A binary operation of type `A → A → A` is unital if there is a unit of type `A` -that satisfies both the left and right unit laws. Furthermore, an binary -operation is _coherently_ unital if the proofs of left and right unit laws agree -on the case where both arguments of the operation are the unit. +A binary operation of type `A → A → A` is **unital** if there is a unit of type +`A` that satisfies both the left and right unit laws. Furthermore, a binary +operation is **coherently unital** if the proofs of the left and right unit laws +agree on the case where both arguments of the operation are the unit. ## Definitions diff --git a/src/foundation/unordered-tuples.lagda.md b/src/foundation/unordered-tuples.lagda.md index da9ffc8820..e2a25a4d49 100644 --- a/src/foundation/unordered-tuples.lagda.md +++ b/src/foundation/unordered-tuples.lagda.md @@ -1,4 +1,4 @@ -# Unordered n-tuples of elements in a type +# Unordered `n`-tuples of elements in a type ```agda module foundation.unordered-tuples where @@ -34,8 +34,8 @@ open import univalent-combinatorics.standard-finite-types ## Idea -An unordered n-tuple of elements of a type `A` consists of an n-element set `X` -equipped with a map `X → A`. +An **unordered `n`-tuple** of elements of a type `A` consists of an `n`-element +set `X` equipped with a map `X → A`. ## Definition diff --git a/src/foundation/weak-limited-principle-of-omniscience.lagda.md b/src/foundation/weak-limited-principle-of-omniscience.lagda.md index 8e5480c9da..6db88e320b 100644 --- a/src/foundation/weak-limited-principle-of-omniscience.lagda.md +++ b/src/foundation/weak-limited-principle-of-omniscience.lagda.md @@ -21,14 +21,12 @@ open import univalent-combinatorics.standard-finite-types -## Idea +## Statement The **Weak Limited Principle of Omniscience** asserts that for any sequence `f : ℕ → Fin 2` either `f n ＝ 0` for all `n : ℕ` or not. In particular, it is a restricted form of the law of excluded middle. -## Definition - ```agda WLPO : UU lzero WLPO = @@ -37,3 +35,9 @@ WLPO = ( Π-Prop ℕ (λ n → Id-Prop (Fin-Set 2) (f n) (zero-Fin 1))) ( neg-Prop (Π-Prop ℕ (λ n → Id-Prop (Fin-Set 2) (f n) (zero-Fin 1)))) ``` + +## See also + +- [The principle of omniscience](foundation.principle-of-omniscience.md) +- [The limited principle of omniscience](foundation.limited-principle-of-omniscience.md) +- [The lesser limited principle of omniscience](foundation.lesser-limited-principle-of-omniscience.md) diff --git a/src/group-theory/e8-lattice.lagda.md b/src/group-theory/e8-lattice.lagda.md index c369ad7a0e..843bc6e783 100644 --- a/src/group-theory/e8-lattice.lagda.md +++ b/src/group-theory/e8-lattice.lagda.md @@ -1,4 +1,4 @@ -# The E₈-lattice +# The `E₈`-lattice ```agda module group-theory.e8-lattice where diff --git a/src/group-theory/normal-submonoids.lagda.md b/src/group-theory/normal-submonoids.lagda.md index d0d68cfe5d..5906e57ef5 100644 --- a/src/group-theory/normal-submonoids.lagda.md +++ b/src/group-theory/normal-submonoids.lagda.md @@ -33,12 +33,12 @@ open import group-theory.subsets-monoids ## Idea -A normal submonoid `N` of `M` is a monoid for which there exists a congruence -relation `~` on `M` such that the elements of `N` are precisely the elements -`x ~ 1`. Such a congruence relation is rarely unique. However, one can show that -the normal submonoids form a retract of the type of congruence relations on `M`, -and that the normal submonoids correspond uniquely to _saturated_ congruence -relations. +A **normal submonoid** `N` of `M` is a monoid for which there exists a +congruence relation `~` on `M` such that the elements of `N` are precisely the +elements `x ~ 1`. Such a congruence relation is rarely unique. However, one can +show that the normal submonoids form a retract of the type of congruence +relations on `M`, and that the normal submonoids correspond uniquely to +_saturated_ congruence relations. A submonoid `N` of `M` is normal if and only if for all `x y : M` and `u : N` we have diff --git a/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md b/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md index 01a4cda134..732bb101ef 100644 --- a/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md +++ b/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md @@ -24,8 +24,8 @@ open import univalent-combinatorics.standard-finite-types ## Idea -Given an unordered n-tuple of elements in a commutative monoid, we can define -their product +Given an unordered `n`-tuple of elements in a commutative monoid, we can define +their product. ## Definition diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index a1d295ada8..ad0fa59a18 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -1,16 +1,30 @@ # Orthogonal factorization systems +## Examples of higher modalities + +| Modality | File | +| --------------------------------- | ------------------------------------------------------------------------------------------------------------- | +| The closed modalities | [`orthogonal-factorization-systems.closed-modalities`](orthogonal-factorization-systems.closed-modalities.md) | +| The double negation modality | [`foundation.double-negation-modality`](foundation.double-negation-modality.md) | +| The identity modality | [`orthogonal-factorization-systems.identity-modality`](orthogonal-factorization-systems.identity-modality.md) | +| The open modalities | [`orthogonal-factorization-systems.open-modalities`](orthogonal-factorization-systems.open-modalities.md) | +| Raising universe level modalities | [`orthogonal-factorization-systems.raise-modalities`](orthogonal-factorization-systems.raise-modalities.md) | +| The truncation modalities | [`foundation.truncation-modalities`](foundation.truncation-modalities.md) | +| The zero modality | [`orthogonal-factorization-systems.zero-modality`](orthogonal-factorization-systems.zero-modality.md) | + ## Files in the orthogonal factorization systems folder ```agda module orthogonal-factorization-systems where +open import orthogonal-factorization-systems.closed-modalities public open import orthogonal-factorization-systems.extensions-of-maps public open import orthogonal-factorization-systems.factorization-operations public open import orthogonal-factorization-systems.factorization-operations-function-classes public open import orthogonal-factorization-systems.factorizations-of-maps public open import orthogonal-factorization-systems.function-classes public open import orthogonal-factorization-systems.higher-modalities public +open import orthogonal-factorization-systems.identity-modality public open import orthogonal-factorization-systems.lifting-operations public open import orthogonal-factorization-systems.lifting-squares public open import orthogonal-factorization-systems.lifts-of-maps public @@ -18,12 +32,16 @@ open import orthogonal-factorization-systems.local-types public open import orthogonal-factorization-systems.mere-lifting-properties public open import orthogonal-factorization-systems.modal-operators public 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.pullback-hom public +open import orthogonal-factorization-systems.raise-modalities public open import orthogonal-factorization-systems.reflective-subuniverses public +open import orthogonal-factorization-systems.separated-types 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.uniquely-eliminating-modalities public open import orthogonal-factorization-systems.wide-function-classes public +open import orthogonal-factorization-systems.zero-modality public ``` diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md new file mode 100644 index 0000000000..cdf017adc4 --- /dev/null +++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md @@ -0,0 +1,129 @@ +# The closed modalities + +```agda +module orthogonal-factorization-systems.closed-modalities where +``` + +
Imports + +```agda +open import foundation.contractible-maps +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.functions +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.universe-levels + +open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.reflective-subuniverses +open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses + +open import synthetic-homotopy-theory.joins-of-types +``` + +
+ +## Idea + +Given any proposition `Q`, the +[join](synthetic-homotopy-theory.joins-of-types.md) operation `_* Q` defines a +[higher modality](orthogonal-factorization-systems.higher-modalities.md). We +call these the **closed modalities**. + +## Definition + +```agda +operator-closed-modality : + (l : Level) {lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ) +operator-closed-modality l Q A = A * type-Prop Q + +unit-closed-modality : + {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality l Q) +unit-closed-modality Q {A} = inl-join A (type-Prop Q) + +is-closed-modal : + {l lQ : Level} (Q : Prop lQ) → UU l → Prop (l ⊔ lQ) +pr1 (is-closed-modal Q B) = type-Prop Q → is-contr B +pr2 (is-closed-modal Q B) = is-prop-function-type is-property-is-contr +``` + +## Properties + +### The closed modalities define `Σ`-closed reflective subuniverses + +```agda +module _ + {l lQ : Level} (Q : Prop lQ) + where + + is-reflective-subuniverse-closed-modality : + is-reflective-subuniverse + { l ⊔ lQ} + ( unit-closed-modality Q) + ( is-closed-modal Q) + pr1 is-reflective-subuniverse-closed-modality A q = + right-zero-law-join-is-contr + ( A) + ( type-Prop Q) + ( is-proof-irrelevant-is-prop (is-prop-type-Prop Q) q) + pr2 is-reflective-subuniverse-closed-modality B is-modal-B A = + is-equiv-is-contr-map + ( λ f → + is-contr-equiv + ( Σ (A → B) (_＝ f)) + ( equiv-Σ + ( _＝ f) + ( right-unit-law-Σ-is-contr + ( λ f' → + is-contr-Σ + ( is-contr-Π is-modal-B) + ( center ∘ is-modal-B) + ( is-contr-Π + ( λ (a , q) → + is-prop-is-contr + ( is-modal-B q) + ( f' a) + ( center (is-modal-B q))))) ∘e + ( equiv-up-join A (type-Prop Q) B)) + ( λ _ → id-equiv)) + ( is-contr-total-path' f)) + + reflective-subuniverse-closed-modality : + reflective-subuniverse (l ⊔ lQ) (l ⊔ lQ) + pr1 reflective-subuniverse-closed-modality = + operator-closed-modality (l ⊔ lQ) Q + pr1 (pr2 reflective-subuniverse-closed-modality) = + unit-closed-modality Q + pr1 (pr2 (pr2 reflective-subuniverse-closed-modality)) = + is-closed-modal Q + pr2 (pr2 (pr2 reflective-subuniverse-closed-modality)) = + is-reflective-subuniverse-closed-modality + + is-Σ-closed-reflective-subuniverse-closed-modality : + is-Σ-closed-reflective-subuniverse + ( reflective-subuniverse-closed-modality) + is-Σ-closed-reflective-subuniverse-closed-modality + X is-modal-X P is-modal-P q = + is-contr-Σ + ( is-modal-X q) + ( center (is-modal-X q)) + ( is-modal-P (center (is-modal-X q)) q) + + Σ-closed-reflective-subuniverse-closed-modality : + Σ-closed-reflective-subuniverse (l ⊔ lQ) (l ⊔ lQ) + pr1 Σ-closed-reflective-subuniverse-closed-modality = + reflective-subuniverse-closed-modality + pr2 Σ-closed-reflective-subuniverse-closed-modality = + is-Σ-closed-reflective-subuniverse-closed-modality +``` + +## References + +- Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type + theory_, Logical Methods in Computer Science, Volume 16, Issue 1, 2020 + ([arXiv:1706.07526](https://arxiv.org/abs/1706.07526), + [doi:10.23638](https://doi.org/10.23638/LMCS-16%281%3A2%292020)) diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md index 12eb03850b..458baa84e1 100644 --- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md @@ -37,8 +37,10 @@ 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`. Because of this, higher modalities in their most general form -only make sense for locally small modal operators. +`x' y' : ○ X`. In other words, `○ X` is +[`○`-separated](orthogonal-factorization-systems.separated-types.md). Because of +this, higher modalities in their most general form only make sense for locally +small modal operators. ## Definition @@ -66,8 +68,8 @@ module _ (f : (x : X) → ○ (P (unit-○ x))) → (x : X) → ind-○ X P f (unit-○ x) ＝ f x - modal-universal-property : UU (lsuc l1 ⊔ l2) - modal-universal-property = + dependent-universal-property-modality : UU (lsuc l1 ⊔ l2) + dependent-universal-property-modality = Σ ind-modality compute-ind-modality rec-modality-ind-modality : ind-modality → rec-modality @@ -98,7 +100,7 @@ module _ ```agda is-higher-modality : UU (lsuc l1 ⊔ l2) is-higher-modality = - modal-universal-property (unit-○) × is-modal-identity-types + dependent-universal-property-modality (unit-○) × is-modal-identity-types ``` ### Components of a `is-higher-modality` proof diff --git a/src/orthogonal-factorization-systems/identity-modality.lagda.md b/src/orthogonal-factorization-systems/identity-modality.lagda.md new file mode 100644 index 0000000000..bc8747608d --- /dev/null +++ b/src/orthogonal-factorization-systems/identity-modality.lagda.md @@ -0,0 +1,50 @@ +# The identity modality + +```agda +module orthogonal-factorization-systems.identity-modality where +``` + +
Imports + +```agda +open import foundation.equivalences +open import foundation.functions +open import foundation.universe-levels + +open import orthogonal-factorization-systems.local-types +open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.uniquely-eliminating-modalities +``` + +
+ +## Idea + +The identity operation on types is trivially a +[higher modality](orthogonal-factorization-systems.higher-modalities.md). + +## Definition + +```agda +operator-id-modality : + (l : Level) → operator-modality l l +operator-id-modality l = id + +unit-id-modality : + {l : Level} → unit-modality (operator-id-modality l) +unit-id-modality = id +``` + +## Properties + +### The identity modality is a uniquely eliminating modality + +```agda +is-uniquely-eliminating-modality-id-modality : + {l : Level} → is-uniquely-eliminating-modality (unit-id-modality {l}) +is-uniquely-eliminating-modality-id-modality {l} _ P = + is-local-family-is-equiv + ( unit-id-modality) + ( is-equiv-id) + ( operator-id-modality l ∘ P) +``` diff --git a/src/orthogonal-factorization-systems/lifting-squares.lagda.md b/src/orthogonal-factorization-systems/lifting-squares.lagda.md index b4a71af441..b906d4f801 100644 --- a/src/orthogonal-factorization-systems/lifting-squares.lagda.md +++ b/src/orthogonal-factorization-systems/lifting-squares.lagda.md @@ -23,7 +23,7 @@ open import orthogonal-factorization-systems.lifts-of-maps ## Idea -A _lifting square_ is a commuting square +A **lifting square** is a commuting square ```text h @@ -171,6 +171,9 @@ module _ ( coherence-htpy-lifting-square l l' K E))) ``` +It remans to show that `coherence-htpy-lifting-square` indeed is a +characterization of identifications of lifting squares. + ### Diagonal maps give lifting squares The diagram diff --git a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md b/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md index 21e99664e3..1c03ab75fb 100644 --- a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md +++ b/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md @@ -28,8 +28,8 @@ open import foundation.universe-levels ## Idea -A _lift_ of a map `f : X → B` along a map `i : A → B` is a map `g : X → A` such -that the composition `i ∘ g` is `f`. +A **lift** of a map `f : X → B` along a map `i : A → B` is a map `g : X → A` +such that the composition `i ∘ g` is `f`. ```text A diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/local-types.lagda.md index ad83346db1..84d1d29aa9 100644 --- a/src/orthogonal-factorization-systems/local-types.lagda.md +++ b/src/orthogonal-factorization-systems/local-types.lagda.md @@ -40,9 +40,12 @@ A type family `A` over `X` is said to be **local at** `f : Y → X`, or is an equivalence. -Likewise a type `A` is said to be `f`-local if the precomposition map +Likewise, a type `A` is said to be `f`-local if the precomposition map `_∘ f : (X → A) → (Y → A)` is an equivalence. +We reserve the name `is-local` for local types, and specify `is-local-family` +when the type may vary over the base. + ## Definition ```agda @@ -53,8 +56,8 @@ module _ is-local-family : {l : Level} → (X → UU l) → UU (l1 ⊔ l2 ⊔ l) is-local-family A = is-equiv (precomp-Π f A) - is-local-type : {l : Level} → UU l → UU (l1 ⊔ l2 ⊔ l) - is-local-type A = is-local-family (λ _ → A) + is-local : {l : Level} → UU l → UU (l1 ⊔ l2 ⊔ l) + is-local A = is-local-family (λ _ → A) ``` ## Properties @@ -62,31 +65,39 @@ module _ ### Being local is a property ```agda +module _ + {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) + where + is-property-is-local-family : - {l : Level} (A : X → UU l) → is-prop (is-local-family A) + {l : Level} (A : X → UU l) → is-prop (is-local-family f A) is-property-is-local-family A = is-property-is-equiv (precomp-Π f A) is-local-family-Prop : {l : Level} → (X → UU l) → Prop (l1 ⊔ l2 ⊔ l) - pr1 (is-local-family-Prop A) = is-local-family A + pr1 (is-local-family-Prop A) = is-local-family f A pr2 (is-local-family-Prop A) = is-property-is-local-family A - is-property-is-local-type : - {l : Level} (A : UU l) → is-prop (is-local-type A) - is-property-is-local-type A = is-property-is-equiv (precomp f A) + is-property-is-local : + {l : Level} (A : UU l) → is-prop (is-local f A) + is-property-is-local A = is-property-is-local-family (λ _ → A) - is-local-type-Prop : + is-local-Prop : {l : Level} → UU l → Prop (l1 ⊔ l2 ⊔ l) - pr1 (is-local-type-Prop A) = is-local-type A - pr2 (is-local-type-Prop A) = is-property-is-local-type A + is-local-Prop A = is-local-family-Prop (λ _ → A) ``` -### Locality distributes over Π-types +### Being local distributes over Π-types ```agda +module _ + {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) + where + map-distributive-Π-is-local-family : {l3 l4 : Level} {A : UU l3} (B : A → X → UU l4) → - ((a : A) → is-local-family (B a)) → is-local-family (λ x → (a : A) → B a x) + ((a : A) → is-local-family f (B a)) → + is-local-family f (λ x → (a : A) → B a x) map-distributive-Π-is-local-family B f-loc = is-equiv-map-equiv ( equiv-swap-Π ∘e @@ -97,79 +108,120 @@ module _ ### If every type is `f`-local, then `f` is an equivalence ```agda - is-equiv-is-local-type : - ((l : Level) (A : UU l) → is-local-type A) → is-equiv f - is-equiv-is-local-type = is-equiv-is-equiv-precomp f +module _ + {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) + where + + is-equiv-is-local : + ((l : Level) (A : UU l) → is-local f A) → is-equiv f + is-equiv-is-local = is-equiv-is-equiv-precomp f ``` -### If the domain and codomain of `f` is `f`-local then `f` is an equivalence +### If the domain and codomain of `f` is `f`-local, then `f` is an equivalence ```agda +module _ + {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) + where + retraction-sec-precomp-domain : sec (precomp f Y) → retr f pr1 (retraction-sec-precomp-domain sec-precomp-Y) = pr1 sec-precomp-Y id pr2 (retraction-sec-precomp-domain sec-precomp-Y) = htpy-eq (pr2 sec-precomp-Y id) - section-is-local-domains' : sec (precomp f Y) → is-local-type X → sec f + section-is-local-domains' : sec (precomp f Y) → is-local f X → sec f pr1 (section-is-local-domains' sec-precomp-Y is-local-X) = pr1 sec-precomp-Y id pr2 (section-is-local-domains' sec-precomp-Y is-local-X) = htpy-eq ( ap ( pr1) - { pair - ( f ∘ pr1 (section-is-local-domains' sec-precomp-Y is-local-X)) + { ( f ∘ pr1 (section-is-local-domains' sec-precomp-Y is-local-X)) , ( ap (postcomp Y f) (pr2 sec-precomp-Y id))} - { pair id refl} + { id , refl} ( eq-is-contr (is-contr-map-is-equiv is-local-X f))) - is-equiv-is-local-domains' : sec (precomp f Y) → is-local-type X → is-equiv f + + is-equiv-is-local-domains' : sec (precomp f Y) → is-local f X → is-equiv f pr1 (is-equiv-is-local-domains' sec-precomp-Y is-local-X) = section-is-local-domains' sec-precomp-Y is-local-X pr2 (is-equiv-is-local-domains' sec-precomp-Y is-local-X) = retraction-sec-precomp-domain sec-precomp-Y - is-equiv-is-local-domains : is-local-type Y → is-local-type X → is-equiv f + + is-equiv-is-local-domains : is-local f Y → is-local f X → is-equiv f is-equiv-is-local-domains is-local-Y = is-equiv-is-local-domains' (pr1 is-local-Y) ``` +### Propositions are `f`-local if `_∘ f` has a converse + +```agda +module _ + {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) + where + + is-local-family-is-prop : + {l : Level} (A : X → UU l) → + ((x : X) → is-prop (A x)) → + (((y : Y) → A (f y)) → ((x : X) → A x)) → + is-local-family f A + is-local-family-is-prop A is-prop-A = + is-equiv-is-prop + (is-prop-Π is-prop-A) + (is-prop-Π (is-prop-A ∘ f)) + + is-local-is-prop : + {l : Level} (A : UU l) → + is-prop A → ((Y → A) → (X → A)) → is-local f A + is-local-is-prop A is-prop-A = + is-local-family-is-prop (λ _ → A) (λ _ → is-prop-A) +``` + ## Examples ### All type families are local at equivalences ```agda +module _ + {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) + where + is-local-family-is-equiv : - is-equiv f → {l : Level} (A : X → UU l) → is-local-family A + is-equiv f → {l : Level} (A : X → UU l) → is-local-family f A is-local-family-is-equiv is-equiv-f = is-equiv-precomp-Π-is-equiv f is-equiv-f - is-local-type-is-equiv : - is-equiv f → {l : Level} (A : UU l) → is-local-type A - is-local-type-is-equiv is-equiv-f = is-equiv-precomp-is-equiv f is-equiv-f + is-local-is-equiv : + is-equiv f → {l : Level} (A : UU l) → is-local f A + is-local-is-equiv is-equiv-f = is-equiv-precomp-is-equiv f is-equiv-f ``` ### Families of contractible types are local at any map ```agda +module _ + {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X) + where + is-local-family-is-contr : {l : Level} (A : X → UU l) → - ((x : X) → is-contr (A x)) → is-local-family A + ((x : X) → is-contr (A x)) → is-local-family f A is-local-family-is-contr A is-contr-A = is-equiv-is-contr ( precomp-Π f A) ( is-contr-Π is-contr-A) ( is-contr-Π (is-contr-A ∘ f)) - is-local-type-is-contr : - {l : Level} (A : UU l) → is-contr A → is-local-type A - is-local-type-is-contr A is-contr-A = + is-local-is-contr : + {l : Level} (A : UU l) → is-contr A → is-local f A + is-local-is-contr A is-contr-A = is-local-family-is-contr (λ _ → A) (λ _ → is-contr-A) ``` ### A type that is local at the unique map `empty → unit` is contractible ```agda -is-contr-is-local-type : - {l : Level} (A : UU l) → is-local-type (λ (_ : empty) → star) A → is-contr A -is-contr-is-local-type A is-local-type-A = +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 ( empty → A) ( λ a _ → a) @@ -177,7 +229,7 @@ is-contr-is-local-type A is-local-type-A = ( λ 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-type-A)) + ( is-equiv-map-inv-is-equiv (is-equiv-map-left-unit-law-Π (λ _ → A))) + ( is-local-A)) ( universal-property-empty' A) ``` diff --git a/src/orthogonal-factorization-systems/modal-operators.lagda.md b/src/orthogonal-factorization-systems/modal-operators.lagda.md index 706874a7b4..5af7c42d45 100644 --- a/src/orthogonal-factorization-systems/modal-operators.lagda.md +++ b/src/orthogonal-factorization-systems/modal-operators.lagda.md @@ -126,7 +126,7 @@ module _ ### Locally small modal operators -We say a modal operator is _locally small_ if it maps small types to locally +We say a modal operator is **locally small** if it maps small types to locally small types. ```agda diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md index 16b50d0ff5..8c93de6112 100644 --- a/src/orthogonal-factorization-systems/null-types.lagda.md +++ b/src/orthogonal-factorization-systems/null-types.lagda.md @@ -28,9 +28,8 @@ A type `A` is said to be **null at** `Y`, or **`Y`-null**, if the constant map const : A → (Y → A) ``` -is an equivalence. - -The idea is that _`A` observes the type `Y` to be contractible_. +is an equivalence. The idea is that _`A` observes the type `Y` to be +contractible_. ## Definition @@ -52,21 +51,21 @@ module _ {l1 l2 : Level} (Y : UU l1) (A : UU l2) where - is-local-is-null : is-null Y A → is-local-type (λ y → star) A + is-local-is-null : is-null Y A → is-local (λ y → star) A is-local-is-null = is-equiv-comp ( const Y A) ( map-left-unit-law-function-type A) ( is-equiv-map-left-unit-law-function-type A) - is-null-is-local : is-local-type (λ y → star) A → is-null Y A + is-null-is-local : is-local (λ y → star) A → is-null Y A is-null-is-local = is-equiv-comp ( precomp (λ y → star) A) ( map-inv-left-unit-law-function-type A) ( is-equiv-map-inv-left-unit-law-function-type A) - equiv-is-local-is-null : is-null Y A ≃ is-local-type (λ y → star) A + equiv-is-local-is-null : is-null Y A ≃ is-local (λ y → star) A equiv-is-local-is-null = equiv-prop ( is-property-is-equiv (const Y A)) @@ -74,6 +73,6 @@ module _ ( is-local-is-null) ( is-null-is-local) - equiv-is-null-is-local : is-local-type (λ y → star) A ≃ is-null Y A + equiv-is-null-is-local : is-local (λ y → star) A ≃ is-null Y A equiv-is-null-is-local = inv-equiv equiv-is-local-is-null ``` diff --git a/src/orthogonal-factorization-systems/open-modalities.lagda.md b/src/orthogonal-factorization-systems/open-modalities.lagda.md new file mode 100644 index 0000000000..ad9b8963c4 --- /dev/null +++ b/src/orthogonal-factorization-systems/open-modalities.lagda.md @@ -0,0 +1,133 @@ +# The open modalities + +```agda +module orthogonal-factorization-systems.open-modalities where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.identity-types +open import foundation.locally-small-types +open import foundation.propositions +open import foundation.universe-levels + +open import orthogonal-factorization-systems.higher-modalities +open import orthogonal-factorization-systems.modal-operators +open import orthogonal-factorization-systems.uniquely-eliminating-modalities +``` + +
+ +## Idea + +Given any proposition `Q`, the hom functor `Q →_` defines a +[higher modality](orthogonal-factorization-systems.higher-modalities.md). We +call these the **open modalities**. + +## Definition + +```agda +operator-open-modality : + (l : Level) {lQ : Level} (Q : Prop lQ) → operator-modality l (lQ ⊔ l) +operator-open-modality l Q X = type-Prop Q → X + +locally-small-operator-open-modality : + (l : Level) {lQ : Level} (Q : Prop lQ) → + locally-small-operator-modality l (lQ ⊔ l) (lQ ⊔ l) +pr1 (locally-small-operator-open-modality l Q) = operator-open-modality l Q +pr2 (locally-small-operator-open-modality l Q) X = is-locally-small' + +unit-open-modality : + {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-open-modality l Q) +unit-open-modality Q x _ = x +``` + +## Properties + +### The open modalities are higher modalities + +```agda +module _ + {l lQ : Level} (Q : Prop lQ) + where + + ind-open-modality : ind-modality {l} (unit-open-modality Q) + ind-open-modality X P f z q = + tr P (eq-htpy λ q' → ap z (eq-is-prop (is-prop-type-Prop Q))) (f (z q) q) + + compute-ind-open-modality : + compute-ind-modality {l} (unit-open-modality Q) (ind-open-modality) + compute-ind-open-modality X P f a = + eq-htpy + ( λ q → + ap + ( λ p → tr P p (f a q)) + ( ( ap + ( eq-htpy) + ( eq-htpy + ( λ _ → ap-const a (eq-is-prop (is-prop-type-Prop Q))))) ∙ + ( eq-htpy-refl-htpy (λ _ → a)))) + + dependent-universal-property-open-modality : + dependent-universal-property-modality {l} (unit-open-modality Q) + pr1 dependent-universal-property-open-modality = ind-open-modality + pr2 dependent-universal-property-open-modality = compute-ind-open-modality +``` + +For local smallness with respect to the appropriate universe level, we must take +the maximum of `l` and `lQ` as our domain. In practice, this allows `lQ` to be +smaller than `l`. + +```agda +module _ + (l : Level) {lQ : Level} (Q : Prop lQ) + where + + is-modal-identity-types-open-modality : + is-modal-identity-types + ( locally-small-operator-open-modality (l ⊔ lQ) Q) + ( unit-open-modality Q) + is-modal-identity-types-open-modality X x y = + is-equiv-has-inverse + ( λ z → eq-htpy (λ q → htpy-eq (z q) q)) + ( λ z → + eq-htpy + ( λ q → + ( ap + ( eq-htpy) + ( eq-htpy + ( λ q' → + ap + ( λ q'' → htpy-eq (z q'') q') + ( eq-is-prop (is-prop-type-Prop Q))))) ∙ + ( isretr-eq-htpy (z q)))) + ( isretr-eq-htpy) + + is-higher-modality-open-modality : + is-higher-modality + ( locally-small-operator-open-modality (l ⊔ lQ) Q) + ( unit-open-modality Q) + pr1 is-higher-modality-open-modality = + dependent-universal-property-open-modality Q + pr2 is-higher-modality-open-modality = + is-modal-identity-types-open-modality + + open-higher-modality : higher-modality (l ⊔ lQ) (l ⊔ lQ) + pr1 open-higher-modality = locally-small-operator-open-modality (l ⊔ lQ) Q + pr1 (pr2 open-higher-modality) = unit-open-modality Q + pr2 (pr2 open-higher-modality) = is-higher-modality-open-modality +``` + +### The open modalities are uniquely eliminating modalities + +```agda +is-uniquely-eliminating-modality-open-modality : + (l : Level) {lQ : Level} (Q : Prop lQ) → + is-uniquely-eliminating-modality {l ⊔ lQ} (unit-open-modality Q) +is-uniquely-eliminating-modality-open-modality l Q = + is-uniquely-eliminating-modality-higher-modality (open-higher-modality l Q) +``` diff --git a/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md index 6cc32209a2..9e69422044 100644 --- a/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-factorization-systems.lagda.md @@ -172,6 +172,14 @@ module _ is-prop-is-orthogonal-factorization-system ``` +### An orthogonal factorization system is uniquely determined by its right class + +This remains to be shown. + +### The right class of an orthogonal factorization system is pullback-stable + +This remains to be shown. + ## References - Egbert Rijke, Michael Shulman, Bas Spitters, _Modalities in homotopy type diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index 318d20cdec..ecc7e22287 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -19,12 +19,12 @@ open import orthogonal-factorization-systems.pullback-hom ## Idea -The map `f : A → X` is said to be _orthogonal to_ `g : B → Y` if the +The map `f : A → X` is said to be **orthogonal to** `g : B → Y` if their pullback-hom is an equivalence. This means that there is a unique lifting operation between `f` and `g`. -In this case we say that `f` is _left orthogonal_ to `g` and `g` is _right -orthogonal_ to `f`. +In this case we say that `f` is **left orthogonal** to `g` and `g` is **right +orthogonal** to `f`. ## Definition diff --git a/src/orthogonal-factorization-systems/raise-modalities.lagda.md b/src/orthogonal-factorization-systems/raise-modalities.lagda.md new file mode 100644 index 0000000000..bd3b959bff --- /dev/null +++ b/src/orthogonal-factorization-systems/raise-modalities.lagda.md @@ -0,0 +1,58 @@ +# The raise modalities + +```agda +module orthogonal-factorization-systems.raise-modalities where +``` + +
Imports + +```agda +open import foundation.functions +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.uniquely-eliminating-modalities +``` + +
+ +## Idea + +The operations of +[raising universe levels](foundation.raising-universe-levels.md) are trivially +[higher modalities](orthogonal-factorization-systems.higher-modalities.md), and +in the case that `l1 ⊔ l2 = l1`, we recover the +[identity modality](orthogonal-factorization-systems.identity-modality.md). + +## Definition + +```agda +operator-raise-modality : + (l1 l2 : Level) → operator-modality l1 (l1 ⊔ l2) +operator-raise-modality l1 l2 = raise l2 + +unit-raise-modality : + {l1 l2 : Level} → unit-modality (operator-raise-modality l1 l2) +unit-raise-modality = map-raise +``` + +## Properties + +### The raise modality is a uniquely eliminating modality + +```agda +is-uniquely-eliminating-modality-raise-modality : + {l1 l2 : Level} → + is-uniquely-eliminating-modality (unit-raise-modality {l1} {l2}) +is-uniquely-eliminating-modality-raise-modality {l1} {l2} _ P = + is-local-family-is-equiv + ( unit-raise-modality) + ( is-equiv-map-raise) + ( operator-raise-modality l1 l2 ∘ P) +``` + +### In the case that `l1 ⊔ l2 = l1` we recover the trivial modality + +This remains to be made formal. diff --git a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md index 7c9b5e91f8..e4b10c4a83 100644 --- a/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-subuniverses.lagda.md @@ -38,7 +38,7 @@ module _ is-reflective-subuniverse = ( (X : UU l) → type-Prop (is-modal' (○ X))) × ( (X : UU l) → type-Prop (is-modal' X) → - (Y : UU l) → is-local-type (unit-○ {Y}) X) + (Y : UU l) → is-local (unit-○ {Y}) X) reflective-subuniverse : (l lM : Level) → UU (lsuc l ⊔ lsuc lM) reflective-subuniverse l lM = diff --git a/src/orthogonal-factorization-systems/separated-types.lagda.md b/src/orthogonal-factorization-systems/separated-types.lagda.md new file mode 100644 index 0000000000..ef8cd09957 --- /dev/null +++ b/src/orthogonal-factorization-systems/separated-types.lagda.md @@ -0,0 +1,33 @@ +# Separated types + +```agda +module orthogonal-factorization-systems.separated-types where +``` + +
Imports + +```agda +open import foundation.identity-types +open import foundation.universe-levels + +open import orthogonal-factorization-systems.local-types +``` + +
+ +## Idea + +A type `A` is said to be **separated** with respect to a map `f`, or +**`f`-separated**, if its identity types are +[`f`-local](orthogonal-factorization-systems.local-types.md). + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (f : X → Y) (A : UU l3) + where + + is-separated : UU (l1 ⊔ l2 ⊔ l3) + is-separated = (x y : A) → is-local f (x ＝ y) +``` diff --git a/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md index 210de3ea91..05e81795a0 100644 --- a/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md @@ -17,8 +17,9 @@ open import orthogonal-factorization-systems.orthogonal-factorization-systems ## Idea -A **stable orthogonal factorization system** is an orthogonal factorization -system whose left class is stable under pullbacks. +A **stable orthogonal factorization system**, or **stable factorization system** +for short, is an orthogonal factorization system whose left class is stable +under pullbacks. The right class of an orthogonal factorization system is always stable under pullbacks. diff --git a/src/orthogonal-factorization-systems/zero-modality.lagda.md b/src/orthogonal-factorization-systems/zero-modality.lagda.md new file mode 100644 index 0000000000..6bcd14b7c9 --- /dev/null +++ b/src/orthogonal-factorization-systems/zero-modality.lagda.md @@ -0,0 +1,55 @@ +# The zero modality + +```agda +module orthogonal-factorization-systems.zero-modality where +``` + +
Imports + +```agda +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.uniquely-eliminating-modalities +``` + +
+ +## Idea + +The **zero modality** is the +[modality](orthogonal-factorization-systems.higher-modalities.md) that maps +every type to the [unit type](foundation.unit-type.md). + +## Definition + +```agda +operator-zero-modality : + (l1 l2 : Level) → operator-modality l1 l2 +operator-zero-modality l1 l2 _ = raise-unit l2 + +unit-zero-modality : + {l1 l2 : Level} → unit-modality (operator-zero-modality l1 l2) +unit-zero-modality _ = raise-star +``` + +## Properties + +### The zero modality is a uniquely eliminating modality + +```agda +is-uniquely-eliminating-modality-zero-modality : + {l1 l2 : Level} → + is-uniquely-eliminating-modality (unit-zero-modality {l1} {l2}) +is-uniquely-eliminating-modality-zero-modality {l2 = l2} A P = + is-local-is-contr + ( unit-zero-modality) + ( raise-unit l2) + ( is-contr-raise-unit) +``` + +### The zero modality is equivalent to `-2`-truncation + +This remains to be made formal. diff --git a/src/ring-theory/ideals-semirings.lagda.md b/src/ring-theory/ideals-semirings.lagda.md index 1050dd42fa..827486e542 100644 --- a/src/ring-theory/ideals-semirings.lagda.md +++ b/src/ring-theory/ideals-semirings.lagda.md @@ -32,7 +32,7 @@ the left/right). This is the standard definition of ideals in semirings. However, such two-sided ideals do not correspond uniquely to congruences on `R`. If we ask in addition that the underlying additive submodule is normal, then we get unique -correspondence to congruences. We will call such ideals _normal_. +correspondence to congruences. We will call such ideals **normal**. ## Definitions diff --git a/src/structured-types/involutive-type-of-h-space-structures.lagda.md b/src/structured-types/involutive-type-of-h-space-structures.lagda.md index 1d0aff03a7..1ed09802fa 100644 --- a/src/structured-types/involutive-type-of-h-space-structures.lagda.md +++ b/src/structured-types/involutive-type-of-h-space-structures.lagda.md @@ -1,4 +1,4 @@ -# The involutive type of H-Space structures on a pointed type +# The involutive type of H-space structures on a pointed type ```agda module structured-types.involutive-type-of-h-space-structures where @@ -30,7 +30,7 @@ open import univalent-combinatorics.2-element-types ## Idea -We construct the involutive type of H-Space structures on a pointed type +We construct the **involutive type of H-space structures** on a pointed type. ## Definition diff --git a/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md index 3f76efdf50..1c30f3a62e 100644 --- a/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-spans-of-pointed-types.lagda.md @@ -23,8 +23,8 @@ open import synthetic-homotopy-theory.cocones-under-spans ## Idea -A cocone under a span of pointed types is _pointed_ if it consists of pointed -maps such that the proofs of point-preservation cohere. +A cocone under a span of pointed types is a **pointed cocone** if it consists of +pointed maps such that the proofs of point-preservation cohere. The type of pointed cocones under a span of pointed types is again canonically pointed at the constant cocone, with `refl` as coherence proof. diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md index d8cebd0dcc..5077c6bab6 100644 --- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md @@ -86,7 +86,7 @@ htpy-cocone : (f : S → A) (g : S → B) {X : UU l4} → cocone f g X → cocone f g X → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) htpy-cocone f g c c' = - Σ ((horizontal-map-cocone f g c) ~ (horizontal-map-cocone f g c')) + Σ ( horizontal-map-cocone f g c ~ horizontal-map-cocone f g c') ( λ K → Σ ( vertical-map-cocone f g c ~ vertical-map-cocone f g c') ( coherence-htpy-cocone f g c c' K)) @@ -113,15 +113,15 @@ is-contr-total-htpy-cocone f g c = is-contr-total-Eq-structure ( λ i' jH' K → Σ ( vertical-map-cocone f g c ~ (pr1 jH')) - ( coherence-htpy-cocone f g c (pair i' jH') K)) + ( coherence-htpy-cocone f g c (i' , jH') K)) ( is-contr-total-htpy (horizontal-map-cocone f g c)) - ( pair (horizontal-map-cocone f g c) refl-htpy) + ( horizontal-map-cocone f g c , refl-htpy) ( is-contr-total-Eq-structure ( λ j' H' → coherence-htpy-cocone f g c - ( pair (horizontal-map-cocone f g c) (pair j' H')) + ( horizontal-map-cocone f g c , j' , H') ( refl-htpy)) ( is-contr-total-htpy (vertical-map-cocone f g c)) - ( pair (vertical-map-cocone f g c) refl-htpy) + ( vertical-map-cocone f g c , refl-htpy) ( is-contr-is-equiv' ( Σ ( ( horizontal-map-cocone f g c ∘ f) ~ ( vertical-map-cocone f g c ∘ g)) @@ -170,7 +170,7 @@ cocone-map-comp : (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) {Y : UU l5} (h : X → Y) {Z : UU l6} (k : Y → Z) → Id (cocone-map f g c (k ∘ h)) (cocone-map f g (cocone-map f g c h) k) -cocone-map-comp f g (pair i (pair j H)) h k = +cocone-map-comp f g (i , j , H) h k = eq-pair-Σ refl (eq-pair-Σ refl (eq-htpy (ap-comp k h ∘ H))) ``` diff --git a/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md b/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md index 8724800b6e..07921e3055 100644 --- a/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md +++ b/src/synthetic-homotopy-theory/groups-of-loops-in-1-types.lagda.md @@ -1,4 +1,4 @@ -# Groups of loops in 1-types +# Groups of loops in `1`-types ```agda module synthetic-homotopy-theory.groups-of-loops-in-1-types where diff --git a/src/synthetic-homotopy-theory/joins-of-types.lagda.md b/src/synthetic-homotopy-theory/joins-of-types.lagda.md index eb8458f791..f763b58e16 100644 --- a/src/synthetic-homotopy-theory/joins-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/joins-of-types.lagda.md @@ -49,11 +49,15 @@ cocone-join : cocone-join A B = cocone-pushout pr1 pr2 up-join : - {l1 l2 : Level} (A : UU l1) (B : UU l2) → - ( {l : Level} → universal-property-pushout l - ( pr1 {A = A} {B = λ x → B}) pr2 (cocone-join A B)) + {l1 l2 : Level} (A : UU l1) (B : UU l2) + {l : Level} → universal-property-pushout l pr1 pr2 (cocone-join A B) up-join A B = up-pushout pr1 pr2 +equiv-up-join : + {l1 l2 : Level} (A : UU l1) (B : UU l2) + {l : Level} (X : UU l) → (A * B → X) ≃ cocone pr1 pr2 X +equiv-up-join A B = equiv-up-pushout pr1 pr2 + inl-join : {l1 l2 : Level} (A : UU l1) (B : UU l2) → A → A * B inl-join A B = pr1 (cocone-join A B) diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index fd9cfb36bb..de80718962 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -90,55 +90,38 @@ is-pushout f g c = is-equiv (cogap f g c) ### Computation with the cogap map ```agda -compute-inl-cogap : +module _ { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} - ( f : S → A) (g : S → B) → + ( f : S → A) (g : S → B) { X : UU l4} (c : cocone f g X) - ( a : A) → cogap f g c (inl-pushout f g a) ＝ horizontal-map-cocone f g c a -compute-inl-cogap f g c = - pr1 - ( htpy-cocone-map-universal-property-pushout - ( f) - ( g) - ( cocone-pushout f g) - ( up-pushout f g) - ( c)) - -compute-inr-cogap : - { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} - ( f : S → A) (g : S → B) → - { X : UU l4} (c : cocone f g X) - ( b : B) → cogap f g c (inr-pushout f g b) ＝ vertical-map-cocone f g c b -compute-inr-cogap f g c = - pr1 - ( pr2 - ( htpy-cocone-map-universal-property-pushout + where + + private + htpy-cc = + htpy-cocone-map-universal-property-pushout ( f) ( g) ( cocone-pushout f g) ( up-pushout f g) - ( c))) - -compute-glue-cogap : - { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} - ( f : S → A) (g : S → B) → - { X : UU l4} (c : cocone f g X) - ( s : S) → - ( ap (cogap f g c) (glue-pushout f g s)) ＝ - ( ( compute-inl-cogap f g c (f s) ∙ coherence-square-cocone f g c s) ∙ - ( inv (compute-inr-cogap f g c (g s)))) -compute-glue-cogap f g c s = - con-inv - ( ap (cogap f g c) (glue-pushout f g s)) - ( compute-inr-cogap f g c (g s)) - ( compute-inl-cogap f g c (f s) ∙ coherence-square-cocone f g c s) - ( pr2 - ( pr2 - ( htpy-cocone-map-universal-property-pushout - ( f) - ( g) - ( cocone-pushout f g) - ( up-pushout f g) - ( c))) - ( s)) + ( c) + + compute-inl-cogap : + ( a : A) → cogap f g c (inl-pushout f g a) ＝ horizontal-map-cocone f g c a + compute-inl-cogap = pr1 htpy-cc + + compute-inr-cogap : + ( b : B) → cogap f g c (inr-pushout f g b) ＝ vertical-map-cocone f g c b + compute-inr-cogap = pr1 (pr2 htpy-cc) + + compute-glue-cogap : + ( s : S) → + ( ap (cogap f g c) (glue-pushout f g s)) ＝ + ( ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s) ∙ + ( inv (compute-inr-cogap (g s)))) + compute-glue-cogap s = + con-inv + ( ap (cogap f g c) (glue-pushout f g s)) + ( compute-inr-cogap (g s)) + ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s) + ( pr2 (pr2 htpy-cc) s) ``` diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md index 6c5ad6dfe3..113a7a0e03 100644 --- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md @@ -93,19 +93,19 @@ which states that the above square is a pullback. cone-pullback-property-pushout : {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (Y : UU l) → - cone (λ (h : A → Y) → h ∘ f) (λ (h : B → Y) → h ∘ g) (X → Y) -pr1 (cone-pullback-property-pushout f g {X} c Y) = + cone (_∘ f) (_∘ g) (X → Y) +pr1 (cone-pullback-property-pushout f g c Y) = precomp (horizontal-map-cocone f g c) Y -pr1 (pr2 (cone-pullback-property-pushout f g {X} c Y)) = +pr1 (pr2 (cone-pullback-property-pushout f g c Y)) = precomp (vertical-map-cocone f g c) Y -pr2 (pr2 (cone-pullback-property-pushout f g {X} c Y)) = +pr2 (pr2 (cone-pullback-property-pushout f g c Y)) = htpy-precomp (coherence-square-cocone f g c) Y pullback-property-pushout : {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l) -pullback-property-pushout l {S} {A} {B} f g {X} c = +pullback-property-pushout l f g c = (Y : UU l) → is-pullback ( precomp f Y) @@ -127,7 +127,7 @@ module _ triangle-map-cocone : { l6 : Level} (Z : UU l6) → - ( cocone-map f g d) ~ ((cocone-map f g c) ∘ (λ (k : Y → Z) → k ∘ h)) + ( cocone-map f g d) ~ (cocone-map f g c ∘ precomp h Z) triangle-map-cocone Z k = inv ( ( cocone-map-comp f g c h k) ∙ @@ -214,10 +214,9 @@ triangle-pullback-property-pushout-universal-property-pushout : {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → {l : Level} (Y : UU l) → ( cocone-map f g c) ~ - ( ( tot (λ i' → tot (λ j' p → htpy-eq p))) ∘ - ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y))) -triangle-pullback-property-pushout-universal-property-pushout - {S = S} {A = A} {B = B} f g c Y h = + ( ( tot (λ i' → tot (λ j' → htpy-eq))) ∘ + ( gap (_∘ f) (_∘ g) (cone-pullback-property-pushout f g c Y))) +triangle-pullback-property-pushout-universal-property-pushout f g c Y h = eq-pair-Σ refl ( eq-pair-Σ refl ( inv (issec-eq-htpy (h ·l coherence-square-cocone f g c)))) @@ -226,12 +225,11 @@ pullback-property-pushout-universal-property-pushout : {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → universal-property-pushout l f g c → pullback-property-pushout l f g c -pullback-property-pushout-universal-property-pushout - l f g c up-c Y = +pullback-property-pushout-universal-property-pushout l f g c up-c Y = is-equiv-right-factor-htpy ( cocone-map f g c) - ( tot (λ i' → tot (λ j' p → htpy-eq p))) - ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y)) + ( tot (λ i' → tot (λ j' → htpy-eq))) + ( gap (_∘ f) (_∘ g) (cone-pullback-property-pushout f g c Y)) ( triangle-pullback-property-pushout-universal-property-pushout f g c Y) ( is-equiv-tot-is-fiberwise-equiv ( λ i' → is-equiv-tot-is-fiberwise-equiv @@ -242,12 +240,11 @@ universal-property-pushout-pullback-property-pushout : {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → pullback-property-pushout l f g c → universal-property-pushout l f g c -universal-property-pushout-pullback-property-pushout - l f g c pb-c Y = +universal-property-pushout-pullback-property-pushout l f g c pb-c Y = is-equiv-comp-htpy ( cocone-map f g c) - ( tot (λ i' → tot (λ j' p → htpy-eq p))) - ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y)) + ( tot (λ i' → tot (λ j' → htpy-eq))) + ( gap (_∘ f) (_∘ g) (cone-pullback-property-pushout f g c Y)) ( triangle-pullback-property-pushout-universal-property-pushout f g c Y) ( pb-c Y) ( is-equiv-tot-is-fiberwise-equiv @@ -263,17 +260,16 @@ is-equiv-universal-property-pushout : (f : S → A) (g : S → B) (c : cocone f g C) → is-equiv f → ({l : Level} → universal-property-pushout l f g c) → is-equiv (pr1 (pr2 c)) -is-equiv-universal-property-pushout - {A = A} {B} f g (pair i (pair j H)) is-equiv-f up-c = +is-equiv-universal-property-pushout f g (i , j , H) is-equiv-f up-c = is-equiv-is-equiv-precomp j ( λ l T → is-equiv-is-pullback' - ( λ (h : A → T) → h ∘ f) - ( λ (h : B → T) → h ∘ g) - ( cone-pullback-property-pushout f g (pair i (pair j H)) T) + ( _∘ f) + ( _∘ g) + ( cone-pullback-property-pushout f g (i , j , H) T) ( is-equiv-precomp-is-equiv f is-equiv-f T) ( pullback-property-pushout-universal-property-pushout - l f g (pair i (pair j H)) up-c T)) + l f g (i , j , H) up-c T)) equiv-universal-property-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4} @@ -296,12 +292,12 @@ universal-property-pushout-is-equiv : is-equiv f → is-equiv (pr1 (pr2 c)) → ({l : Level} → universal-property-pushout l f g c) universal-property-pushout-is-equiv - f g (pair i (pair j H)) is-equiv-f is-equiv-j {l} = - let c = (pair i (pair j H)) in + f g (i , j , H) is-equiv-f is-equiv-j {l} = + let c = (i , j , H) in universal-property-pushout-pullback-property-pushout l f g c ( λ T → is-pullback-is-equiv' - ( λ h → h ∘ f) - ( λ h → h ∘ g) + ( _∘ f) + ( _∘ g) ( cone-pullback-property-pushout f g c T) ( is-equiv-precomp-is-equiv f is-equiv-f T) ( is-equiv-precomp-is-equiv j is-equiv-j T)) @@ -333,24 +329,22 @@ equiv-universal-property-pushout' : (f : S → A) (e : S ≃ B) (c : cocone f (map-equiv e) C) → ({l : Level} → universal-property-pushout l f (map-equiv e) c) → A ≃ C -equiv-universal-property-pushout' f e c up-c = - pair - ( pr1 c) - ( is-equiv-universal-property-pushout' - ( f) - ( map-equiv e) - ( c) - ( is-equiv-map-equiv e) - ( up-c)) +pr1 (equiv-universal-property-pushout' f e c up-c) = pr1 c +pr2 (equiv-universal-property-pushout' f e c up-c) = + is-equiv-universal-property-pushout' + ( f) + ( map-equiv e) + ( c) + ( is-equiv-map-equiv e) + ( up-c) universal-property-pushout-is-equiv' : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4} (f : S → A) (g : S → B) (c : cocone f g C) → is-equiv g → is-equiv (pr1 c) → ({l : Level} → universal-property-pushout l f g c) -universal-property-pushout-is-equiv' - f g (pair i (pair j H)) is-equiv-g is-equiv-i {l} = - let c = (pair i (pair j H)) in +universal-property-pushout-is-equiv' f g (i , j , H) is-equiv-g is-equiv-i {l} = + let c = (i , j , H) in universal-property-pushout-pullback-property-pushout l f g c ( λ T → is-pullback-is-equiv ( precomp f T) diff --git a/src/trees/planar-binary-trees.lagda.md b/src/trees/planar-binary-trees.lagda.md index 5299e671a6..a717bc8137 100644 --- a/src/trees/planar-binary-trees.lagda.md +++ b/src/trees/planar-binary-trees.lagda.md @@ -19,9 +19,9 @@ open import trees.w-types ## Idea -A planar binary tree is a binary tree in which the branchings are labelled by -the booleans. The idea is that at any branching point in a planar binary tree, -we know which branch goes to the left and which branch goes to the right. +A planar binary tree is a binary tree in which the branchings are labeled by the +booleans. The idea is that at any branching point in a planar binary tree, we +know which branch goes to the left and which branch goes to the right. Planar binary trees are commonly called binary trees, but in univalent mathematics it makes sense to recognize that the branching points in a binary diff --git a/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md b/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md index 21fa76d696..d19830aaa6 100644 --- a/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/2-element-decidable-subtypes.lagda.md @@ -1,4 +1,4 @@ -# 2-element decidable subtypes +# `2`-element decidable subtypes ```agda module univalent-combinatorics.2-element-decidable-subtypes where diff --git a/src/univalent-combinatorics/2-element-subtypes.lagda.md b/src/univalent-combinatorics/2-element-subtypes.lagda.md index 7a31a6f207..ee89102588 100644 --- a/src/univalent-combinatorics/2-element-subtypes.lagda.md +++ b/src/univalent-combinatorics/2-element-subtypes.lagda.md @@ -1,4 +1,4 @@ -# 2-element subtypes +# `2`-element subtypes ```agda module univalent-combinatorics.2-element-subtypes where diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md index 377ce08aa1..7b7f0aa502 100644 --- a/src/univalent-combinatorics/2-element-types.lagda.md +++ b/src/univalent-combinatorics/2-element-types.lagda.md @@ -1,4 +1,4 @@ -# 2-element types +# `2`-element types ```agda module univalent-combinatorics.2-element-types where diff --git a/src/univalent-combinatorics/discrete-sigma-decompositions.lagda.md b/src/univalent-combinatorics/discrete-sigma-decompositions.lagda.md index d374d99b07..312be1116a 100644 --- a/src/univalent-combinatorics/discrete-sigma-decompositions.lagda.md +++ b/src/univalent-combinatorics/discrete-sigma-decompositions.lagda.md @@ -1,4 +1,4 @@ -# Finite discrete Σ-Decompositions +# Finite discrete Σ-decompositions ```agda module univalent-combinatorics.discrete-sigma-decompositions where diff --git a/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md b/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md index e3a191db03..10323c731a 100644 --- a/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md +++ b/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md @@ -1,4 +1,4 @@ -# Set quotients of index 2 +# Set quotients of index `2` ```agda {-# OPTIONS --lossy-unification #-} diff --git a/src/univalent-combinatorics/sigma-decompositions.lagda.md b/src/univalent-combinatorics/sigma-decompositions.lagda.md index 813a0c1efe..91d811d9c4 100644 --- a/src/univalent-combinatorics/sigma-decompositions.lagda.md +++ b/src/univalent-combinatorics/sigma-decompositions.lagda.md @@ -115,7 +115,7 @@ module _ matching-correspondence-Σ-Decomposition-𝔽 ``` -### Fibered double finite Σ-Decompositions +### Fibered double finite Σ-decompositions ```agda fibered-Σ-Decomposition-𝔽 : @@ -210,7 +210,7 @@ module _ ( is-finite-Decidable-Equivalence-Relation-𝔽 A) ``` -### Characterization of the equality of finite Σ-Decompositions +### Characterization of the equality of finite Σ-decompositions ```agda module _ diff --git a/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md b/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md index 33dcd644f6..d59f39a167 100644 --- a/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md +++ b/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md @@ -1,4 +1,4 @@ -# Finite trivial Σ-Decompositions +# Finite trivial Σ-decompositions ```agda module univalent-combinatorics.trivial-sigma-decompositions where diff --git a/src/univalent-combinatorics/unions-subtypes.lagda.md b/src/univalent-combinatorics/unions-subtypes.lagda.md index f11de794ff..6bd7943bdd 100644 --- a/src/univalent-combinatorics/unions-subtypes.lagda.md +++ b/src/univalent-combinatorics/unions-subtypes.lagda.md @@ -1,4 +1,4 @@ -# Union of finite subtypes +# Unions of finite subtypes ```agda module univalent-combinatorics.unions-subtypes where diff --git a/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md b/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md index 61903d61c8..15be09ace3 100644 --- a/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md +++ b/src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md @@ -1,4 +1,4 @@ -# Unlabelled rooted trees +# Unlabeled rooted trees ```agda module univalent-combinatorics.unlabeled-rooted-trees where @@ -14,7 +14,7 @@ module univalent-combinatorics.unlabeled-rooted-trees where ## Idea -An unlabelled rooted tree is an unlabelled tree equipped with a vertex. +An unlabeled rooted tree is an unlabeled tree equipped with a vertex. ## Definition diff --git a/src/univalent-combinatorics/unlabeled-trees.lagda.md b/src/univalent-combinatorics/unlabeled-trees.lagda.md index 852e43a9b1..7dd78c36ac 100644 --- a/src/univalent-combinatorics/unlabeled-trees.lagda.md +++ b/src/univalent-combinatorics/unlabeled-trees.lagda.md @@ -1,4 +1,4 @@ -# Unlabelled trees +# Unlabeled trees ```agda module univalent-combinatorics.unlabeled-trees where @@ -14,5 +14,5 @@ module univalent-combinatorics.unlabeled-trees where ## Idea -An unlabelled tree is an undirected graph `G` such that any cycle in `G` must +An unlabeled tree is an undirected graph `G` such that any cycle in `G` must have length 1.