From ecbdd480354c4317f0c0893531c584aeb59bc96f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 23 Sep 2024 22:21:25 +0200 Subject: [PATCH] Some typos, wording improvements, and brief prose additions (#1186) - Change namespace header wording from ```md ## Files in the ... folder ``` to ```md ## Modules in the ... namespace ``` - Improve typesetting and wording in `foundation.telescopes` - Add brief main module introduction to `modal-type-theory` - Add a remark about polymorphism in module about the precategory of posets - A series of miscellaneous typo fixes --- scripts/fix_imports.py | 2 +- src/category-theory.lagda.md | 2 +- src/commutative-algebra.lagda.md | 2 +- src/elementary-number-theory.lagda.md | 2 +- src/finite-algebra.lagda.md | 2 +- src/finite-group-theory.lagda.md | 2 +- src/foundation-core.lagda.md | 2 +- src/foundation.lagda.md | 2 +- src/foundation/telescopes.lagda.md | 57 ++++++++++--------- src/graph-theory.lagda.md | 2 +- src/group-theory.lagda.md | 2 +- src/higher-group-theory.lagda.md | 2 +- src/linear-algebra.lagda.md | 2 +- src/lists.lagda.md | 2 +- src/modal-type-theory.lagda.md | 15 ++++- ...ction-on-homotopies-flat-modality.lagda.md | 5 +- ...n-identifications-crisp-functions.lagda.md | 6 +- ...-on-identifications-flat-modality.lagda.md | 5 +- .../crisp-dependent-pair-types.lagda.md | 6 +- .../crisp-law-of-excluded-middle.lagda.md | 3 +- src/modal-type-theory/crisp-types.lagda.md | 15 ++--- .../flat-discrete-crisp-types.lagda.md | 28 ++++----- src/modal-type-theory/flat-modality.lagda.md | 5 +- .../flat-sharp-adjunction.lagda.md | 8 ++- .../functoriality-flat-modality.lagda.md | 12 ++++ .../sharp-codiscrete-types.lagda.md | 2 +- src/modal-type-theory/sharp-modality.lagda.md | 4 ++ ...roperty-flat-discrete-crisp-types.lagda.md | 3 +- ...encyclopedia-of-integer-sequences.lagda.md | 2 +- src/order-theory.lagda.md | 2 +- src/order-theory/large-suplattices.lagda.md | 10 ++-- ...ategory-of-decidable-total-orders.lagda.md | 2 +- .../precategory-of-posets.lagda.md | 12 +++- .../precategory-of-total-orders.lagda.md | 2 +- src/organic-chemistry.lagda.md | 4 +- src/orthogonal-factorization-systems.lagda.md | 2 +- src/polytopes.lagda.md | 2 +- src/primitives.lagda.md | 2 +- src/real-numbers.lagda.md | 2 +- src/reflection.lagda.md | 2 +- src/ring-theory.lagda.md | 2 +- src/ring-theory/precategory-of-rings.lagda.md | 2 +- src/set-theory.lagda.md | 2 +- src/species.lagda.md | 2 +- src/structured-types.lagda.md | 2 +- .../wild-category-of-pointed-types.lagda.md | 2 +- src/synthetic-category-theory.lagda.md | 2 +- src/synthetic-homotopy-theory.lagda.md | 2 +- .../eckmann-hilton-argument.lagda.md | 7 ++- src/type-theories.lagda.md | 2 +- src/univalent-combinatorics.lagda.md | 2 +- .../dedekind-finite-sets.lagda.md | 2 +- .../kuratowski-finite-sets.lagda.md | 2 +- src/universal-algebra.lagda.md | 2 +- src/wild-category-theory.lagda.md | 2 +- 55 files changed, 164 insertions(+), 115 deletions(-) diff --git a/scripts/fix_imports.py b/scripts/fix_imports.py index b6760c4a7f..d83b827013 100755 --- a/scripts/fix_imports.py +++ b/scripts/fix_imports.py @@ -145,7 +145,7 @@ def prettify_imports_block(block): agdaBlockStart = utils.find_index(contents, '```agda') if len(agdaBlockStart) > 1: - print('Warning: No Agda import block found inside
block in:\n\t' + + print('Warning: No Agda import block found inside `
` block in:\n\t' + str(fpath), file=sys.stderr) status |= FLAG_NO_IMPORT_BLOCK continue diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index d1810f3b3b..e4bb19aab7 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -8,7 +8,7 @@ {{#include tables/precategories.md}} -## Files in the category theory folder +## Modules in the category theory namespace ```agda module category-theory where diff --git a/src/commutative-algebra.lagda.md b/src/commutative-algebra.lagda.md index 0eceedfe0f..7719d0d4d2 100644 --- a/src/commutative-algebra.lagda.md +++ b/src/commutative-algebra.lagda.md @@ -1,6 +1,6 @@ # Commutative algebra -## Files in the commutative algebra folder +## Modules in the commutative algebra namespace ```agda module commutative-algebra where diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 25b7f236ba..99f0184e5d 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -1,6 +1,6 @@ # Elementary number theory -## Files in the elementary number theory folder +## Modules in the elementary number theory namespace ```agda module elementary-number-theory where diff --git a/src/finite-algebra.lagda.md b/src/finite-algebra.lagda.md index 359239c09d..3e2d66d204 100644 --- a/src/finite-algebra.lagda.md +++ b/src/finite-algebra.lagda.md @@ -1,6 +1,6 @@ # Finite algebra -## Files in the finite algebra folder +## Modules in the finite algebra namespace ```agda module finite-algebra where diff --git a/src/finite-group-theory.lagda.md b/src/finite-group-theory.lagda.md index e618f005a3..8c555ee159 100644 --- a/src/finite-group-theory.lagda.md +++ b/src/finite-group-theory.lagda.md @@ -1,6 +1,6 @@ # Finite group theory -## Files in the finite group theory folder +## Modules in the finite group theory namespace ```agda module finite-group-theory where diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index fc536f02cc..9b9dd2512c 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -1,6 +1,6 @@ # Foundation core -## Files in the foundation-core folder +## Modules in the foundation-core namespace ```agda module foundation-core where diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 16ab4ee134..b892a43bab 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -4,7 +4,7 @@ {-# OPTIONS --guardedness #-} ``` -## Files in the foundation folder +## Modules in the foundation namespace ```agda module foundation where diff --git a/src/foundation/telescopes.lagda.md b/src/foundation/telescopes.lagda.md index 30521fa62b..7c88a0a1a7 100644 --- a/src/foundation/telescopes.lagda.md +++ b/src/foundation/telescopes.lagda.md @@ -16,35 +16,36 @@ open import foundation.universe-levels ## Idea -A **telescope**, or **iterated type family**, is a list of type families -`(A₀, A₁, A₂, ..., A_n)` consisting of +A {{#concept "telescope" Disambiguation="of types" Agda=telescope}}, or +**iterated type family**, is a list of type families `(A₀, A₁, A₂, …, Aₙ)` +consisting of - a type `A₀`, - a type family `A₁ : A₀ → 𝒰`, - a type family `A₂ : (x₀ : A₀) → A₁ x₀ → 𝒰`, -- ... -- a type family `A_n : (x₀ : A₀) ... (x_(n-1) : A_(n-1) x₀ ... x_(n-2)) → 𝒰`. +- ⋮ +- a type family `Aₙ : (x₀ : A₀) ⋯ (xₙ₋₁ : Aₙ₋₁ x₀ ⋯ xₙ₋₂) → 𝒰`. -We say that a telescope `(A₀,...,A_n)` has **length** `n+1`. In other words, the -length of the telescope `(A₀,...,A_n)` is the length of the (dependent) list -`(A₀,...,A_n)`. +We say that a telescope `(A₀, …, Aₙ)` has **length** `n+1`. In other words, the +length of the telescope `(A₀, …, Aₙ)` is the length of the (dependent) list +`(A₀, …, Aₙ)`. We encode the type of telescopes as a family of inductive types ```text - telescope : (l : Level) → ℕ → UUω + telescope : (l : Level) → ℕ → UUω. ``` The type of telescopes is a [directed tree](trees.directed-trees.md) ```text - ... → T₃ → T₂ → T₁ → T₀, + ⋯ → T₃ → T₂ → T₁ → T₀, ``` -where `T_n` is the type of all telescopes of length `n`, and the map from -`T_(n+1)` to `T_n` maps `(A₀,...,A_n)` to `(A₀,...,A_(n-1))`. The type of such -directed trees can be defined as a coinductive record type, and we will define -the tree `T` of telescopes as a particular element of this tree. +where `Tₙ` is the type of all telescopes of length `n`, and the map from `Tₙ₊₁` +to `Tₙ` maps `(A₀, …, Aₙ)` to `(A₀, …, Aₙ₋₁)`. The type of such directed trees +can be defined as a coinductive record type, and we will define the tree `T` of +telescopes as a particular element of this tree. ## Definitions @@ -61,11 +62,7 @@ data (X → telescope l2 n) → telescope (l1 ⊔ l2) (succ-ℕ n) open telescope public -``` - -A very slight reformulation of `cons-telescope` for convenience: -```agda prepend-telescope : {l1 l2 : Level} {n : ℕ} → (A : UU l1) → ({x : A} → telescope l2 n) → telescope (l1 ⊔ l2) (succ-ℕ n) @@ -76,9 +73,9 @@ prepend-telescope A B = cons-telescope {X = A} (λ x → B {x}) One issue with the previous definition of telescopes is that it is impossible to extract any type information from it. At the expense of giving up full universe -polymorphism, we can define a notion of **telescopes at a universe level** that -admits such projections. This definition is also compatible with the -`--level-universe` restriction. +polymorphism, we can define **telescopes at a universe level**. These admit such +projections, and are moreover compatible with the `--level-universe` +restriction. ```agda data telescope-Level (l : Level) : ℕ → UU (lsuc l) @@ -114,17 +111,17 @@ apply-base-telescope P (cons-telescope A) = ### Telescopes as instance arguments -To get Agda to infer telescopes, we help it along a little using +To have Agda infer telescopes, we help it along using [instance arguments](https://agda.readthedocs.io/en/latest/language/instance-arguments.html). -These are a special kind of implicit argument in Agda that are resolved by the -instance resolution algorithm. We register building blocks for this algorithm to -use below, i.e. _instances_. Then Agda will attempt to use those to construct +These are a special kind of implicit argument that are resolved by _the instance +resolution algorithm_. We register building blocks, called _instances_, for this +algorithm to use below. Then Agda will attempt to use those to construct telescopes of the appropriate kind when asked to. -In the case of telescopes, this has the unfortunate disadvantage that we can -only define instances for fixed length telescopes. We have defined instances of -telescopes up to length 18, so although Agda cannot infer a telescope of a -general length using this approach, it can infer them up to this given length. +In the case of telescopes, this has the disadvantage that we can only define +instances for fixed length telescopes. We have defined instances of telescopes +up to length 18, so although Agda cannot infer a telescope of a general length +using this approach, it can infer them up to this given length. ```agda instance-telescope : {l : Level} {n : ℕ} → {{telescope l n}} → telescope l n @@ -912,3 +909,7 @@ instance - [Dependent telescopes](foundation.dependent-telescopes.md) - [Iterated Σ-types](foundation.iterated-dependent-pair-types.md) - [Iterated Π-types](foundation.iterated-dependent-product-types.md) + +## External links + +- [type telescope](https://ncatlab.org/nlab/show/type+telescope) at $n$Lab diff --git a/src/graph-theory.lagda.md b/src/graph-theory.lagda.md index e03916e255..9ac8fd5589 100644 --- a/src/graph-theory.lagda.md +++ b/src/graph-theory.lagda.md @@ -1,6 +1,6 @@ # Graph theory -## Files in the graph theory folder +## Modules in the graph theory namespace ```agda module graph-theory where diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index 5ce7c983b7..962a96a816 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -1,6 +1,6 @@ # Group theory -## Files in the group theory folder +## Modules in the group theory namespace ```agda module group-theory where diff --git a/src/higher-group-theory.lagda.md b/src/higher-group-theory.lagda.md index 13e68733d8..ff263e15a5 100644 --- a/src/higher-group-theory.lagda.md +++ b/src/higher-group-theory.lagda.md @@ -1,6 +1,6 @@ # Higher group theory -## Files in the higher group theory folder +## Modules in the higher group theory namespace ```agda module higher-group-theory where diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index 257c870e77..883be1c3fa 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -1,6 +1,6 @@ # Linear algebra -## Files in the linear algebra folder +## Modules in the linear algebra namespace ```agda module linear-algebra where diff --git a/src/lists.lagda.md b/src/lists.lagda.md index 18b0ea48f3..0263108995 100644 --- a/src/lists.lagda.md +++ b/src/lists.lagda.md @@ -1,6 +1,6 @@ # Lists -## Files in the lists folder +## Modules in the lists namespace ```agda module lists where diff --git a/src/modal-type-theory.lagda.md b/src/modal-type-theory.lagda.md index 872f769c29..e9f60ad038 100644 --- a/src/modal-type-theory.lagda.md +++ b/src/modal-type-theory.lagda.md @@ -4,7 +4,20 @@ {-# OPTIONS --cohesion --flat-split #-} ``` -## Files in the modal type theory folder +Modal type theory is the study of type theory extended with syntactic _modal_ +operators. These are operations on types that increase the expressivity of the +type theory in some way. + +In this namespace, we consider modal extensions of Martin-Löf type theory with a +[flat modality](modal-type-theory.flat-modality.md) `♭`, +[sharp modality](modal-type-theory.sharp-modality.md) `♯`, and more to come. The +[adjoint pair of modalities](modal-type-theory.flat-sharp-adjunction.md) +`♭ ⊣ ＃` display a structure on all types referred to as _spatial_, or +_cohesive_ structure. + +- To read more, continue to [crisp types](modal-type-theory.crisp-types.md). + +## Modules in the modal type theory namespace ```agda module modal-type-theory where diff --git a/src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md b/src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md index 028fdaeee2..248652177b 100644 --- a/src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md +++ b/src/modal-type-theory/action-on-homotopies-flat-modality.lagda.md @@ -22,8 +22,9 @@ open import modal-type-theory.functoriality-flat-modality ## Idea -Given a crisp [homotopy](foundation-core.homotopies.md) of maps `f ~ g`, then -there is a homotopy `♭ f ~ ♭ g` where `♭ f` is the +Given a [crisp](modal-type-theory.crisp-types.md) +[homotopy](foundation-core.homotopies.md) of maps `f ~ g`, then there is a +homotopy `♭ f ~ ♭ g` where `♭ f` is the [functorial action of the flat modality on maps](modal-type-theory.functoriality-flat-modality.md). ## Definitions diff --git a/src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md b/src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md index 5b28c70c99..085fda16e2 100644 --- a/src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md +++ b/src/modal-type-theory/action-on-identifications-crisp-functions.lagda.md @@ -20,12 +20,12 @@ open import modal-type-theory.crisp-identity-types ## Idea -A function defined on [crisp elements](modal-type-theory.crisp-types.md) -`f : @♭ A → B` preserves crisp +A function defined on crisp elements `f : @♭ A → B` preserves crisp [identifications](foundation-core.identity-types.md), in the sense that it maps a crisp identification `p : x ＝ y` in `A` to an identification `crisp-ap f p : f x ＝ f y` in `B`. This action on identifications can be -understood as crisp functoriality of crisp identity types. +understood as crisp functoriality of [crisp](modal-type-theory.crisp-types.md) +identity types. This is a strengthening of the [action on identifications of functions](foundation.action-on-identifications-functions.md) diff --git a/src/modal-type-theory/action-on-identifications-flat-modality.lagda.md b/src/modal-type-theory/action-on-identifications-flat-modality.lagda.md index a573dcddf1..4f878208a8 100644 --- a/src/modal-type-theory/action-on-identifications-flat-modality.lagda.md +++ b/src/modal-type-theory/action-on-identifications-flat-modality.lagda.md @@ -22,8 +22,9 @@ open import modal-type-theory.flat-modality ## Idea -Given a crisp [identification](foundation-core.identity-types.md) `x ＝ y` in -`A`, then there is an identification `intro-flat x ＝ intro-flat y` in `♭ A`. +Given a [crisp](modal-type-theory.crisp-types.md) +[identification](foundation-core.identity-types.md) `x ＝ y` in `A`, then there +is an identification `intro-flat x ＝ intro-flat y` in `♭ A`. ## Definitions diff --git a/src/modal-type-theory/crisp-dependent-pair-types.lagda.md b/src/modal-type-theory/crisp-dependent-pair-types.lagda.md index 69ac59e250..962a9f0762 100644 --- a/src/modal-type-theory/crisp-dependent-pair-types.lagda.md +++ b/src/modal-type-theory/crisp-dependent-pair-types.lagda.md @@ -99,7 +99,7 @@ module _ compute-counit-flat-Σ : counit-flat {A = Σ A B} ~ - ( map-Σ B counit-flat (λ where (intro-flat _) → counit-flat)) ∘ + ( map-Σ B counit-flat counit-family-flat) ∘ ( map-distributive-flat-Σ) compute-counit-flat-Σ (intro-flat _) = refl ``` @@ -117,7 +117,7 @@ module _ is-flat-discrete-crisp-Σ is-disc-B = is-equiv-left-map-triangle ( counit-flat) - ( map-Σ B counit-flat (λ where (intro-flat _) → counit-flat)) + ( map-Σ B counit-flat counit-family-flat) ( map-distributive-flat-Σ) ( λ where (intro-flat _) → refl) ( is-equiv-map-distributive-flat-Σ) @@ -129,7 +129,7 @@ module _ is-fiberwise-equiv-is-equiv-map-Σ ( B) ( counit-flat) - ( λ where (intro-flat _) → counit-flat) + ( counit-family-flat) ( is-disc-A) ( is-equiv-right-map-triangle ( counit-flat) diff --git a/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md b/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md index a5a795e2f0..52f9b9c10f 100644 --- a/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md +++ b/src/modal-type-theory/crisp-law-of-excluded-middle.lagda.md @@ -22,7 +22,8 @@ open import foundation-core.propositions ## Idea The {{#concept "crisp law of excluded middle" Agda=Crisp-LEM}} asserts that any -crisp [proposition](foundation-core.propositions.md) `P` is +[crisp](modal-type-theory.crisp-types.md) +[proposition](foundation-core.propositions.md) `P` is [decidable](foundation.decidable-types.md). ## Definition diff --git a/src/modal-type-theory/crisp-types.lagda.md b/src/modal-type-theory/crisp-types.lagda.md index fc0a210f20..fe5e13dfc2 100644 --- a/src/modal-type-theory/crisp-types.lagda.md +++ b/src/modal-type-theory/crisp-types.lagda.md @@ -44,13 +44,14 @@ one which is crisp and one which is cohesive, we may in a type signature write ``` Observe that for us to be able to assume `x` is crisp at all, we must also -assume that the type `A` and the universe level `l` are crisp, following the -rule that crisp hypotheses may only be formed in crisp contexts. - -So what does it mean for `A` to be a {{#concept "crisp type"}}? Since the -universe of types is itself a type, and every type comes equipped with cohesive -structure, it means that the definition of `A` is indifferent to the cohesive -structure on the universe. +assume that the type `A` and the [universe level](foundation.universe-levels.md) +`l` are crisp, following the rule that crisp hypotheses may only be formed in +crisp contexts. + +So what does it mean for `A` to be a crisp type? Since the universe of types is +itself a type, and every type comes equipped with cohesive structure, that `A` +is a {{#concept "crisp type"}} means that the definition of `A` is indifferent +to the cohesive structure on the universe. Note that saying a type is crisp is very different to saying that the cohesive structure of the type is trivial, which one could in one way informally state as diff --git a/src/modal-type-theory/flat-discrete-crisp-types.lagda.md b/src/modal-type-theory/flat-discrete-crisp-types.lagda.md index 0aa7b7204b..5bf37687fc 100644 --- a/src/modal-type-theory/flat-discrete-crisp-types.lagda.md +++ b/src/modal-type-theory/flat-discrete-crisp-types.lagda.md @@ -36,8 +36,8 @@ open import modal-type-theory.functoriality-flat-modality ## Idea -A crisp type is said to be -{{$concept "flat discrete" Disambiguation="crisp type" Agda=is-flat-discrete-crisp}} +A [crisp type](modal-type-theory.crisp-types.md) is said to be +{{#concept "flat discrete" Disambiguation="crisp type" Agda=is-flat-discrete-crisp}} if it is [flat](modal-type-theory.flat-modality.md) modal. I.e. if the flat counit is an [equivalence](foundation-core.equivalences.md) at that type. @@ -120,9 +120,9 @@ module _ is-flat-discrete-crisp-equiv : @♭ A ≃ B → is-flat-discrete-crisp A → is-flat-discrete-crisp B - is-flat-discrete-crisp-equiv e bB = + is-flat-discrete-crisp-equiv e bA = is-equiv-htpy-equiv' - ( e ∘e (counit-flat , bB) ∘e action-flat-equiv (inv-equiv e)) + ( e ∘e (counit-flat , bA) ∘e action-flat-equiv (inv-equiv e)) ( λ where (intro-flat x) → is-section-map-inv-equiv e x) is-flat-discrete-crisp-equiv' : @@ -133,7 +133,7 @@ module _ ( λ where (intro-flat x) → is-retraction-map-inv-equiv e x) ``` -### Types `♭ A` are flat discrete +### Types in the image of `♭` are flat discrete This is Theorem 6.18 of {{#cite Shu18}}. @@ -152,15 +152,15 @@ Given crisp elements `x` and `y` of `A` We have a [commuting triangle](foundation-core.commuting-triangles-of-maps.md) ```text - ♭ (x ＝ y) - ∧ | - Eq-eq-flat /~ | - / | - (intro-flat x ＝ intro-flat y) | counit-flat - \ | - ap (counit-flat) \ | - ∨ ∨ - (x ＝ y) + ♭ (x = y) + ∧ | + Eq-eq-flat /~ | + / | + (intro-flat x = intro-flat y) | counit-flat + \ | + ap (counit-flat) \ | + ∨ ∨ + (x = y) ``` where the top-left map `Eq-eq-flat` is an equivalence. Thus, the right map is an diff --git a/src/modal-type-theory/flat-modality.lagda.md b/src/modal-type-theory/flat-modality.lagda.md index d3b1c42c08..10318f9d11 100644 --- a/src/modal-type-theory/flat-modality.lagda.md +++ b/src/modal-type-theory/flat-modality.lagda.md @@ -163,5 +163,6 @@ module _ ## External links -- [Flat Modality](https://agda.readthedocs.io/en/latest/language/flat.html) on - the Agda documentation pages. +- [Flat Modality](https://agda.readthedocs.io/en/latest/language/flat.html) at + the Agda documentation pages +- [flat modality](https://ncatlab.org/nlab/show/flat+modality) at $n$Lab diff --git a/src/modal-type-theory/flat-sharp-adjunction.lagda.md b/src/modal-type-theory/flat-sharp-adjunction.lagda.md index e0f9f2a500..f3cd07d5ef 100644 --- a/src/modal-type-theory/flat-sharp-adjunction.lagda.md +++ b/src/modal-type-theory/flat-sharp-adjunction.lagda.md @@ -30,7 +30,7 @@ open import modal-type-theory.sharp-modality ## Idea We postulate that the [flat modality](modal-type-theory.flat-modality.md) `♭` is -a crisp left adjoint to the +a [crisp](modal-type-theory.crisp-types.md) left adjoint to the [sharp modality](modal-type-theory.sharp-modality.md) `♯`. In [The sharp modality](modal-type-theory.sharp-modality.md) we postulated that @@ -38,7 +38,7 @@ In [The sharp modality](modal-type-theory.sharp-modality.md) we postulated that that has a [modal induction principle](orthogonal-factorization-systems.modal-induction.md). In the file -[Sharp-Codiscrete types](modal-type-theory.sharp-codiscrete-types.md), we +[sharp codiscrete types](modal-type-theory.sharp-codiscrete-types.md), we postulated that the [subuniverse](foundation.subuniverses.md) of sharp modal types has appropriate closure properties. Please note that there is some redundancy between the postulated axioms, and they are likely to change in the @@ -110,6 +110,8 @@ The accompanying computation principle remains to be fully formalized. ### Flat eats sharp +We have equivalences `♭ (♯ A) ≃ ♭ A`. + ```agda module _ {@♭ l : Level} {@♭ A : UU l} @@ -158,6 +160,8 @@ module _ ### Sharp eats flat +We have equivalences `♯ (♭ A) ≃ ♯ A`. + ```agda module _ {@♭ l : Level} {@♭ A : UU l} diff --git a/src/modal-type-theory/functoriality-flat-modality.lagda.md b/src/modal-type-theory/functoriality-flat-modality.lagda.md index 9f822969d8..150a1c469e 100644 --- a/src/modal-type-theory/functoriality-flat-modality.lagda.md +++ b/src/modal-type-theory/functoriality-flat-modality.lagda.md @@ -50,6 +50,18 @@ module _ action-flat-family B = action-flat-crisp-family (crispen B) ``` +### The counit of the flat modality's action on type families + +```agda +module _ + {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : A → UU l2} + where + + counit-family-flat : + (y : ♭ A) → action-flat-family B y → B (counit-flat y) + counit-family-flat (intro-flat _) = counit-flat +``` + ### The flat modality's action on maps ```agda diff --git a/src/modal-type-theory/sharp-codiscrete-types.lagda.md b/src/modal-type-theory/sharp-codiscrete-types.lagda.md index 887f38e44e..0eb4a695fb 100644 --- a/src/modal-type-theory/sharp-codiscrete-types.lagda.md +++ b/src/modal-type-theory/sharp-codiscrete-types.lagda.md @@ -34,7 +34,7 @@ A type is said to be {{#concept "sharp codiscrete" Agda=is-sharp-codiscrete}} if it is [sharp](modal-type-theory.sharp-modality.md) modal, i.e. if the sharp unit is an [equivalence](foundation-core.equivalences.md) at that type. -We postulate that codiscrete types are closed under +We postulate that sharp codiscrete types are closed under - the formation of identity types - the formation of dependent function types diff --git a/src/modal-type-theory/sharp-modality.lagda.md b/src/modal-type-theory/sharp-modality.lagda.md index ba9c2f224e..3dba911431 100644 --- a/src/modal-type-theory/sharp-modality.lagda.md +++ b/src/modal-type-theory/sharp-modality.lagda.md @@ -402,3 +402,7 @@ compute-rec-subuniverse-sharp = {{#bibliography}} {{#reference Shu18}} {{#reference Dlicata335/Cohesion-Agda}} {{#reference Felixwellen/DCHoTT-Agda}} {{#reference DavidJaz/Cohesion}} + +## External links + +- [sharp modality](https://ncatlab.org/nlab/show/sharp+modality) at $n$Lab diff --git a/src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md b/src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md index a6bd8f03a0..63e293c714 100644 --- a/src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md +++ b/src/modal-type-theory/universal-property-flat-discrete-crisp-types.lagda.md @@ -34,7 +34,8 @@ The {{#concept "universal property" Disambiguation="of flat discrete crisp types" Agda=universal-property-flat-discrete-crisp-type}} of a [flat discrete crisp type](modal-type-theory.flat-discrete-crisp-types.md) `A` states that under the [flat modality](modal-type-theory.flat-modality.md) -`♭`, `A` is colocal at the counit of `♭`. +`♭`, `A` is [colocal](orthogonal-factorization-systems.types-colocal-at-maps.md) +at the counit of `♭`. By this we mean that for every [crisp type](modal-type-theory.crisp-types.md) `B` the map diff --git a/src/online-encyclopedia-of-integer-sequences.lagda.md b/src/online-encyclopedia-of-integer-sequences.lagda.md index 413851fe23..697e4582db 100644 --- a/src/online-encyclopedia-of-integer-sequences.lagda.md +++ b/src/online-encyclopedia-of-integer-sequences.lagda.md @@ -1,6 +1,6 @@ # Online encyclopedia of integer sequences -## Files in the OEIS folder +## Modules in the OEIS namespace ```agda module online-encyclopedia-of-integer-sequences where diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index de476c0b14..fdb7cae0eb 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -1,6 +1,6 @@ # Order theory -## Files in the order theory folder +## Modules in the order theory namespace ```agda module order-theory where diff --git a/src/order-theory/large-suplattices.lagda.md b/src/order-theory/large-suplattices.lagda.md index ac9782f0a4..6f8bb90417 100644 --- a/src/order-theory/large-suplattices.lagda.md +++ b/src/order-theory/large-suplattices.lagda.md @@ -4,24 +4,22 @@ module order-theory.large-suplattices where ``` -Imports +
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.large-binary-relations - open import foundation.binary-relations - +open import foundation.dependent-pair-types open import foundation.identity-types +open import foundation.large-binary-relations open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.universe-levels open import order-theory.large-posets +open import order-theory.least-upper-bounds-large-posets open import order-theory.posets open import order-theory.suplattices -open import order-theory.least-upper-bounds-large-posets open import order-theory.upper-bounds-large-posets ``` diff --git a/src/order-theory/precategory-of-decidable-total-orders.lagda.md b/src/order-theory/precategory-of-decidable-total-orders.lagda.md index 7632fb7f60..ee91924562 100644 --- a/src/order-theory/precategory-of-decidable-total-orders.lagda.md +++ b/src/order-theory/precategory-of-decidable-total-orders.lagda.md @@ -51,7 +51,7 @@ Decidable-Total-Order-Large-Precategory = ( λ l → l)) ``` -### The precategory or total orders of universe level `l` +### The precategory of total orders at a universe level ```agda Decidable-Total-Order-Precategory : (l : Level) → Precategory (lsuc l) l diff --git a/src/order-theory/precategory-of-posets.lagda.md b/src/order-theory/precategory-of-posets.lagda.md index 29876db4bc..2d4708a629 100644 --- a/src/order-theory/precategory-of-posets.lagda.md +++ b/src/order-theory/precategory-of-posets.lagda.md @@ -28,6 +28,16 @@ consists of [posets](order-theory.posets.md) and ### The large precategory of posets +**Remark.** In this formalization we see a clear limit to our approach using +[large precategories](category-theory.large-precategories.md). Large +precategories are only designed to encapsulate structures that are universe +polymorphic in a single universe level variable. However, posets are polymorphic +in two universe level variables, leading to a shortcoming in the below +formalization. Namely, we cannot capture the structure of all posets and +morphisms between them. For instance, we can only capture morphisms between two +posets of the form `A : Poset (α l1) (β l1)` and `B : Poset (α l2) (β l2)`, and +not arbitrary ones of the form `A : Poset l1 l2` and `B : Poset l3 l4`. + ```agda parametric-Poset-Large-Precategory : (α β : Level → Level) → @@ -55,7 +65,7 @@ Poset-Large-Precategory : Large-Precategory lsuc (_⊔_) Poset-Large-Precategory = parametric-Poset-Large-Precategory (λ l → l) (λ l → l) ``` -### The precategory or posets of universe level `l` +### The precategory of posets at a universe level ```agda Poset-Precategory : (l : Level) → Precategory (lsuc l) l diff --git a/src/order-theory/precategory-of-total-orders.lagda.md b/src/order-theory/precategory-of-total-orders.lagda.md index 8a9fc8c68a..aeb5d9ffd2 100644 --- a/src/order-theory/precategory-of-total-orders.lagda.md +++ b/src/order-theory/precategory-of-total-orders.lagda.md @@ -48,7 +48,7 @@ Total-Order-Large-Precategory = ( parametric-Total-Order-Full-Large-Subprecategory (λ l → l) (λ l → l)) ``` -### The precategory or total orders of universe level `l` +### The precategory of total orders at a universe level ```agda Total-Order-Precategory : (l : Level) → Precategory (lsuc l) l diff --git a/src/organic-chemistry.lagda.md b/src/organic-chemistry.lagda.md index ce03691caf..d4b75e9bc7 100644 --- a/src/organic-chemistry.lagda.md +++ b/src/organic-chemistry.lagda.md @@ -1,6 +1,6 @@ -# Organic Chemistry +# Organic chemistry -## Files in the organic chemistry folder +## Modules in the organic chemistry namespace ```agda module organic-chemistry where diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index ffbc40cb41..59412d4838 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -4,7 +4,7 @@ {{#include tables/higher-modalities.md}} -## Files in the orthogonal factorization systems folder +## Modules in the orthogonal factorization systems namespace ```agda module orthogonal-factorization-systems where diff --git a/src/polytopes.lagda.md b/src/polytopes.lagda.md index 5c99a1d9d3..93741a955f 100644 --- a/src/polytopes.lagda.md +++ b/src/polytopes.lagda.md @@ -1,6 +1,6 @@ # Polytopes -## Files in the polytopes folder +## Modules in the polytopes namespace ```agda module polytopes where diff --git a/src/primitives.lagda.md b/src/primitives.lagda.md index eb87d699dc..acbfb7f982 100644 --- a/src/primitives.lagda.md +++ b/src/primitives.lagda.md @@ -1,6 +1,6 @@ # Primitives -## Files in the primitives folder +## Modules in the primitives namespace ```agda module primitives where diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index ce0ae91405..0dcf4ac5ce 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -1,6 +1,6 @@ # Real numbers -## Files in the real numbers folder +## Modules in the real numbers namespace ```agda module real-numbers where diff --git a/src/reflection.lagda.md b/src/reflection.lagda.md index f0d2255e66..0e4c56b9dc 100644 --- a/src/reflection.lagda.md +++ b/src/reflection.lagda.md @@ -4,7 +4,7 @@ {-# OPTIONS --rewriting #-} ``` -## Files in the reflection folder +## Modules in the reflection namespace ```agda module reflection where diff --git a/src/ring-theory.lagda.md b/src/ring-theory.lagda.md index 0262edca9e..9ea7cb8d0b 100644 --- a/src/ring-theory.lagda.md +++ b/src/ring-theory.lagda.md @@ -1,6 +1,6 @@ # Ring theory -## Files in the ring theory folder +## Modules in the ring theory namespace ```agda module ring-theory where diff --git a/src/ring-theory/precategory-of-rings.lagda.md b/src/ring-theory/precategory-of-rings.lagda.md index e4d937c4e3..e22cb72547 100644 --- a/src/ring-theory/precategory-of-rings.lagda.md +++ b/src/ring-theory/precategory-of-rings.lagda.md @@ -40,7 +40,7 @@ Ring-Large-Precategory = ( λ {l1} {l2} {R} {S} → right-unit-law-comp-hom-Ring R S) ``` -### The precategory or rings of universe level `l` +### The precategory of rings at a universe level ```agda Ring-Precategory : (l : Level) → Precategory (lsuc l) l diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md index 36a50cbf2a..7330b0cf07 100644 --- a/src/set-theory.lagda.md +++ b/src/set-theory.lagda.md @@ -1,6 +1,6 @@ # Set theory -## Files in the set theory folder +## Modules in the set theory namespace ```agda module set-theory where diff --git a/src/species.lagda.md b/src/species.lagda.md index 404c24e387..c36d98ea52 100644 --- a/src/species.lagda.md +++ b/src/species.lagda.md @@ -1,6 +1,6 @@ # Species -## Files in the species folder +## Modules in the species namespace ```agda module species where diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index 84ce3ff547..3cdeac110c 100644 --- a/src/structured-types.lagda.md +++ b/src/structured-types.lagda.md @@ -4,7 +4,7 @@ {-# OPTIONS --guardedness #-} ``` -## Files in the structured types folder +## Modules in the structured types namespace ```agda module structured-types where diff --git a/src/structured-types/wild-category-of-pointed-types.lagda.md b/src/structured-types/wild-category-of-pointed-types.lagda.md index 1ae08161f4..14d31f1fa0 100644 --- a/src/structured-types/wild-category-of-pointed-types.lagda.md +++ b/src/structured-types/wild-category-of-pointed-types.lagda.md @@ -196,7 +196,7 @@ is-transitive-globular-structure-pointed-Π = is-transitive-globular-structure-Id (pointed-2-htpy α β) ``` -#### The uniform large globular structure on pointed types +#### The nonuniform large globular structure on pointed types ```agda large-globular-structure-Pointed-Type : diff --git a/src/synthetic-category-theory.lagda.md b/src/synthetic-category-theory.lagda.md index aa78200560..9b8b60665e 100644 --- a/src/synthetic-category-theory.lagda.md +++ b/src/synthetic-category-theory.lagda.md @@ -20,7 +20,7 @@ Some core principles of higher category theory include: - Any valid statement or construction in category theory must respect isomorphisms {{#cite Makkai98}}. -## Files in the Synthetic category theory folder +## Modules in the synthetic category theory namespace ```agda module synthetic-category-theory where diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index 1936a61a82..99cc4374cb 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -4,7 +4,7 @@ {-# OPTIONS --rewriting --guardedness #-} ``` -## Files in the synthetic homotopy theory folder +## Modules in the synthetic homotopy theory namespace ```agda module synthetic-homotopy-theory where diff --git a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md index ae0c5ba39e..032085a619 100644 --- a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md +++ b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md @@ -785,9 +785,10 @@ module _ ## External links - [The Eckmann-Hilton argument](https://1lab.dev/Algebra.Magma.Unital.EckmannHilton.html) - at 1lab. + at 1lab - [Eckmann-Hilton argument](https://ncatlab.org/nlab/show/Eckmann-Hilton+argument) - at $n$Lab. + at $n$Lab - [Eckmann-Hilton argument](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument) - at Wikipedia. + at Wikipedia - [Eckmann-Hilton and the Hopf Fibration](https://www.youtube.com/watch?v=hU4_dVpmkKM) + recorded talk given by Raymond Baker at HoTT-UF 24 diff --git a/src/type-theories.lagda.md b/src/type-theories.lagda.md index fe22a9f4a2..1255733d03 100644 --- a/src/type-theories.lagda.md +++ b/src/type-theories.lagda.md @@ -4,7 +4,7 @@ {-# OPTIONS --guardedness #-} ``` -## Files in the type theories folder +## Modules in the type theories namespace ```agda module type-theories where diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md index 9cf585b8a3..d7d2896487 100644 --- a/src/univalent-combinatorics.lagda.md +++ b/src/univalent-combinatorics.lagda.md @@ -15,7 +15,7 @@ such that all its homotopy groups up to level `k` are finite. The π-finite type enjoy useful closure properties, such as closedness under Σ, cartesian products, coproducts, and closedness under Π under a mild condition. -## Files in the univalent combinatorics folder +## Modules in the univalent combinatorics namespace ```agda module univalent-combinatorics where diff --git a/src/univalent-combinatorics/dedekind-finite-sets.lagda.md b/src/univalent-combinatorics/dedekind-finite-sets.lagda.md index 11f8576fef..6d9d1faf2c 100644 --- a/src/univalent-combinatorics/dedekind-finite-sets.lagda.md +++ b/src/univalent-combinatorics/dedekind-finite-sets.lagda.md @@ -60,7 +60,7 @@ module _ ## See also - [Finite types](univalent-combinatorics.finite-types.md) -- [Kratowsky-finite sets](univalent-combinatorics.kuratowski-finite-sets.md) +- [Kuratowski finite sets](univalent-combinatorics.kuratowski-finite-sets.md) ## References diff --git a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md index 89140ea232..8255b3ad10 100644 --- a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md +++ b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md @@ -92,7 +92,7 @@ has-decidable-equality-is-finite-type-𝔽-Kuratowski X = ## See also - [Finite types](univalent-combinatorics.finite-types.md) -- [Dedekind-finite sets](univalent-combinatorics.dedekind-finite-sets.md) +- [Dedekind finite sets](univalent-combinatorics.dedekind-finite-sets.md) ## External links diff --git a/src/universal-algebra.lagda.md b/src/universal-algebra.lagda.md index f3f214e968..183927520e 100644 --- a/src/universal-algebra.lagda.md +++ b/src/universal-algebra.lagda.md @@ -1,6 +1,6 @@ # Universal algebra -## Files in the universal algebra folder +## Modules in the universal algebra namespace ```agda module universal-algebra where diff --git a/src/wild-category-theory.lagda.md b/src/wild-category-theory.lagda.md index 10c293d9e0..63cf266e2d 100644 --- a/src/wild-category-theory.lagda.md +++ b/src/wild-category-theory.lagda.md @@ -8,7 +8,7 @@ {{#include tables/wild-categories.md}} -## Files in the wild category theory folder +## Modules in the wild category theory namespace ```agda module wild-category-theory where