From ccbaa463dc9df760e33db0996896924e69cfb94d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 21 Mar 2023 20:44:35 +0100 Subject: [PATCH] Formatting fixes (#530) Just a bunch of miscellaneous formatting. - Fix capitalization of module titles - Make comment headers into actual headers - Remove some superfluous whitespace - Organize VSCode settings - Add VSCode settings that nest ".agdai" and ".agda~" files under the associated ".lagda.md" file to declutter the file view. - Fix a breaking bug with `generate_main_index` when there are duplicate titles - Add `
` blocks to all files (except `foundation-core.universe-levels`) - Remove unused imports --- .prettierrc.json | 34 +++++----- .vscode/settings.json | 50 ++++++++++---- Makefile | 2 +- grant-acknowledgements.md | 2 +- scripts/demote_foundation_imports.py | 4 +- scripts/generate_main_index_file.py | 2 +- scripts/remove_unused_imports.py | 8 ++- src/category-theory/anafunctors.lagda.md | 2 +- .../isomorphisms-large-precategories.lagda.md | 2 +- .../ideals-commutative-rings.lagda.md | 1 - .../ideals-commutative-semirings.lagda.md | 2 - .../maximal-ideals-commutative-rings.lagda.md | 8 +++ .../nilradical-commutative-rings.lagda.md | 15 ---- ...ers-of-elements-commutative-rings.lagda.md | 1 - .../prime-ideals-commutative-rings.lagda.md | 1 - ...icals-of-ideals-commutative-rings.lagda.md | 8 --- .../sums-commutative-rings.lagda.md | 2 +- .../sums-commutative-semirings.lagda.md | 2 +- .../bezouts-lemma.lagda.md | 6 +- .../congruence-natural-numbers.lagda.md | 4 +- .../divisibility-natural-numbers.lagda.md | 1 - .../finitary-natural-numbers.lagda.md | 2 +- .../goldbach-conjecture.lagda.md | 3 +- .../greatest-common-divisor-integers.lagda.md | 8 ++- .../inequality-integers.lagda.md | 16 +++-- .../inequality-natural-numbers.lagda.md | 2 - .../integer-partitions.lagda.md | 14 ++-- .../integers.lagda.md | 3 - ...-arithmetic-standard-finite-types.lagda.md | 2 +- .../modular-arithmetic.lagda.md | 2 +- .../multiplication-integers.lagda.md | 4 +- .../multiplication-natural-numbers.lagda.md | 4 +- .../rational-numbers.lagda.md | 2 +- .../sums-of-natural-numbers.lagda.md | 7 +- .../twin-prime-conjecture.lagda.md | 8 +-- ...rdering-principle-natural-numbers.lagda.md | 7 +- .../delooping-sign-homomorphism.lagda.md | 2 +- .../finite-type-groups.lagda.md | 2 +- src/foundation-core.lagda.md | 2 +- src/foundation-core/cones-pullbacks.lagda.md | 2 +- .../contractible-types.lagda.md | 2 +- src/foundation-core/coproduct-types.lagda.md | 2 +- .../equivalence-induction.lagda.md | 4 +- src/foundation-core/equivalences.lagda.md | 4 +- ...unctoriality-dependent-pair-types.lagda.md | 9 ++- src/foundation-core/truncated-maps.lagda.md | 2 +- src/foundation-core/truncated-types.lagda.md | 2 +- .../universal-property-pullbacks.lagda.md | 2 +- src/foundation/0-maps.lagda.md | 6 ++ .../algebras-polynomial-endofunctors.lagda.md | 2 - src/foundation/automorphisms.lagda.md | 6 ++ src/foundation/binary-equivalences.lagda.md | 4 +- ...erations-unordered-pairs-of-types.lagda.md | 2 +- src/foundation/boolean-reflection.lagda.md | 2 +- src/foundation/booleans.lagda.md | 2 +- ...cantor-schroder-bernstein-escardo.lagda.md | 4 +- .../cartesian-product-types.lagda.md | 7 +- ...mmuting-3-simplices-of-homotopies.lagda.md | 6 ++ .../commuting-3-simplices-of-maps.lagda.md | 6 ++ ...commuting-triangles-of-homotopies.lagda.md | 6 ++ src/foundation/cones-pullbacks.lagda.md | 6 ++ src/foundation/coproduct-types.lagda.md | 2 +- src/foundation/cospans.lagda.md | 6 ++ src/foundation/decidable-embeddings.lagda.md | 1 - .../decidable-equivalence-relations.lagda.md | 22 +++--- src/foundation/decidable-maps.lagda.md | 4 +- src/foundation/decidable-relations.lagda.md | 11 ++- src/foundation/decidable-types.lagda.md | 2 +- .../dependent-binomial-theorem.lagda.md | 2 +- src/foundation/dependent-pair-types.lagda.md | 7 +- src/foundation/dependent-paths.lagda.md | 10 +-- ...rete-relaxed-sigma-decompositions.lagda.md | 19 +++--- .../discrete-sigma-decompositions.lagda.md | 18 ++--- ...epimorphisms-with-respect-to-sets.lagda.md | 2 +- .../equality-cartesian-product-types.lagda.md | 6 ++ .../equality-fibers-of-maps.lagda.md | 6 ++ src/foundation/faithful-maps.lagda.md | 6 ++ src/foundation/functions.lagda.md | 7 +- .../functoriality-fibers-of-maps.lagda.md | 6 ++ ...amental-theorem-of-identity-types.lagda.md | 6 ++ src/foundation/identity-systems.lagda.md | 6 ++ src/foundation/images-subtypes.lagda.md | 15 ++-- ...-limited-principle-of-omniscience.lagda.md | 1 - src/foundation/morphisms-cospans.lagda.md | 6 ++ src/foundation/path-algebra.lagda.md | 6 +- src/foundation/perfect-images.lagda.md | 8 +-- src/foundation/pullbacks.lagda.md | 18 ++--- .../relaxed-sigma-decompositions.lagda.md | 30 +++----- src/foundation/set-truncations.lagda.md | 12 +++- src/foundation/sets.lagda.md | 2 +- .../sigma-decomposition-subuniverse.lagda.md | 13 ++-- src/foundation/sigma-decompositions.lagda.md | 34 ++++------ .../strongly-extensional-maps.lagda.md | 10 ++- .../subtype-identity-principle.lagda.md | 6 ++ ...vial-relaxed-sigma-decompositions.lagda.md | 20 +++--- .../trivial-sigma-decompositions.lagda.md | 19 +++--- src/foundation/tuples-of-types.lagda.md | 2 - ...rithmetic-cartesian-product-types.lagda.md | 6 ++ ...ithmetic-dependent-function-types.lagda.md | 15 ++-- ...e-arithmetic-dependent-pair-types.lagda.md | 6 ++ src/foundation/type-duality.lagda.md | 30 ++++---- .../uniqueness-set-quotients.lagda.md | 2 +- ...-property-cartesian-product-types.lagda.md | 13 ++-- ...universal-property-fiber-products.lagda.md | 8 ++- .../universal-property-maybe.lagda.md | 4 +- ...property-propositional-truncation.lagda.md | 4 +- ...universal-property-set-truncation.lagda.md | 2 +- .../universal-property-unit-type.lagda.md | 2 - src/foundation/universe-levels.lagda.md | 7 +- src/graph-theory/directed-graphs.lagda.md | 12 ++-- .../regular-undirected-graphs.lagda.md | 6 ++ ...merism-enriched-undirected-graphs.lagda.md | 2 +- .../category-of-concrete-groups.lagda.md | 7 +- .../central-elements-groups.lagda.md | 1 - .../central-elements-monoids.lagda.md | 1 - src/group-theory/decidable-subgroups.lagda.md | 2 +- ...dent-products-commutative-monoids.lagda.md | 2 - .../function-abelian-groups.lagda.md | 2 - .../function-commutative-monoids.lagda.md | 4 -- src/group-theory/function-groups.lagda.md | 2 - src/group-theory/function-monoids.lagda.md | 3 - src/group-theory/function-semigroups.lagda.md | 2 - src/group-theory/group-solver.lagda.md | 2 +- .../homomorphisms-higher-groups.lagda.md | 10 ++- .../homomorphisms-monoids.lagda.md | 2 +- .../homomorphisms-semigroups.lagda.md | 4 +- src/group-theory/normal-subgroups.lagda.md | 2 +- src/group-theory/normal-submonoids.lagda.md | 2 + src/group-theory/subgroups.lagda.md | 2 +- src/group-theory/torsors.lagda.md | 10 ++- src/linear-algebra/vectors.lagda.md | 2 +- .../distributive-lattices.lagda.md | 2 +- src/order-theory/finite-posets.lagda.md | 2 +- .../homomorphisms-frames.lagda.md | 4 +- .../homomorphisms-meet-semilattices.lagda.md | 4 +- .../homomorphisms-meet-sup-lattices.lagda.md | 4 +- .../homomorphisms-sup-lattices.lagda.md | 4 +- src/order-theory/large-posets.lagda.md | 2 +- .../largest-elements-preorders.lagda.md | 6 ++ src/order-theory/posets.lagda.md | 2 +- src/order-theory/sup-lattices.lagda.md | 4 +- src/organic-chemistry/ethane.lagda.md | 2 +- src/organic-chemistry/hydrocarbons.lagda.md | 2 +- .../central-elements-rings.lagda.md | 1 - .../central-elements-semirings.lagda.md | 1 - src/ring-theory/function-rings.lagda.md | 3 - src/ring-theory/homomorphisms-rings.lagda.md | 36 +++++++--- src/ring-theory/ideals-rings.lagda.md | 2 - src/ring-theory/ideals-semirings.lagda.md | 1 - src/ring-theory/isomorphisms-rings.lagda.md | 18 +++-- src/ring-theory/localizations-rings.lagda.md | 36 ++++++---- src/ring-theory/maximal-ideals-rings.lagda.md | 8 +++ .../nilpotent-elements-rings.lagda.md | 3 - .../nilpotent-elements-semirings.lagda.md | 8 --- src/ring-theory/quotient-rings.lagda.md | 2 +- src/ring-theory/rings.lagda.md | 2 +- src/ring-theory/semirings.lagda.md | 2 +- src/ring-theory/subsets-rings.lagda.md | 1 - src/ring-theory/subsets-semirings.lagda.md | 1 - src/ring-theory/sums-rings.lagda.md | 2 +- src/ring-theory/sums-semirings.lagda.md | 2 +- src/set-theory/cumulative-hierarchy.lagda.md | 5 +- ...species-of-finite-inhabited-types.lagda.md | 1 - ...omposition-species-of-subuniverse.lagda.md | 16 ----- ...cle-index-series-species-of-types.lagda.md | 1 - .../derivatives-species-of-types.lagda.md | 2 - .../equivalences-species-of-types.lagda.md | 2 - .../exponents-species-of-types.lagda.md | 4 -- ...arge-composition-species-of-types.lagda.md | 4 -- src/species/morphisms-finite-species.lagda.md | 1 - .../morphisms-species-of-types.lagda.md | 3 - src/species/species-of-finite-types.lagda.md | 2 +- .../species-of-types-in-subuniverse.lagda.md | 1 - .../morphisms-coherent-h-spaces.lagda.md | 4 +- .../pointed-homotopies.lagda.md | 8 ++- ...types-equipped-with-automorphisms.lagda.md | 8 +++ src/structured-types/wild-monoids.lagda.md | 10 +-- .../26-descent.lagda.md | 2 +- .../double-loop-spaces.lagda.md | 2 +- .../loop-spaces.lagda.md | 2 +- .../suspensions-of-types.lagda.md | 4 +- .../triple-loop-spaces.lagda.md | 20 ++++-- .../universal-cover-circle.lagda.md | 8 ++- src/trees/extensional-w-types.lagda.md | 2 +- src/trees/functoriality-w-types.lagda.md | 2 +- src/trees/undirected-trees.lagda.md | 68 ++++++++++++------- src/trees/w-types.lagda.md | 2 +- .../fibered-dependent-type-theories.lagda.md | 8 +-- .../sections-dependent-type-theories.lagda.md | 2 +- .../simple-type-theories.lagda.md | 2 +- .../counting-fibers-of-maps.lagda.md | 12 ++-- .../decidable-equivalence-relations.lagda.md | 3 - .../decidable-propositions.lagda.md | 2 - ...t-truncation-over-finite-products.lagda.md | 6 +- .../embeddings-standard-finite-types.lagda.md | 10 ++- .../embeddings.lagda.md | 1 - .../finite-presentations.lagda.md | 8 +++ .../finite-types.lagda.md | 2 - .../inhabited-finite-types.lagda.md | 1 - src/univalent-combinatorics/lists.lagda.md | 52 +++++++++----- ...tations-complete-undirected-graph.lagda.md | 8 +-- .../pi-finite-types.lagda.md | 2 +- .../presented-pi-finite-types.lagda.md | 8 +++ .../ramsey-theory.lagda.md | 8 +++ .../sigma-decompositions.lagda.md | 10 --- .../small-types.lagda.md | 3 - .../standard-finite-types.lagda.md | 12 ++-- .../surjective-maps.lagda.md | 8 --- .../symmetric-difference.lagda.md | 49 ++++++------- .../trivial-sigma-decompositions.lagda.md | 5 -- .../type-duality.lagda.md | 4 -- .../unions-subtypes.lagda.md | 1 - .../unlabeled-partitions.lagda.md | 8 +++ .../quotient-algebras.lagda.md | 10 +-- .../terms-over-signatures.lagda.md | 2 - 215 files changed, 823 insertions(+), 642 deletions(-) diff --git a/.prettierrc.json b/.prettierrc.json index 8ca7e370a0..9b476cb4fd 100644 --- a/.prettierrc.json +++ b/.prettierrc.json @@ -1,19 +1,19 @@ { - "arrowParens": "always", - "bracketSameLine": false, - "bracketSpacing": true, - "embeddedLanguageFormatting": "off", - "htmlWhitespaceSensitivity": "css", - "insertPragma": false, - "jsxSingleQuote": false, - "printWidth": 80, - "proseWrap": "always", - "quoteProps": "as-needed", - "requirePragma": false, - "semi": true, - "singleAttributePerLine": false, - "singleQuote": false, - "tabWidth": 2, - "trailingComma": "es5", - "useTabs": false + "arrowParens": "always", + "bracketSameLine": false, + "bracketSpacing": true, + "embeddedLanguageFormatting": "off", + "htmlWhitespaceSensitivity": "css", + "insertPragma": false, + "jsxSingleQuote": false, + "printWidth": 80, + "proseWrap": "always", + "quoteProps": "as-needed", + "requirePragma": false, + "semi": true, + "singleAttributePerLine": false, + "singleQuote": false, + "tabWidth": 2, + "trailingComma": "es5", + "useTabs": false } diff --git a/.vscode/settings.json b/.vscode/settings.json index 77bfc7e597..12a9921e03 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,41 +1,63 @@ { + // UI settings "breadcrumbs.enabled": false, + + "explorer.fileNesting.enabled": true, + "explorer.fileNesting.expand": false, + "explorer.fileNesting.patterns": { + "*.agda": "${capture}.agdai, ${capture}.agda~", + "*.lagda": "${capture}.agdai, ${capture}.agda~", + "*.lagda.md": "${capture}.agdai, ${capture}.agda~" + }, + + // Snippet setup "editor.quickSuggestions": { "other": "inline" }, "editor.snippetSuggestions": "top", "editor.wordBasedSuggestions": false, + "javascript.suggest.names": false, + + // Autoformatting and file type specific settings + "editor.defaultFormatter": "esbenp.prettier-vscode", + "editor.formatOnType": true, + "editor.formatOnSave": true, + + "files.insertFinalNewline": true, "files.trimFinalNewlines": true, "files.trimTrailingWhitespace": true, - "javascript.suggest.names": false, + "[agda]": { "editor.tabSize": 2, "editor.rulers": [80], "editor.formatOnType": true, "editor.formatOnSave": true }, + "[css]": { + "editor.quickSuggestions": { + "other": true + }, + "editor.suggest.insertMode": "replace", + "gitlens.codeLens.scopes": ["document"], + "editor.tabSize": 2 + }, + "[javascript]": { + "editor.maxTokenizationLineLength": 2500, + "editor.tabSize": 2 + }, "[json][jsonc]": { "editor.quickSuggestions": { "strings": true }, "editor.suggest.insertMode": "replace", - "gitlens.codeLens.scopes": ["document"], - "editor.defaultFormatter": "esbenp.prettier-vscode", - "editor.formatOnType": true, - "editor.formatOnSave": true + "gitlens.codeLens.scopes": ["document"] }, "[markdown]": { "editor.tabSize": 2, - "editor.rulers": [80], - "editor.defaultFormatter": "esbenp.prettier-vscode", - "editor.formatOnType": true, - "editor.formatOnSave": true + "editor.rulers": [80] }, "[python]": { "editor.tabSize": 4, - "editor.defaultFormatter": "ms-python.python", - "editor.formatOnType": true, - "editor.formatOnSave": true - }, - "files.insertFinalNewline": true + "editor.defaultFormatter": "ms-python.python" + } } diff --git a/Makefile b/Makefile index 7ca72e8209..df63c21e15 100644 --- a/Makefile +++ b/Makefile @@ -28,7 +28,7 @@ METAFILES:=CITATION.cff \ agdaFiles : @rm -rf $@ @rm -rf src/everything.lagda.md - @find src -name temp -prune -o -type f \( -name "*.agda" -o -name "*.lagda" -o -name "*.lagda.md" \) -print > $@ + @find src -name temp -prune -o -type f \( -name "*.agda" -o -name "*.lagda" -o -name "*.lagda.md" \) -print > $@ @sort -o $@ $@ @wc -l $@ @echo "$(shell (find src -name '*.lagda.md' -print0 | xargs -0 cat ) | wc -l) LOC" diff --git a/grant-acknowledgements.md b/grant-acknowledgements.md index 2bdc7dcfa3..31edf99616 100644 --- a/grant-acknowledgements.md +++ b/grant-acknowledgements.md @@ -1,4 +1,4 @@ -# Grant Acknowledgements +# Grant acknowledgements - The [TydiForm project](https://tydiform.fmf.uni-lj.si) (2020-Present). Air Force Office of Scientific Research, award number FA9550-21-1-0024. diff --git a/scripts/demote_foundation_imports.py b/scripts/demote_foundation_imports.py index 89c7a48f34..bae07e0be3 100644 --- a/scripts/demote_foundation_imports.py +++ b/scripts/demote_foundation_imports.py @@ -17,7 +17,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir): if nonpublic is None: utils.multithread.thread_safe_print( - f"'{agda_module}' Could not find imports. Skipping.") + f"'{agda_module}' Could not find imports.") return # Subdivide imports into namespaces @@ -25,7 +25,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir): if not "foundation" in namespaces.keys(): utils.multithread.thread_safe_print( - f"'{agda_module}' has no foundation imports. Skipping.") + f"'{agda_module}' has no foundation imports.") return new_nonpublic = set(nonpublic) diff --git a/scripts/generate_main_index_file.py b/scripts/generate_main_index_file.py index 958cca6f18..5423ebf6c0 100755 --- a/scripts/generate_main_index_file.py +++ b/scripts/generate_main_index_file.py @@ -41,7 +41,7 @@ def generate_namespace_entry_list(namespace): print(f"WARNING! Duplicate titles in {namespace}:") for ec in equal_titles: print( - f" Title '{ec[0][0]}': {', '.join(m[1][:m.rfind('.lagda.md')] for m in ec)}") + f" Title '{ec[0][0]}': {', '.join(m[1][:m[1].rfind('.lagda.md')] for m in ec)}") module_titles_and_mdfiles = sorted( zip(module_titles, module_mdfiles), key=lambda tm: (tm[0].casefold(), tm[1])) diff --git a/scripts/remove_unused_imports.py b/scripts/remove_unused_imports.py index 446221d98d..410dcecf2f 100644 --- a/scripts/remove_unused_imports.py +++ b/scripts/remove_unused_imports.py @@ -19,9 +19,13 @@ def process_agda_file(agda_file, agda_options, root, temp_dir): agda_module = utils.get_agda_module_name(agda_file, root) # If no nonpublic imports, skip - if not nonpublic: + if nonpublic is None: utils.multithread.thread_safe_print( - f"'{agda_module}' Could not find imports. Skipping.") + f"'{agda_module}' Could not find imports.") + return + elif len(nonpublic) == 0: + utils.multithread.thread_safe_print( + f"'{agda_module}' No nonpublic imports.") return # Proceed with search for unused imports diff --git a/src/category-theory/anafunctors.lagda.md b/src/category-theory/anafunctors.lagda.md index 1567ab5e66..9e51ae06b8 100644 --- a/src/category-theory/anafunctors.lagda.md +++ b/src/category-theory/anafunctors.lagda.md @@ -39,7 +39,7 @@ anafunctor-Precat l C D = Σ ( (X Y : obj-Precat C) (U : obj-Precat D) (u : F₀ X U) → (V : obj-Precat D) (v : F₀ Y V) → (f : type-hom-Precat C X Y) → type-hom-Precat D U V) - ( λ F₁ → + ( λ F₁ → ( ( X : obj-Precat C) → type-trunc-Prop (Σ (obj-Precat D) (F₀ X))) × ( ( ( X : obj-Precat C) (U : obj-Precat D) (u : F₀ X U) → F₁ X X U u U u (id-hom-Precat C) ＝ id-hom-Precat D) × diff --git a/src/category-theory/isomorphisms-large-precategories.lagda.md b/src/category-theory/isomorphisms-large-precategories.lagda.md index 3c913856e0..71f5a282ce 100644 --- a/src/category-theory/isomorphisms-large-precategories.lagda.md +++ b/src/category-theory/isomorphisms-large-precategories.lagda.md @@ -125,7 +125,7 @@ iso-eq-Large-Precat C X .X refl = id-iso-Large-Precat C Let `f : hom x y` and suppose `g g' : hom y x` are both two-sided inverses to `f`. It is enough to show that `g = g'` since the equalities are propositions (since the hom-types are sets). But we have the following chain of equalities: -`g = comp g id_y = comp g (comp f g') = comp (comp g f) g' = comp id_x g' = g'.` +`g = comp g id_y = comp g (comp f g') = comp (comp g f) g' = comp id_x g' = g'`. ```agda module _ diff --git a/src/commutative-algebra/ideals-commutative-rings.lagda.md b/src/commutative-algebra/ideals-commutative-rings.lagda.md index 3d40507e9f..81b5fcd471 100644 --- a/src/commutative-algebra/ideals-commutative-rings.lagda.md +++ b/src/commutative-algebra/ideals-commutative-rings.lagda.md @@ -13,7 +13,6 @@ open import commutative-algebra.subsets-commutative-rings open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions -open import foundation.subtypes open import foundation.universe-levels open import ring-theory.ideals-rings diff --git a/src/commutative-algebra/ideals-commutative-semirings.lagda.md b/src/commutative-algebra/ideals-commutative-semirings.lagda.md index 5f3fe50661..3acc2a83fe 100644 --- a/src/commutative-algebra/ideals-commutative-semirings.lagda.md +++ b/src/commutative-algebra/ideals-commutative-semirings.lagda.md @@ -13,11 +13,9 @@ open import commutative-algebra.subsets-commutative-semirings open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions -open import foundation.subtypes open import foundation.universe-levels open import ring-theory.ideals-semirings -open import ring-theory.subsets-semirings ```
diff --git a/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md b/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md index 1923b55d1b..2e7e9709f7 100644 --- a/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md +++ b/src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md @@ -4,6 +4,14 @@ module commutative-algebra.maximal-ideals-commutative-rings where ``` +
Imports + +```agda + +``` + +
+ ## Idea Maximal ideals in a commutative ring `R` are proper ideals `I` such that any diff --git a/src/commutative-algebra/nilradical-commutative-rings.lagda.md b/src/commutative-algebra/nilradical-commutative-rings.lagda.md index f5815582a0..e50d07f6c5 100644 --- a/src/commutative-algebra/nilradical-commutative-rings.lagda.md +++ b/src/commutative-algebra/nilradical-commutative-rings.lagda.md @@ -7,30 +7,15 @@ module commutative-algebra.nilradical-commutative-rings where
Imports ```agda -open import commutative-algebra.binomial-theorem-commutative-rings open import commutative-algebra.commutative-rings open import commutative-algebra.ideals-commutative-rings -open import commutative-algebra.powers-of-elements-commutative-rings open import commutative-algebra.subsets-commutative-rings -open import commutative-algebra.sums-commutative-rings -open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.binomial-coefficients -open import elementary-number-theory.distance-natural-numbers -open import elementary-number-theory.inequality-natural-numbers -open import elementary-number-theory.natural-numbers - -open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types -open import foundation.propositional-truncations -open import foundation.subtypes open import foundation.universe-levels open import ring-theory.nilpotent-elements-rings - -open import univalent-combinatorics.coproduct-types -open import univalent-combinatorics.standard-finite-types ```
diff --git a/src/commutative-algebra/powers-of-elements-commutative-rings.lagda.md b/src/commutative-algebra/powers-of-elements-commutative-rings.lagda.md index 3370cf3622..36a04b549d 100644 --- a/src/commutative-algebra/powers-of-elements-commutative-rings.lagda.md +++ b/src/commutative-algebra/powers-of-elements-commutative-rings.lagda.md @@ -13,7 +13,6 @@ open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.parity-natural-numbers -open import foundation.empty-types open import foundation.identity-types open import foundation.universe-levels diff --git a/src/commutative-algebra/prime-ideals-commutative-rings.lagda.md b/src/commutative-algebra/prime-ideals-commutative-rings.lagda.md index 84edf85357..f691c235e0 100644 --- a/src/commutative-algebra/prime-ideals-commutative-rings.lagda.md +++ b/src/commutative-algebra/prime-ideals-commutative-rings.lagda.md @@ -16,7 +16,6 @@ open import foundation.disjunction open import foundation.propositions open import foundation.universe-levels -open import ring-theory.ideals-rings open import ring-theory.subsets-rings ``` diff --git a/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md b/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md index df38249139..803f5c06b9 100644 --- a/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md +++ b/src/commutative-algebra/radicals-of-ideals-commutative-rings.lagda.md @@ -12,24 +12,16 @@ open import commutative-algebra.commutative-rings open import commutative-algebra.ideals-commutative-rings open import commutative-algebra.powers-of-elements-commutative-rings open import commutative-algebra.subsets-commutative-rings -open import commutative-algebra.sums-commutative-rings open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.binomial-coefficients -open import elementary-number-theory.distance-natural-numbers -open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.existential-quantification -open import foundation.identity-types open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels - -open import univalent-combinatorics.coproduct-types -open import univalent-combinatorics.standard-finite-types ``` diff --git a/src/commutative-algebra/sums-commutative-rings.lagda.md b/src/commutative-algebra/sums-commutative-rings.lagda.md index 5ce16d09d1..3d78554b68 100644 --- a/src/commutative-algebra/sums-commutative-rings.lagda.md +++ b/src/commutative-algebra/sums-commutative-rings.lagda.md @@ -180,7 +180,7 @@ module _ shift-sum-Commutative-Ring = shift-sum-Ring (ring-Commutative-Ring R) ``` -### Splitting Sums +### Splitting sums ```agda split-sum-Commutative-Ring : diff --git a/src/commutative-algebra/sums-commutative-semirings.lagda.md b/src/commutative-algebra/sums-commutative-semirings.lagda.md index 63aa2194a2..d629d10693 100644 --- a/src/commutative-algebra/sums-commutative-semirings.lagda.md +++ b/src/commutative-algebra/sums-commutative-semirings.lagda.md @@ -200,7 +200,7 @@ module _ sum-zero-Semiring (semiring-Commutative-Semiring R) ``` -### Splitting Sums +### Splitting sums ```agda split-sum-Commutative-Semiring : diff --git a/src/elementary-number-theory/bezouts-lemma.lagda.md b/src/elementary-number-theory/bezouts-lemma.lagda.md index 57d2e91b8d..4e3793d891 100755 --- a/src/elementary-number-theory/bezouts-lemma.lagda.md +++ b/src/elementary-number-theory/bezouts-lemma.lagda.md @@ -387,7 +387,7 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) = by ap (λ p → add-ℤ (add-ℤ (mul-ℤ (neg-ℤ a) (int-ℕ (succ-ℕ x))) p) (add-ℤ (mul-ℤ (int-ℤ-Mod (succ-ℕ x) u) (int-ℕ y)) (neg-ℤ (mul-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ y))))) - (commutative-mul-ℤ (int-ℕ y) (int-ℕ (succ-ℕ x))) + (commutative-mul-ℤ (int-ℕ y) (int-ℕ (succ-ℕ x))) ＝ add-ℤ (add-ℤ (mul-ℤ (neg-ℤ a) (int-ℕ (succ-ℕ x))) (mul-ℤ (int-ℤ-Mod (succ-ℕ x) u) (int-ℕ y))) (add-ℤ (mul-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ y)) @@ -432,7 +432,7 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) = ＝ dist-ℤ (int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y)) (int-ℕ (mul-ℕ (abs-ℤ a) (succ-ℕ x))) by inv (dist-int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y) - (mul-ℕ (abs-ℤ a) (succ-ℕ x))) + (mul-ℕ (abs-ℤ a) (succ-ℕ x))) ＝ dist-ℤ (int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y)) (mul-ℤ (int-ℕ (abs-ℤ a)) (int-ℕ (succ-ℕ x))) by ap (λ p → dist-ℤ (int-ℕ (mul-ℕ (nat-Fin (succ-ℕ x) u) y)) p) @@ -792,7 +792,7 @@ remainder-min-dist-succ-x-is-distance x y = (int-ℕ (succ-ℕ x)) by ap (λ H → add-ℤ H (int-ℕ (succ-ℕ x))) (distributive-neg-add-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ t)) (int-ℕ y)) - (neg-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ s)) (int-ℕ (succ-ℕ x)))) ) + (neg-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ s)) (int-ℕ (succ-ℕ x))))) ＝ add-ℤ (add-ℤ (neg-ℤ (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ t)) (int-ℕ y))) (mul-ℤ (mul-ℤ (int-ℕ q) (int-ℕ s)) (int-ℕ (succ-ℕ x)))) (int-ℕ (succ-ℕ x)) diff --git a/src/elementary-number-theory/congruence-natural-numbers.lagda.md b/src/elementary-number-theory/congruence-natural-numbers.lagda.md index b84082ab29..f70a84ead1 100644 --- a/src/elementary-number-theory/congruence-natural-numbers.lagda.md +++ b/src/elementary-number-theory/congruence-natural-numbers.lagda.md @@ -160,7 +160,7 @@ is-one-cong-succ-ℕ {k} x H = ```agda scalar-invariant-cong-ℕ : - (k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (mul-ℕ z x) (mul-ℕ z y) + (k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (mul-ℕ z x) (mul-ℕ z y) pr1 (scalar-invariant-cong-ℕ k x y z (pair d p)) = mul-ℕ z d pr2 (scalar-invariant-cong-ℕ k x y z (pair d p)) = ( associative-mul-ℕ z d k) ∙ @@ -181,7 +181,7 @@ scalar-invariant-cong-ℕ' k x y z H = ```agda congruence-mul-ℕ : (k : ℕ) {x y x' y' : ℕ} → - cong-ℕ k x x' → cong-ℕ k y y' → cong-ℕ k (mul-ℕ x y) (mul-ℕ x' y') + cong-ℕ k x x' → cong-ℕ k y y' → cong-ℕ k (mul-ℕ x y) (mul-ℕ x' y') congruence-mul-ℕ k {x} {y} {x'} {y'} H K = trans-cong-ℕ k (mul-ℕ x y) (mul-ℕ x y') (mul-ℕ x' y') ( scalar-invariant-cong-ℕ k y y' x K) diff --git a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md index 7f774c861c..f9ee1dc931 100644 --- a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md +++ b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md @@ -16,7 +16,6 @@ open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.identity-types -open import foundation.negation open import foundation.propositional-maps open import foundation.propositions open import foundation.universe-levels diff --git a/src/elementary-number-theory/finitary-natural-numbers.lagda.md b/src/elementary-number-theory/finitary-natural-numbers.lagda.md index c8f02114b9..1e33a590cf 100644 --- a/src/elementary-number-theory/finitary-natural-numbers.lagda.md +++ b/src/elementary-number-theory/finitary-natural-numbers.lagda.md @@ -204,7 +204,7 @@ issec-inv-convert-based-ℕ : (k n : ℕ) → convert-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n) ＝ n issec-inv-convert-based-ℕ k zero-ℕ = is-zero-nat-zero-Fin {k} issec-inv-convert-based-ℕ k (succ-ℕ n) = - ( convert-based-succ-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n)) ∙ + ( convert-based-succ-based-ℕ (succ-ℕ k) (inv-convert-based-ℕ k n)) ∙ ( ap succ-ℕ (issec-inv-convert-based-ℕ k n)) isretr-inv-convert-based-ℕ : diff --git a/src/elementary-number-theory/goldbach-conjecture.lagda.md b/src/elementary-number-theory/goldbach-conjecture.lagda.md index ae7d10eab9..9b7598344f 100644 --- a/src/elementary-number-theory/goldbach-conjecture.lagda.md +++ b/src/elementary-number-theory/goldbach-conjecture.lagda.md @@ -8,7 +8,6 @@ module elementary-number-theory.goldbach-conjecture where ```agda open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.divisibility-natural-numbers open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.parity-natural-numbers @@ -22,7 +21,7 @@ open import foundation.universe-levels -# The Goldbach Conjecture +## Conjecture ```agda Goldbach-conjecture : UU lzero diff --git a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md index 76437d5ef7..0a4a09f13d 100644 --- a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md +++ b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md @@ -29,7 +29,7 @@ open import foundation.universe-levels -# Greatest common divisors of integers +## Definition ```agda is-common-divisor-ℤ : ℤ → ℤ → ℤ → UU lzero @@ -38,9 +38,13 @@ is-common-divisor-ℤ x y d = (div-ℤ d x) × (div-ℤ d y) is-gcd-ℤ : ℤ → ℤ → ℤ → UU lzero is-gcd-ℤ x y d = is-nonnegative-ℤ d × ((k : ℤ) → is-common-divisor-ℤ x y k ↔ div-ℤ k d) +``` + +## Properties --- We relate divisibility and being a gcd on ℕ and on ℤ +### We relate divisibility and being a gcd on ℕ and on ℤ +```agda is-common-divisor-int-is-common-divisor-ℕ : {x y d : ℕ} → is-common-divisor-ℕ x y d → is-common-divisor-ℤ (int-ℕ x) (int-ℕ y) (int-ℕ d) diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md index 6d77680ae3..87e3757c33 100644 --- a/src/elementary-number-theory/inequality-integers.lagda.md +++ b/src/elementary-number-theory/inequality-integers.lagda.md @@ -1,4 +1,4 @@ -# Inequality of integers +# Inequality on the integers ```agda module elementary-number-theory.inequality-integers where @@ -23,12 +23,16 @@ open import foundation.universe-levels -# Inequality on the integers +## Definition ```agda leq-ℤ : ℤ → ℤ → UU lzero leq-ℤ x y = is-nonnegative-ℤ (diff-ℤ y x) +``` + +## Properties +```agda refl-leq-ℤ : (k : ℤ) → leq-ℤ k k refl-leq-ℤ k = tr is-nonnegative-ℤ (inv (right-inverse-law-add-ℤ k)) star @@ -67,8 +71,6 @@ succ-leq-ℤ k = leq-ℤ-succ-leq-ℤ : (k l : ℤ) → leq-ℤ k l → leq-ℤ k (succ-ℤ l) leq-ℤ-succ-leq-ℤ k l p = trans-leq-ℤ k l (succ-ℤ l) p (succ-leq-ℤ l) --- Bureaucracy - concatenate-eq-leq-eq-ℤ : {x' x y y' : ℤ} → x' ＝ x → leq-ℤ x y → y ＝ y' → leq-ℤ x' y' concatenate-eq-leq-eq-ℤ refl H refl = H @@ -82,16 +84,16 @@ concatenate-eq-leq-ℤ : concatenate-eq-leq-ℤ y refl H = H ``` -## The strict ordering on ℤ +### The strict ordering on ℤ ```agda le-ℤ : ℤ → ℤ → UU lzero le-ℤ x y = is-positive-ℤ (diff-ℤ x y) ``` -```agda --- We show that ℤ is an ordered ring +## ℤ is an ordered ring +```agda preserves-order-add-ℤ' : {x y : ℤ} (z : ℤ) → leq-ℤ x y → leq-ℤ (add-ℤ x z) (add-ℤ y z) preserves-order-add-ℤ' {x} {y} z = diff --git a/src/elementary-number-theory/inequality-natural-numbers.lagda.md b/src/elementary-number-theory/inequality-natural-numbers.lagda.md index 9705070abb..11f61fff54 100644 --- a/src/elementary-number-theory/inequality-natural-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-natural-numbers.lagda.md @@ -570,8 +570,6 @@ preserves-leq-add-ℕ {m} {m'} {n} {n'} H K = -------------------------------------------------------------------------------- --- We prove some lemmas about inequalities -- - leq-add-ℕ : (m n : ℕ) → m ≤-ℕ (add-ℕ m n) leq-add-ℕ m zero-ℕ = refl-leq-ℕ m leq-add-ℕ m (succ-ℕ n) = diff --git a/src/elementary-number-theory/integer-partitions.lagda.md b/src/elementary-number-theory/integer-partitions.lagda.md index 3eee4de233..7e497c9fc8 100644 --- a/src/elementary-number-theory/integer-partitions.lagda.md +++ b/src/elementary-number-theory/integer-partitions.lagda.md @@ -2,20 +2,16 @@ ```agda module elementary-number-theory.integer-partitions where +``` -open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.natural-numbers -open import elementary-number-theory.nonzero-natural-numbers +
Imports -open import foundation.dependent-pair-types -open import foundation.fibers-of-maps -open import foundation.identity-types -open import foundation.universe-levels +```agda -open import univalent-combinatorics.finite-types -open import univalent-combinatorics.lists ``` +
+ ## Idea An integer partition of a natural number n is a list of nonzero natural numbers diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md index a353c12fb8..978c970e67 100644 --- a/src/elementary-number-theory/integers.lagda.md +++ b/src/elementary-number-theory/integers.lagda.md @@ -314,9 +314,6 @@ pr2 positive-ℤ-Set = is-set-positive-ℤ int-positive-ℤ : positive-ℤ → ℤ int-positive-ℤ = pr1 --- arst : (x y : positive-ℤ) → (int-positive-ℤ x ＝ int-positive-ℤ y) → x ＝ y --- arst (pair (inr (inr x)) is-pos-x) y p = _ -- {!ex-falso is-pos-x!} - is-positive-int-positive-ℤ : (x : positive-ℤ) → is-positive-ℤ (int-positive-ℤ x) is-positive-int-positive-ℤ = pr2 diff --git a/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md b/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md index ce1ffcd79c..e902286c6a 100644 --- a/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md +++ b/src/elementary-number-theory/modular-arithmetic-standard-finite-types.lagda.md @@ -446,7 +446,7 @@ is-add-one-succ-Fin' : is-add-one-succ-Fin' zero-ℕ (inr star) = refl is-add-one-succ-Fin' (succ-ℕ k) x = ( ap (succ-Fin (succ-ℕ (succ-ℕ k))) (inv (issec-nat-Fin (succ-ℕ k) x))) ∙ - ( ap ( mod-succ-ℕ (succ-ℕ k)) + ( ap ( mod-succ-ℕ (succ-ℕ k)) ( ap ( add-ℕ (nat-Fin (succ-ℕ (succ-ℕ k)) x)) ( inv (is-one-nat-one-Fin (succ-ℕ k))))) diff --git a/src/elementary-number-theory/modular-arithmetic.lagda.md b/src/elementary-number-theory/modular-arithmetic.lagda.md index 0cff8776d2..50fd1a07b7 100644 --- a/src/elementary-number-theory/modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/modular-arithmetic.lagda.md @@ -135,7 +135,7 @@ is-zero-int-zero-ℤ-Mod (zero-ℕ) = refl is-zero-int-zero-ℤ-Mod (succ-ℕ k) = ap int-ℕ (is-zero-nat-zero-Fin {k}) int-ℤ-Mod-bounded : (k : ℕ) → (x : ℤ-Mod (succ-ℕ k)) - → leq-ℤ (int-ℤ-Mod (succ-ℕ k) x) (int-ℕ (succ-ℕ k)) + → leq-ℤ (int-ℤ-Mod (succ-ℕ k) x) (int-ℕ (succ-ℕ k)) int-ℤ-Mod-bounded zero-ℕ (inr x) = star int-ℤ-Mod-bounded (succ-ℕ k) (inl x) = is-nonnegative-succ-ℤ (add-ℤ (inr (inr k)) diff --git a/src/elementary-number-theory/multiplication-integers.lagda.md b/src/elementary-number-theory/multiplication-integers.lagda.md index d33d510067..22f8a64287 100644 --- a/src/elementary-number-theory/multiplication-integers.lagda.md +++ b/src/elementary-number-theory/multiplication-integers.lagda.md @@ -480,9 +480,11 @@ is-positive-right-factor-mul-ℤ : {x y : ℤ} → is-positive-ℤ (mul-ℤ x y) → is-positive-ℤ x → is-positive-ℤ y is-positive-right-factor-mul-ℤ {x} {y} H = is-positive-left-factor-mul-ℤ (is-positive-eq-ℤ (commutative-mul-ℤ x y) H) +``` --- Lemmas about nonnegative integers +### Lemmas about nonnegative integers +```agda is-nonnegative-mul-ℤ : {x y : ℤ} → is-nonnegative-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (mul-ℤ x y) diff --git a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md index 046cdcfc9b..cbe4e09be0 100644 --- a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md @@ -205,9 +205,11 @@ is-nonzero-left-factor-mul-ℕ .zero-ℕ y H refl = H (left-zero-law-mul-ℕ y) is-nonzero-right-factor-mul-ℕ : (x y : ℕ) → is-nonzero-ℕ (mul-ℕ x y) → is-nonzero-ℕ y is-nonzero-right-factor-mul-ℕ x .zero-ℕ H refl = H (right-zero-law-mul-ℕ x) +``` --- We conclude that y = 1 if (x+1)y = x+1 +We conclude that $y = 1$ if $(x+1)y = x+1$. +```agda is-one-is-right-unit-mul-ℕ : (x y : ℕ) → mul-ℕ (succ-ℕ x) y ＝ succ-ℕ x → is-one-ℕ y is-one-is-right-unit-mul-ℕ x y p = diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index 7953c556c0..6675637f50 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/src/elementary-number-theory/rational-numbers.lagda.md @@ -39,7 +39,7 @@ equivalence relation given by `(n/m) ~ (n'/m') := Id (mul-ℤ n m') (mul-ℤ n' ## Definitions -### Reduced Fraction +### Reduced fraction ```agda is-reduced-fraction-ℤ : fraction-ℤ → UU lzero diff --git a/src/elementary-number-theory/sums-of-natural-numbers.lagda.md b/src/elementary-number-theory/sums-of-natural-numbers.lagda.md index a46555dd52..b51ad816ca 100644 --- a/src/elementary-number-theory/sums-of-natural-numbers.lagda.md +++ b/src/elementary-number-theory/sums-of-natural-numbers.lagda.md @@ -99,5 +99,8 @@ abstract ### Each of the summands is less than or equal to the total sum --- -`agda -- leq-sum-Fin-ℕ : -- {k : ℕ} (f : Fin k → ℕ) (x : Fin k) → leq-ℕ (f x) (sum-Fin-ℕ f) -- leq-sum-Fin-ℕ {succ-ℕ k} f x = {!leq-add-ℕ!} -- ` +```agda +-- leq-sum-Fin-ℕ : +-- {k : ℕ} (f : Fin k → ℕ) (x : Fin k) → leq-ℕ (f x) (sum-Fin-ℕ f) +-- leq-sum-Fin-ℕ {succ-ℕ k} f x = {!leq-add-ℕ!} +``` diff --git a/src/elementary-number-theory/twin-prime-conjecture.lagda.md b/src/elementary-number-theory/twin-prime-conjecture.lagda.md index d2bb74e6c5..ae5acadc67 100644 --- a/src/elementary-number-theory/twin-prime-conjecture.lagda.md +++ b/src/elementary-number-theory/twin-prime-conjecture.lagda.md @@ -20,14 +20,14 @@ open import foundation.universe-levels # The twin prime conjecture +The twin prime conjecture asserts that there are infinitely many twin primes. We +assert that there are infinitely twin primes by asserting that for every n : ℕ +there is a twin prime that is larger than n. + ```agda is-twin-prime-ℕ : ℕ → UU lzero is-twin-prime-ℕ n = (is-prime-ℕ n) × (is-prime-ℕ (succ-ℕ (succ-ℕ n))) -{- The twin prime conjecture asserts that there are infinitely many twin - primes. We assert that there are infinitely twin primes by asserting that - for every n : ℕ there is a twin prime that is larger than n. -} - twin-prime-conjecture : UU lzero twin-prime-conjecture = (n : ℕ) → Σ ℕ (λ p → (is-twin-prime-ℕ p) × (leq-ℕ n p)) diff --git a/src/elementary-number-theory/well-ordering-principle-natural-numbers.lagda.md b/src/elementary-number-theory/well-ordering-principle-natural-numbers.lagda.md index 8c268ab904..d2c190ddc2 100644 --- a/src/elementary-number-theory/well-ordering-principle-natural-numbers.lagda.md +++ b/src/elementary-number-theory/well-ordering-principle-natural-numbers.lagda.md @@ -119,10 +119,13 @@ number-well-ordering-principle-ℕ : {l : Level} (P : ℕ → UU l) (d : is-decidable-fam P) (nP : Σ ℕ P) → ℕ number-well-ordering-principle-ℕ P d nP = pr1 (well-ordering-principle-ℕ P d nP) +``` + +### The well-ordering principle returns `0` if `P 0` holds -{- Also show that the well-ordering principle returns 0 if P 0 holds, - independently of the input (pair n p) : Σ ℕ P. -} +This is independently of the input `(pair n p) : Σ ℕ P`. +```agda is-zero-well-ordering-principle-succ-ℕ : {l : Level} (P : ℕ → UU l) (d : is-decidable-fam P) (n : ℕ) (p : P (succ-ℕ n)) (d0 : is-decidable (P zero-ℕ)) → diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md index 95cbfa2d80..e05681a631 100644 --- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md @@ -1283,7 +1283,7 @@ module _ ( Fin-UU-Fin l1 (succ-ℕ (succ-ℕ n))) ( star) ( compute-raise-Fin l1 (succ-ℕ (succ-ℕ n)))))))) - ( inv + ( inv ( comp-eq-equiv ( raise l4 (Fin 2)) ( equivalence-class diff --git a/src/finite-group-theory/finite-type-groups.lagda.md b/src/finite-group-theory/finite-type-groups.lagda.md index 4beccbc058..2b213865af 100644 --- a/src/finite-group-theory/finite-type-groups.lagda.md +++ b/src/finite-group-theory/finite-type-groups.lagda.md @@ -122,7 +122,7 @@ module _ ( λ p → ( ap ( λ r → eq-pair-Σ (pr1 (pair-eq-Σ p)) r) - ( eq-is-prop (is-trunc-Id (is-prop-type-trunc-Prop _ _)))) ∙ + ( eq-is-prop (is-trunc-Id (is-prop-type-trunc-Prop _ _)))) ∙ ( issec-pair-eq-Σ (Fin-UU-Fin l n) (Fin-UU-Fin l n) p))) ( eq-is-prop ( is-prop-preserves-mul-Semigroup diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index 29984d1fd8..0a6805d7dd 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -1,4 +1,4 @@ -# Foundation Core +# Foundation core ```agda module foundation-core where diff --git a/src/foundation-core/cones-pullbacks.lagda.md b/src/foundation-core/cones-pullbacks.lagda.md index b1c5c58639..75524f9b34 100644 --- a/src/foundation-core/cones-pullbacks.lagda.md +++ b/src/foundation-core/cones-pullbacks.lagda.md @@ -254,7 +254,7 @@ module _ ( coherence-square-cone f' g' c')) fam-htpy-parallel-cone : - {l4 : Level} {C : UU l4} (c : cone f g C) → (c' : cone f' g' C) → + {l4 : Level} {C : UU l4} (c : cone f g C) → (c' : cone f' g' C) → (vertical-map-cone f g c ~ vertical-map-cone f' g' c') → UU _ fam-htpy-parallel-cone c c' Hp = Σ ( horizontal-map-cone f g c ~ horizontal-map-cone f' g' c') diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md index c4ca6c0d7b..11599baeb5 100644 --- a/src/foundation-core/contractible-types.lagda.md +++ b/src/foundation-core/contractible-types.lagda.md @@ -189,7 +189,7 @@ module _ ( A × B) ( pair ( pair (pr1 (center is-contr-AB))) - ( pair pr2 (λ x → refl)) ) + ( pair pr2 (λ x → refl)) ) ( is-contr-AB) module _ diff --git a/src/foundation-core/coproduct-types.lagda.md b/src/foundation-core/coproduct-types.lagda.md index e985f78a67..fc390ffb2c 100644 --- a/src/foundation-core/coproduct-types.lagda.md +++ b/src/foundation-core/coproduct-types.lagda.md @@ -24,7 +24,7 @@ of `A` and `B`. ## Definition ```agda -data _+_ {l1 l2 : Level} (A : UU l1) (B : UU l2) : UU (l1 ⊔ l2) where +data _+_ {l1 l2 : Level} (A : UU l1) (B : UU l2) : UU (l1 ⊔ l2) where inl : A → A + B inr : B → A + B diff --git a/src/foundation-core/equivalence-induction.lagda.md b/src/foundation-core/equivalence-induction.lagda.md index 4a69c16592..93b979e03d 100644 --- a/src/foundation-core/equivalence-induction.lagda.md +++ b/src/foundation-core/equivalence-induction.lagda.md @@ -62,8 +62,8 @@ module _ ( pair A id-equiv) ( pair ( pair A id-equiv) - ( λ t → ( inv (contraction c (pair A id-equiv))) ∙ - ( contraction c t))) + ( λ t → ( inv (contraction c (pair A id-equiv))) ∙ + ( contraction c t))) ( P)) -- Theorem 17.1.1 (iii) implies (ii) diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index 6e099fd7d7..3edc248d7b 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -123,7 +123,7 @@ module _ is-equiv-has-inverse' (pair g (pair H K)) has-inverse-is-equiv : is-equiv f → has-inverse f - pr1 (has-inverse-is-equiv (pair (pair g G) (pair h H))) = g + pr1 (has-inverse-is-equiv (pair (pair g G) (pair h H))) = g pr1 (pr2 (has-inverse-is-equiv (pair (pair g G) (pair h H)))) = G pr2 (pr2 (has-inverse-is-equiv (pair (pair g G) (pair h H)))) = (((inv-htpy (H ·r g)) ∙h (h ·l G)) ·r f) ∙h H @@ -352,7 +352,7 @@ module _ abstract is-equiv-is-retraction : {i j : Level} {A : UU i} {B : UU j} {f : A → B} {g : B → A} → - is-equiv f → (g ∘ f) ~ id → is-equiv g + is-equiv f → (g ∘ f) ~ id → is-equiv g is-equiv-is-retraction {A = A} {f = f} {g = g} is-equiv-f H = is-equiv-left-factor-htpy id g f (inv-htpy H) is-equiv-id is-equiv-f ``` diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md index 497762a6e1..35498f9478 100644 --- a/src/foundation-core/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation-core/functoriality-dependent-pair-types.lagda.md @@ -40,9 +40,11 @@ module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} (f : (x : A) → B x → C x) where +``` - {- Any family of maps induces a map on the total spaces. -} +Any family of maps induces a map on the total spaces. +```agda tot : Σ A B → Σ A C pr1 (tot t) = pr1 t pr2 (tot t) = f (pr1 t) (pr2 t) @@ -128,13 +130,14 @@ tot-comp f g (pair x y) = refl ### The fibers of `tot` +We show that for any family of maps, the fiber of the induced map on total +spaces are equivalent to the fibers of the maps in the family. + ```agda module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} (f : (x : A) → B x → C x) where - {- We show that for any family of maps, the fiber of the induced map on total - spaces are equivalent to the fibers of the maps in the family. -} map-compute-fib-tot : (t : Σ A C) → fib (tot f) t → fib (f (pr1 t)) (pr2 t) pr1 (map-compute-fib-tot .(tot f (pair x y)) (pair (pair x y) refl)) = y diff --git a/src/foundation-core/truncated-maps.lagda.md b/src/foundation-core/truncated-maps.lagda.md index 471b9b603f..b41a901fb1 100644 --- a/src/foundation-core/truncated-maps.lagda.md +++ b/src/foundation-core/truncated-maps.lagda.md @@ -314,7 +314,7 @@ module _ ```agda module _ - {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} {C : A → UU l3} {f : (x : A) → B x → C x} where diff --git a/src/foundation-core/truncated-types.lagda.md b/src/foundation-core/truncated-types.lagda.md index 5b16e221a9..6eed38b8d1 100644 --- a/src/foundation-core/truncated-types.lagda.md +++ b/src/foundation-core/truncated-types.lagda.md @@ -143,7 +143,7 @@ abstract is-trunc-is-equiv' : {l1 l2 : Level} (k : 𝕋) (A : UU l1) {B : UU l2} (f : A → B) → is-equiv f → is-trunc k A → is-trunc k B - is-trunc-is-equiv' k A f is-equiv-f is-trunc-A = + is-trunc-is-equiv' k A f is-equiv-f is-trunc-A = is-trunc-is-equiv k A ( map-inv-is-equiv is-equiv-f) ( is-equiv-map-inv-is-equiv is-equiv-f) diff --git a/src/foundation-core/universal-property-pullbacks.lagda.md b/src/foundation-core/universal-property-pullbacks.lagda.md index 6ff3363d71..2d4cf60798 100644 --- a/src/foundation-core/universal-property-pullbacks.lagda.md +++ b/src/foundation-core/universal-property-pullbacks.lagda.md @@ -122,5 +122,5 @@ module _ ( Σ (C' → C) (λ h → cone-map f g c h ＝ c')) ( equiv-tot ( λ h → extensionality-cone f g (cone-map f g c h) c')) - ( is-contr-map-is-equiv (up C') c') + ( is-contr-map-is-equiv (up C') c') ``` diff --git a/src/foundation/0-maps.lagda.md b/src/foundation/0-maps.lagda.md index 831611983b..6a9549dc73 100644 --- a/src/foundation/0-maps.lagda.md +++ b/src/foundation/0-maps.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.0-maps where +``` + +
Imports +```agda open import foundation-core.0-maps public ``` + +
diff --git a/src/foundation/algebras-polynomial-endofunctors.lagda.md b/src/foundation/algebras-polynomial-endofunctors.lagda.md index 655598543f..2bd9a0be0b 100644 --- a/src/foundation/algebras-polynomial-endofunctors.lagda.md +++ b/src/foundation/algebras-polynomial-endofunctors.lagda.md @@ -55,8 +55,6 @@ structure-algebra-polynomial-endofunctor X = pr2 X ### Morphisms of algebras for polynomial endofunctors ```agda --- Morphisms of algebras for polynomial endofunctors - hom-algebra-polynomial-endofunctor : {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} (X : algebra-polynomial-endofunctor-UU l3 A B) → diff --git a/src/foundation/automorphisms.lagda.md b/src/foundation/automorphisms.lagda.md index 683bb3f17e..77eabc4698 100644 --- a/src/foundation/automorphisms.lagda.md +++ b/src/foundation/automorphisms.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.automorphisms where +``` + +
Imports +```agda open import foundation-core.automorphisms public ``` + +
diff --git a/src/foundation/binary-equivalences.lagda.md b/src/foundation/binary-equivalences.lagda.md index 019bf5975c..10003b3b8b 100644 --- a/src/foundation/binary-equivalences.lagda.md +++ b/src/foundation/binary-equivalences.lagda.md @@ -21,9 +21,9 @@ A binary operation `f : A → B → C` is said to be a binary equivalence if the functions `λ x → f x b` and `λ y → f a y` are equivalences for each `a : A` and `b : B` respectively. -```agda -{- Binary equivalences and binary embeddings -} +## Definitions +```agda fix-left : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B → C) → A → B → C diff --git a/src/foundation/binary-operations-unordered-pairs-of-types.lagda.md b/src/foundation/binary-operations-unordered-pairs-of-types.lagda.md index 3fcadf20d7..6ddb84fbbb 100644 --- a/src/foundation/binary-operations-unordered-pairs-of-types.lagda.md +++ b/src/foundation/binary-operations-unordered-pairs-of-types.lagda.md @@ -18,7 +18,7 @@ open import foundation-core.universe-levels ## Idea A binary operation on an unordered pair of types A indexed by a 2-element type I -is a map `((i : I) → A i) → B`. +is a map `((i : I) → A i) → B`. ## Definition diff --git a/src/foundation/boolean-reflection.lagda.md b/src/foundation/boolean-reflection.lagda.md index 7e93ecf0e8..4d012fe43b 100644 --- a/src/foundation/boolean-reflection.lagda.md +++ b/src/foundation/boolean-reflection.lagda.md @@ -1,4 +1,4 @@ -# Boolean Reflection +# Boolean reflection ```agda module foundation.boolean-reflection where diff --git a/src/foundation/booleans.lagda.md b/src/foundation/booleans.lagda.md index 04a02cda77..094d865dbc 100644 --- a/src/foundation/booleans.lagda.md +++ b/src/foundation/booleans.lagda.md @@ -44,7 +44,7 @@ data bool : UU lzero where true false : bool {-# BUILTIN BOOL bool #-} -{-# BUILTIN TRUE true #-} +{-# BUILTIN TRUE true #-} {-# BUILTIN FALSE false #-} ``` diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md index 5efd913fd8..d603e9bb1b 100644 --- a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md +++ b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md @@ -1,4 +1,4 @@ -# The Cantor-Schröder-Bernstein-Escardó theorem +# The Cantor–Schröder–Bernstein–Escardó theorem ```agda module foundation.cantor-schroder-bernstein-escardo where @@ -111,7 +111,7 @@ module _ map-Cantor-Schröder-Bernstein-Escardó' (map-emb g y) d ＝ y ψ (inl v') = is-retr-inverse-of-perfect-image {is-emb-g = is-emb-map-emb g} y v' - ψ (inr v) = ex-falso (v γ) + ψ (inr v) = ex-falso (v γ) a (inr γ) = pair x ψ where w : diff --git a/src/foundation/cartesian-product-types.lagda.md b/src/foundation/cartesian-product-types.lagda.md index e811b215dd..51457808b3 100644 --- a/src/foundation/cartesian-product-types.lagda.md +++ b/src/foundation/cartesian-product-types.lagda.md @@ -2,8 +2,13 @@ ```agda {-# OPTIONS --safe #-} - module foundation.cartesian-product-types where +``` + +
Imports +```agda open import foundation-core.cartesian-product-types public ``` + +
diff --git a/src/foundation/commuting-3-simplices-of-homotopies.lagda.md b/src/foundation/commuting-3-simplices-of-homotopies.lagda.md index 0d02c0a52f..b4cd90278e 100644 --- a/src/foundation/commuting-3-simplices-of-homotopies.lagda.md +++ b/src/foundation/commuting-3-simplices-of-homotopies.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.commuting-3-simplices-of-homotopies where +``` + +
Imports +```agda open import foundation-core.commuting-3-simplices-of-homotopies public ``` + +
diff --git a/src/foundation/commuting-3-simplices-of-maps.lagda.md b/src/foundation/commuting-3-simplices-of-maps.lagda.md index b7b98b9246..62d1386a38 100644 --- a/src/foundation/commuting-3-simplices-of-maps.lagda.md +++ b/src/foundation/commuting-3-simplices-of-maps.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.commuting-3-simplices-of-maps where +``` + +
Imports +```agda open import foundation-core.commuting-3-simplices-of-maps public ``` + +
diff --git a/src/foundation/commuting-triangles-of-homotopies.lagda.md b/src/foundation/commuting-triangles-of-homotopies.lagda.md index 4d1c7242dc..ab831beb32 100644 --- a/src/foundation/commuting-triangles-of-homotopies.lagda.md +++ b/src/foundation/commuting-triangles-of-homotopies.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.commuting-triangles-of-homotopies where +``` + +
Imports +```agda open import foundation-core.commuting-triangles-of-homotopies public ``` + +
diff --git a/src/foundation/cones-pullbacks.lagda.md b/src/foundation/cones-pullbacks.lagda.md index 41374973e3..719c276769 100644 --- a/src/foundation/cones-pullbacks.lagda.md +++ b/src/foundation/cones-pullbacks.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.cones-pullbacks where +``` + +
Imports +```agda open import foundation-core.cones-pullbacks public ``` + +
diff --git a/src/foundation/coproduct-types.lagda.md b/src/foundation/coproduct-types.lagda.md index 9b34cd4cbb..5ee19f83a8 100644 --- a/src/foundation/coproduct-types.lagda.md +++ b/src/foundation/coproduct-types.lagda.md @@ -152,7 +152,7 @@ module _ is-not-contractible-coprod-is-contr : is-contr A → is-contr B → is-not-contractible (A + B) is-not-contractible-coprod-is-contr HA HB HAB = - neq-inl-inr {x = center HA} {y = center HB} (eq-is-contr HAB) + neq-inl-inr {x = center HA} {y = center HB} (eq-is-contr HAB) ``` ### Coproducts of mutually exclusive propositions are propositions diff --git a/src/foundation/cospans.lagda.md b/src/foundation/cospans.lagda.md index a49b6ddee8..764ed026e3 100644 --- a/src/foundation/cospans.lagda.md +++ b/src/foundation/cospans.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.cospans where +``` + +
Imports +```agda open import foundation-core.cospans public ``` + +
diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md index b70b1ba1d9..72a18ce68b 100644 --- a/src/foundation/decidable-embeddings.lagda.md +++ b/src/foundation/decidable-embeddings.lagda.md @@ -7,7 +7,6 @@ module foundation.decidable-embeddings where
Imports ```agda -open import foundation.decidable-equality open import foundation.decidable-maps open import foundation.decidable-subtypes open import foundation.decidable-types diff --git a/src/foundation/decidable-equivalence-relations.lagda.md b/src/foundation/decidable-equivalence-relations.lagda.md index b67ee8d8a6..195ea83633 100644 --- a/src/foundation/decidable-equivalence-relations.lagda.md +++ b/src/foundation/decidable-equivalence-relations.lagda.md @@ -7,44 +7,42 @@ module foundation.decidable-equivalence-relations where
Imports ```agda -open import foundation.cartesian-product-types -open import foundation.contractible-types -open import foundation.coproduct-types open import foundation.decidable-equality open import foundation.decidable-propositions open import foundation.decidable-relations open import foundation.decidable-subtypes open import foundation.decidable-types -open import foundation.dependent-pair-types -open import foundation.diagonal-maps-of-types open import foundation.effective-maps-equivalence-relations open import foundation.equivalence-classes open import foundation.equivalence-relations open import foundation.existential-quantification open import foundation.function-extensionality -open import foundation.functions open import foundation.functoriality-cartesian-product-types -open import foundation.functoriality-dependent-pair-types -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopies -open import foundation.identity-types open import foundation.images open import foundation.propositional-truncations open import foundation.reflecting-maps-equivalence-relations open import foundation.sets open import foundation.slice open import foundation.surjective-maps -open import foundation.type-arithmetic-cartesian-product-types -open import foundation.type-arithmetic-dependent-pair-types open import foundation.universal-property-image +open import foundation-core.cartesian-product-types +open import foundation-core.contractible-types +open import foundation-core.dependent-pair-types open import foundation-core.embeddings open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps +open import foundation-core.functions +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.fundamental-theorem-of-identity-types +open import foundation-core.homotopies +open import foundation-core.identity-types open import foundation-core.logical-equivalences open import foundation-core.propositions open import foundation-core.subtypes +open import foundation-core.type-arithmetic-cartesian-product-types +open import foundation-core.type-arithmetic-dependent-pair-types open import foundation-core.universe-levels ``` diff --git a/src/foundation/decidable-maps.lagda.md b/src/foundation/decidable-maps.lagda.md index ee65535f0b..85be938057 100644 --- a/src/foundation/decidable-maps.lagda.md +++ b/src/foundation/decidable-maps.lagda.md @@ -9,12 +9,12 @@ module foundation.decidable-maps where ```agda open import foundation.decidable-equality open import foundation.decidable-types -open import foundation.equivalences -open import foundation.functoriality-dependent-pair-types open import foundation-core.dependent-pair-types +open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.functions +open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.retractions open import foundation-core.universe-levels diff --git a/src/foundation/decidable-relations.lagda.md b/src/foundation/decidable-relations.lagda.md index 52ce7250be..184ea70753 100644 --- a/src/foundation/decidable-relations.lagda.md +++ b/src/foundation/decidable-relations.lagda.md @@ -9,14 +9,13 @@ module foundation.decidable-relations where ```agda open import foundation.binary-relations open import foundation.decidable-types -open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.functoriality-dependent-pair-types -open import foundation.homotopies -open import foundation.propositions -open import foundation.universe-levels open import foundation-core.decidable-propositions +open import foundation-core.dependent-pair-types +open import foundation-core.equivalences +open import foundation-core.homotopies +open import foundation-core.propositions +open import foundation-core.universe-levels ```
diff --git a/src/foundation/decidable-types.lagda.md b/src/foundation/decidable-types.lagda.md index 6568688b2f..28e5c2cc98 100644 --- a/src/foundation/decidable-types.lagda.md +++ b/src/foundation/decidable-types.lagda.md @@ -38,7 +38,7 @@ using the propositional truncation. ## Definition -### The Curry-Howard interpretation of decidability +### The Curry–Howard interpretation of decidability ```agda is-decidable : {l : Level} (A : UU l) → UU l diff --git a/src/foundation/dependent-binomial-theorem.lagda.md b/src/foundation/dependent-binomial-theorem.lagda.md index e016cd4ff1..ae54661876 100644 --- a/src/foundation/dependent-binomial-theorem.lagda.md +++ b/src/foundation/dependent-binomial-theorem.lagda.md @@ -39,7 +39,7 @@ module _ where fam-coprod : - Fin 2 → UU (l1 ⊔ l2) + Fin 2 → UU (l1 ⊔ l2) fam-coprod (inl (inr star)) = raise l2 A fam-coprod (inr star) = raise l1 B diff --git a/src/foundation/dependent-pair-types.lagda.md b/src/foundation/dependent-pair-types.lagda.md index 2f4c75141c..a6646527de 100644 --- a/src/foundation/dependent-pair-types.lagda.md +++ b/src/foundation/dependent-pair-types.lagda.md @@ -2,8 +2,13 @@ ```agda {-# OPTIONS --safe #-} - module foundation.dependent-pair-types where +``` + +
Imports +```agda open import foundation-core.dependent-pair-types public ``` + +
diff --git a/src/foundation/dependent-paths.lagda.md b/src/foundation/dependent-paths.lagda.md index 9f6d3bb92f..ece4a9dd2f 100644 --- a/src/foundation/dependent-paths.lagda.md +++ b/src/foundation/dependent-paths.lagda.md @@ -143,7 +143,7 @@ module _ where d-concat : path-over B (p01 ∙ p12) b0 b2 - d-concat = (tr-concat {B = B} p01 p12 b0) ∙ ((ap (tr B p12) q01) ∙ (q12)) + d-concat = (tr-concat {B = B} p01 p12 b0) ∙ ((ap (tr B p12) q01) ∙ (q12)) module _ {l1 l2 : Level} {A : UU l1} {a0 a1 : A} (B : A → UU l2) (p01 : a0 ＝ a1) {b0 : B a0} {b1 : B a1} @@ -151,7 +151,7 @@ module _ where d-inv : path-over B (inv p01) b1 b0 - d-inv = (inv (ap (tr B (inv p01)) q01)) ∙ ((inv (tr-concat {B = B} (p01) (inv p01) b0)) ∙ ( + d-inv = (inv (ap (tr B (inv p01)) q01)) ∙ ((inv (tr-concat {B = B} (p01) (inv p01) b0)) ∙ ( ap (λ t → tr B t b0) (right-inv p01))) ``` @@ -181,7 +181,7 @@ module _ d-concat B p01 q01 p12 q12) p23 q23)) ＝ d-concat B p01 q01 (p12 ∙ p23) (d-concat B p12 q12 p23 q23) d-assoc' p01 q01 p12 q12 p23 q23 = - tr-path-over-path-over² B (assoc p01 p12 p23) + tr-path-over-path-over² B (assoc p01 p12 p23) (d-concat B (p01 ∙ p12) (d-concat B p01 q01 p12 q12) p23 q23) (d-concat B p01 q01 (p12 ∙ p23) (d-concat B p12 q12 p23 q23)) (d-assoc p01 q01 p12 q12 p23 q23) @@ -213,14 +213,14 @@ module _ d-right-inv' : (p : a0 ＝ a1) (q : path-over B p b0 b1) → (tr (λ t → path-over B t b0 b0) (right-inv p) (d-concat B p q (inv p) (d-inv B p q))) ＝ ( refl-path-over B a0 b0) - d-right-inv' p q = tr-path-over-path-over² B (right-inv p) + d-right-inv' p q = tr-path-over-path-over² B (right-inv p) (d-concat B p q (inv p) (d-inv B p q)) (refl-path-over B a0 b0) (d-right-inv p q) d-left-inv : (p : a0 ＝ a1) (q : path-over B p b0 b1) → path-over² B (left-inv p) (d-concat B (inv p) (d-inv B p q) p q) (refl-path-over B a1 b1) d-left-inv refl refl = refl - d-left-inv' : (p : a0 ＝ a1) (q : path-over B p b0 b1) → + d-left-inv' : (p : a0 ＝ a1) (q : path-over B p b0 b1) → (tr (λ t → path-over B t b1 b1) (left-inv p) (d-concat B (inv p) (d-inv B p q) p q)) ＝ ( refl-path-over B a1 b1) d-left-inv' p q = tr-path-over-path-over² B (left-inv p) diff --git a/src/foundation/discrete-relaxed-sigma-decompositions.lagda.md b/src/foundation/discrete-relaxed-sigma-decompositions.lagda.md index b632e5f6c1..7cab80a7c4 100644 --- a/src/foundation/discrete-relaxed-sigma-decompositions.lagda.md +++ b/src/foundation/discrete-relaxed-sigma-decompositions.lagda.md @@ -8,19 +8,18 @@ module foundation.discrete-relaxed-sigma-decompositions where ```agda open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.equality-dependent-pair-types open import foundation.equivalences -open import foundation.functions -open import foundation.functoriality-propositional-truncation -open import foundation.identity-types -open import foundation.propositional-truncations -open import foundation.propositions open import foundation.relaxed-sigma-decompositions -open import foundation.subtypes -open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type -open import foundation.universe-levels + +open import foundation-core.dependent-pair-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.functions +open import foundation-core.identity-types +open import foundation-core.propositions +open import foundation-core.subtypes +open import foundation-core.type-arithmetic-dependent-pair-types +open import foundation-core.universe-levels ```
diff --git a/src/foundation/discrete-sigma-decompositions.lagda.md b/src/foundation/discrete-sigma-decompositions.lagda.md index af84843f62..69217d7449 100644 --- a/src/foundation/discrete-sigma-decompositions.lagda.md +++ b/src/foundation/discrete-sigma-decompositions.lagda.md @@ -8,19 +8,19 @@ module foundation.discrete-sigma-decompositions where ```agda open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.equality-dependent-pair-types open import foundation.equivalences -open import foundation.functions -open import foundation.functoriality-propositional-truncation -open import foundation.identity-types open import foundation.propositional-truncations -open import foundation.propositions open import foundation.sigma-decompositions -open import foundation.subtypes -open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type -open import foundation.universe-levels + +open import foundation-core.dependent-pair-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.functions +open import foundation-core.identity-types +open import foundation-core.propositions +open import foundation-core.subtypes +open import foundation-core.type-arithmetic-dependent-pair-types +open import foundation-core.universe-levels ``` diff --git a/src/foundation/epimorphisms-with-respect-to-sets.lagda.md b/src/foundation/epimorphisms-with-respect-to-sets.lagda.md index a84ec6149e..938cc75b20 100644 --- a/src/foundation/epimorphisms-with-respect-to-sets.lagda.md +++ b/src/foundation/epimorphisms-with-respect-to-sets.lagda.md @@ -61,7 +61,7 @@ abstract ( Id-Prop C (g b) (h b)) ( λ u → ( inv (ap g (pr2 u))) ∙ - ( ( htpy-eq p (pr1 u)) ∙ + ( ( htpy-eq p (pr1 u)) ∙ ( ap h (pr2 u)))))) ``` diff --git a/src/foundation/equality-cartesian-product-types.lagda.md b/src/foundation/equality-cartesian-product-types.lagda.md index e0cfa21797..c720fde3cf 100644 --- a/src/foundation/equality-cartesian-product-types.lagda.md +++ b/src/foundation/equality-cartesian-product-types.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.equality-cartesian-product-types where +``` + +
Imports +```agda open import foundation-core.equality-cartesian-product-types public ``` + +
diff --git a/src/foundation/equality-fibers-of-maps.lagda.md b/src/foundation/equality-fibers-of-maps.lagda.md index 27dd62750f..71e103ab12 100644 --- a/src/foundation/equality-fibers-of-maps.lagda.md +++ b/src/foundation/equality-fibers-of-maps.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.equality-fibers-of-maps where +``` + +
Imports +```agda open import foundation-core.equality-fibers-of-maps public ``` + +
diff --git a/src/foundation/faithful-maps.lagda.md b/src/foundation/faithful-maps.lagda.md index d5d917782a..a2c31b4e16 100644 --- a/src/foundation/faithful-maps.lagda.md +++ b/src/foundation/faithful-maps.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.faithful-maps where +``` + +
Imports +```agda open import foundation-core.faithful-maps public ``` + +
diff --git a/src/foundation/functions.lagda.md b/src/foundation/functions.lagda.md index d44b65a1c6..2d4c03d026 100644 --- a/src/foundation/functions.lagda.md +++ b/src/foundation/functions.lagda.md @@ -2,8 +2,13 @@ ```agda {-# OPTIONS --safe #-} - module foundation.functions where +``` + +
Imports +```agda open import foundation-core.functions public ``` + +
diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md index a1b796b1b1..093a1cfcda 100644 --- a/src/foundation/functoriality-fibers-of-maps.lagda.md +++ b/src/foundation/functoriality-fibers-of-maps.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.functoriality-fibers-of-maps where +``` + +
Imports +```agda open import foundation-core.functoriality-fibers-of-maps public ``` + +
diff --git a/src/foundation/fundamental-theorem-of-identity-types.lagda.md b/src/foundation/fundamental-theorem-of-identity-types.lagda.md index b6df99b793..86bf017bb5 100644 --- a/src/foundation/fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/fundamental-theorem-of-identity-types.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.fundamental-theorem-of-identity-types where +``` + +
Imports +```agda open import foundation-core.fundamental-theorem-of-identity-types public ``` + +
diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md index 08fed50434..c5d8a938eb 100644 --- a/src/foundation/identity-systems.lagda.md +++ b/src/foundation/identity-systems.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.identity-systems where +``` + +
Imports +```agda open import foundation-core.identity-systems public ``` + +
diff --git a/src/foundation/images-subtypes.lagda.md b/src/foundation/images-subtypes.lagda.md index 111d6a3a37..fece81644c 100644 --- a/src/foundation/images-subtypes.lagda.md +++ b/src/foundation/images-subtypes.lagda.md @@ -7,18 +7,11 @@ module foundation.images-subtypes where
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.fibers-of-maps -open import foundation.functions -open import foundation.homotopies -open import foundation.identity-types open import foundation.images -open import foundation.propositional-truncations -open import foundation.propositions -open import foundation.subtypes -open import foundation.univalence -open import foundation.universe-levels + +open import foundation-core.functions +open import foundation-core.subtypes +open import foundation-core.universe-levels ```
diff --git a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md index 56118c0a50..1ac7dfec34 100644 --- a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md +++ b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md @@ -7,7 +7,6 @@ module foundation.lesser-limited-principle-of-omniscience where
Imports ```agda -open import elementary-number-theory.divisibility-natural-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.parity-natural-numbers diff --git a/src/foundation/morphisms-cospans.lagda.md b/src/foundation/morphisms-cospans.lagda.md index b399f8d107..f996254ddd 100644 --- a/src/foundation/morphisms-cospans.lagda.md +++ b/src/foundation/morphisms-cospans.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.morphisms-cospans where +``` + +
Imports +```agda open import foundation-core.morphisms-cospans public ``` + +
diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md index baca0d4692..a7c3481d04 100644 --- a/src/foundation/path-algebra.lagda.md +++ b/src/foundation/path-algebra.lagda.md @@ -239,14 +239,14 @@ module _ nat-sq-right-inv-Id² = (((horizontal-concat-Id² refl (inv (ap-const refl α))) ∙ nat-htpy right-inv α) ∙ (horizontal-concat-Id² (ap-binary-comp-diagonal (_∙_) id inv α) refl)) ∙ - ap (λ t → (horizontal-concat-Id² t (horizontal-inv-Id² α)) ∙ right-inv p') (ap-id α) + ap (λ t → (horizontal-concat-Id² t (horizontal-inv-Id² α)) ∙ right-inv p') (ap-id α) nat-sq-left-inv-Id² : coherence-square-identifications (left-inv p) refl (horizontal-concat-Id² (horizontal-inv-Id² α) α) (left-inv p') nat-sq-left-inv-Id² = ((((horizontal-concat-Id² refl (inv (ap-const refl α))) ∙ nat-htpy left-inv α) ∙ (horizontal-concat-Id² (ap-binary-comp-diagonal (_∙_) inv id α) refl)) ∙ - ap (λ t → (horizontal-concat-Id² (horizontal-inv-Id² α) t) ∙ left-inv p') (ap-id α)) + ap (λ t → (horizontal-concat-Id² (horizontal-inv-Id² α) t) ∙ left-inv p') (ap-id α)) ``` ### Interchange laws for 2-paths @@ -549,7 +549,7 @@ module _ ( ( ap (concat' x000 p110̂) p0̂0̂0) ∙ ( assoc p0̂00 p10̂0 p110̂)))))) ( ( assoc p000̂ p00̂1 p0̂11) ∙ - ( ( ap (concat p000̂ x111) p0̂0̂1) ∙ + ( ( ap (concat p000̂ x111) p0̂0̂1) ∙ ( ( inv (assoc p000̂ p0̂01 p10̂1)) ∙ ( ( ap (concat' x000 p10̂1) p0̂00̂) ∙ ( ( assoc p0̂00 p100̂ p10̂1) ∙ diff --git a/src/foundation/perfect-images.lagda.md b/src/foundation/perfect-images.lagda.md index 9cecdcd6c3..dfbcab580d 100644 --- a/src/foundation/perfect-images.lagda.md +++ b/src/foundation/perfect-images.lagda.md @@ -1,4 +1,4 @@ -# Perfect Images +# Perfect images ```agda module foundation.perfect-images where @@ -48,7 +48,7 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) where - is-perfect-image : (a : A) → UU (l1 ⊔ l2) + is-perfect-image : (a : A) → UU (l1 ⊔ l2) is-perfect-image a = (a₀ : A) (n : ℕ) → (iterate n (g ∘ f)) a₀ ＝ a → fib g a₀ ``` @@ -178,7 +178,7 @@ module _ is-not-perfect-image : (a : A) → UU (l1 ⊔ l2) is-not-perfect-image a = - Σ A (λ a₀ → (Σ ℕ (λ n → ((iterate n (g ∘ f)) a₀ ＝ a) × ¬ (fib g a₀)))) + Σ A (λ a₀ → (Σ ℕ (λ n → ((iterate n (g ∘ f)) a₀ ＝ a) × ¬ (fib g a₀)))) ``` If we assume law of excluded middle and `g` is embedding, we can prove that if @@ -234,7 +234,7 @@ module _ q = is-injective-is-emb is-emb-g (pr1 u) a : fib f b - a = pair ((iterate n (g ∘ f)) x₀) q + a = pair ((iterate n (g ∘ f)) x₀) q w : ¬ (is-perfect-image f g ((iterate n (g ∘ f)) x₀)) w = λ s → pr2 u (s x₀ n refl) diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index cf2f27a032..d76fadafcc 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -311,10 +311,12 @@ module _ {c = triple p q H} {triple p' q' H'} (triple Hp Hq HH)) ( is-equiv-map-equiv-canonical-pullback-htpy Hf Hg) ( is-pb-c) +``` -{- In the following part we will relate the type htpy-parallel-cone to the Identity - type of cones. Here we will rely on function extensionality. -} +In the following part we will relate the type htpy-parallel-cone to the identity +type of cones. Here we will rely on function extensionality. +```agda refl-htpy-parallel-cone : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) (c : cone f g C) → @@ -999,9 +1001,9 @@ cone-ap : ( λ (α : Id (p c1) (p c2)) → (ap f α) ∙ (H c2)) ( λ (β : Id (q c1) (q c2)) → (H c1) ∙ (ap g β)) ( Id c1 c2) -pr1 (cone-ap f g (pair p (pair q H)) c1 c2) = ap p -pr1 (pr2 (cone-ap f g (pair p (pair q H)) c1 c2)) = ap q -pr2 (pr2 (cone-ap f g (pair p (pair q H)) c1 c2)) γ = +pr1 (cone-ap f g (pair p (pair q H)) c1 c2) = ap p +pr1 (pr2 (cone-ap f g (pair p (pair q H)) c1 c2)) = ap q +pr2 (pr2 (cone-ap f g (pair p (pair q H)) c1 c2)) γ = ( ap (λ t → t ∙ (H c2)) (inv (ap-comp f p γ))) ∙ ( ( inv-nat-htpy H γ) ∙ ( ap (λ t → (H c1) ∙ t) (ap-comp g q γ))) @@ -1017,9 +1019,9 @@ cone-ap' : ( λ (α : Id (p c1) (p c2)) → tr (λ t → Id (f (p c1)) t) (H c2) (ap f α)) ( λ (β : Id (q c1) (q c2)) → (H c1) ∙ (ap g β)) ( Id c1 c2) -pr1 (cone-ap' f g (pair p (pair q H)) c1 c2) = ap p -pr1 (pr2 (cone-ap' f g (pair p (pair q H)) c1 c2)) = ap q -pr2 (pr2 (cone-ap' f g (pair p (pair q H)) c1 c2)) γ = +pr1 (cone-ap' f g (pair p (pair q H)) c1 c2) = ap p +pr1 (pr2 (cone-ap' f g (pair p (pair q H)) c1 c2)) = ap q +pr2 (pr2 (cone-ap' f g (pair p (pair q H)) c1 c2)) γ = ( tr-Id-right (H c2) (ap f (ap p γ))) ∙ ( ( ap (λ t → t ∙ (H c2)) (inv (ap-comp f p γ))) ∙ ( ( inv-nat-htpy H γ) ∙ diff --git a/src/foundation/relaxed-sigma-decompositions.lagda.md b/src/foundation/relaxed-sigma-decompositions.lagda.md index 3a8a627c7b..affbe2ae87 100644 --- a/src/foundation/relaxed-sigma-decompositions.lagda.md +++ b/src/foundation/relaxed-sigma-decompositions.lagda.md @@ -8,32 +8,22 @@ module foundation.relaxed-sigma-decompositions where
Imports ```agda -open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.empty-types -open import foundation.equality-dependent-function-types -open import foundation.equality-dependent-pair-types open import foundation.equational-reasoning open import foundation.equivalence-extensionality open import foundation.equivalences -open import foundation.function-extensionality -open import foundation.functions -open import foundation.functoriality-dependent-pair-types -open import foundation.functoriality-propositional-truncation -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopies -open import foundation.identity-types -open import foundation.inhabited-types -open import foundation.propositional-truncations -open import foundation.sets open import foundation.structure-identity-principle -open import foundation.transport -open import foundation.type-arithmetic-dependent-pair-types -open import foundation.type-arithmetic-empty-type open import foundation.type-theoretic-principle-of-choice -open import foundation.unit-type open import foundation.univalence -open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.dependent-pair-types +open import foundation-core.functions +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.fundamental-theorem-of-identity-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.type-arithmetic-dependent-pair-types +open import foundation-core.universe-levels ```
diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md index 0d55b66a5c..4eeb0a2c0f 100644 --- a/src/foundation/set-truncations.lagda.md +++ b/src/foundation/set-truncations.lagda.md @@ -261,9 +261,11 @@ abstract ( trunc-Set A) ( unit-trunc-Set) ( is-surjective-and-effective-unit-trunc-Set A) +``` --- Uniqueness of trunc-Set +### Uniqueness of trunc-Set +```agda module _ {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) {h : type-hom-Set B (trunc-Set A)} (H : (h ∘ f) ~ unit-trunc-Set) @@ -469,9 +471,11 @@ module _ ( map-coprod unit-trunc-Set unit-trunc-Set) triangle-distributive-trunc-coprod-Set = pr2 (center distributive-trunc-coprod-Set) +``` --- Set truncations of Σ-types +### Set truncations of Σ-types +```agda module _ {l1 l2 : Level} (A : UU l1) (B : A → UU l2) where @@ -509,9 +513,11 @@ module _ type-trunc-Set (Σ A B) → type-trunc-Set (Σ A (λ x → type-trunc-Set (B x))) map-equiv-trunc-Σ-Set = map-equiv equiv-trunc-Σ-Set +``` --- trunc-Set distributes over products +### `trunc-Set` distributes over products +```agda module _ {l1 l2 : Level} (A : UU l1) (B : UU l2) where diff --git a/src/foundation/sets.lagda.md b/src/foundation/sets.lagda.md index f6b3f991a8..f7f173bdc0 100644 --- a/src/foundation/sets.lagda.md +++ b/src/foundation/sets.lagda.md @@ -33,7 +33,7 @@ open import foundation-core.universe-levels ### The type of all sets in a universe is a 1-type ```agda -is-1-type-Set : {l : Level} → is-1-type (Set l) +is-1-type-Set : {l : Level} → is-1-type (Set l) is-1-type-Set = is-trunc-Truncated-Type zero-𝕋 Set-1-Type : (l : Level) → 1-Type (lsuc l) diff --git a/src/foundation/sigma-decomposition-subuniverse.lagda.md b/src/foundation/sigma-decomposition-subuniverse.lagda.md index 82dd01231e..cca90d0761 100644 --- a/src/foundation/sigma-decomposition-subuniverse.lagda.md +++ b/src/foundation/sigma-decomposition-subuniverse.lagda.md @@ -7,14 +7,15 @@ module foundation.sigma-decomposition-subuniverse where
Imports ```agda -open import foundation.cartesian-product-types -open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.homotopies -open import foundation.propositions open import foundation.relaxed-sigma-decompositions open import foundation.subuniverses -open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.dependent-pair-types +open import foundation-core.equivalences +open import foundation-core.homotopies +open import foundation-core.propositions +open import foundation-core.universe-levels ```
diff --git a/src/foundation/sigma-decompositions.lagda.md b/src/foundation/sigma-decompositions.lagda.md index a17ad5bf32..01b9204f07 100644 --- a/src/foundation/sigma-decompositions.lagda.md +++ b/src/foundation/sigma-decompositions.lagda.md @@ -8,32 +8,24 @@ module foundation.sigma-decompositions where
Imports ```agda -open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.empty-types -open import foundation.equality-dependent-function-types -open import foundation.equality-dependent-pair-types open import foundation.equational-reasoning open import foundation.equivalence-extensionality open import foundation.equivalences -open import foundation.function-extensionality -open import foundation.functions -open import foundation.functoriality-dependent-pair-types -open import foundation.functoriality-propositional-truncation -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopies -open import foundation.identity-types open import foundation.inhabited-types open import foundation.propositional-truncations open import foundation.sets open import foundation.structure-identity-principle -open import foundation.transport -open import foundation.type-arithmetic-dependent-pair-types -open import foundation.type-arithmetic-empty-type open import foundation.type-theoretic-principle-of-choice -open import foundation.unit-type open import foundation.univalence +open import foundation-core.contractible-types +open import foundation-core.dependent-pair-types +open import foundation-core.functions +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.fundamental-theorem-of-identity-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.type-arithmetic-dependent-pair-types open import foundation-core.universe-levels ``` @@ -620,7 +612,7 @@ module _ snd-equiv-fibered-Σ-Decomposition = pr2 module _ - { l1 l2 l3 l4 l5 : Level} {A : UU l1} + { l1 l2 l3 l4 l5 : Level} {A : UU l1} ( D : fibered-Σ-Decomposition l2 l3 l4 l5 A) where @@ -651,7 +643,7 @@ module _ ( pair (indexing-type-Σ-Decomposition Y) id-equiv ) ( is-contr-total-Eq-structure ( λ V f g → - ( ( map-equiv-Σ (λ u → type-Inhabited-Type (V u)) id-equiv g) ∘ + ( ( map-equiv-Σ (λ u → type-Inhabited-Type (V u)) id-equiv g) ∘ ( map-matching-correspondence-Σ-Decomposition Y)) ~ ( pr1 f)) ( is-contr-total-equiv-Fam-Inhabited-Types @@ -753,7 +745,7 @@ module _ snd-equiv-displayed-Σ-Decomposition = pr2 module _ - { l1 l2 l3 l4 l5 : Level} {A : UU l1} + { l1 l2 l3 l4 l5 : Level} {A : UU l1} ( disp-D : displayed-Σ-Decomposition l2 l3 l4 l5 A) where @@ -947,7 +939,7 @@ module _ ( map-inv-displayed-fibered-Σ-Decomposition ( map-displayed-fibered-Σ-Decomposition fib-D)) ( fib-D) - ( ( ( inv-equiv f) , + ( ( ( inv-equiv f) , ( ( λ x → id-equiv) , ( htpy-matching-correspondence))) , ( ( id-equiv) , @@ -979,7 +971,7 @@ module _ htpy-matching-correspondence : map-equiv ( - ( equiv-Σ N id-equiv (inv-equiv ∘ t) ) ∘e + ( equiv-Σ N id-equiv (inv-equiv ∘ t)) ∘e matching-correspondence-displayed-fibered-Σ-Decomposition (fib-D)) ~ map-equiv s diff --git a/src/foundation/strongly-extensional-maps.lagda.md b/src/foundation/strongly-extensional-maps.lagda.md index 9776ea7a7d..113662ac4f 100644 --- a/src/foundation/strongly-extensional-maps.lagda.md +++ b/src/foundation/strongly-extensional-maps.lagda.md @@ -37,5 +37,11 @@ strongly-extensional A B f = ## Properties --- -`agda -- is-strongly-extensional : -- {l1 l2 l3 l4 : Level} (A : Type-With-Apartness l1 l2) -- (B : Type-With-Apartness l3 l4) → -- (f : type-Type-With-Apartness A → type-Type-With-Apartness B) → -- strongly-extensional A B f -- is-strongly-extensional A B f x y H = {!!} -- ` +```agda +-- is-strongly-extensional : +-- {l1 l2 l3 l4 : Level} (A : Type-With-Apartness l1 l2) +-- (B : Type-With-Apartness l3 l4) → +-- (f : type-Type-With-Apartness A → type-Type-With-Apartness B) → +-- strongly-extensional A B f +-- is-strongly-extensional A B f x y H = {!!} +``` diff --git a/src/foundation/subtype-identity-principle.lagda.md b/src/foundation/subtype-identity-principle.lagda.md index 5dd6cd8ec6..4ebb572ffb 100644 --- a/src/foundation/subtype-identity-principle.lagda.md +++ b/src/foundation/subtype-identity-principle.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.subtype-identity-principle where +``` + +
Imports +```agda open import foundation-core.subtype-identity-principle public ``` + +
diff --git a/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md b/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md index b48c8f9747..86ff491bd4 100644 --- a/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md +++ b/src/foundation/trivial-relaxed-sigma-decompositions.lagda.md @@ -8,20 +8,18 @@ module foundation.trivial-relaxed-sigma-decompositions where ```agda open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.empty-types -open import foundation.equality-dependent-pair-types open import foundation.equivalences -open import foundation.functions -open import foundation.functoriality-propositional-truncation -open import foundation.identity-types -open import foundation.propositions open import foundation.relaxed-sigma-decompositions -open import foundation.subtypes -open import foundation.type-arithmetic-dependent-pair-types -open import foundation.type-arithmetic-empty-type open import foundation.unit-type -open import foundation.universe-levels + +open import foundation-core.dependent-pair-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.functions +open import foundation-core.identity-types +open import foundation-core.propositions +open import foundation-core.subtypes +open import foundation-core.type-arithmetic-dependent-pair-types +open import foundation-core.universe-levels ```
diff --git a/src/foundation/trivial-sigma-decompositions.lagda.md b/src/foundation/trivial-sigma-decompositions.lagda.md index 1e63185737..073b698031 100644 --- a/src/foundation/trivial-sigma-decompositions.lagda.md +++ b/src/foundation/trivial-sigma-decompositions.lagda.md @@ -8,21 +8,22 @@ module foundation.trivial-sigma-decompositions where ```agda open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.empty-types -open import foundation.equality-dependent-pair-types open import foundation.equivalences -open import foundation.functions open import foundation.functoriality-propositional-truncation -open import foundation.identity-types open import foundation.inhabited-types -open import foundation.propositions open import foundation.sigma-decompositions -open import foundation.subtypes -open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-empty-type open import foundation.unit-type -open import foundation.universe-levels + +open import foundation-core.dependent-pair-types +open import foundation-core.empty-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.functions +open import foundation-core.identity-types +open import foundation-core.propositions +open import foundation-core.subtypes +open import foundation-core.type-arithmetic-dependent-pair-types +open import foundation-core.universe-levels ```
diff --git a/src/foundation/tuples-of-types.lagda.md b/src/foundation/tuples-of-types.lagda.md index b73a80115a..ce839496b6 100644 --- a/src/foundation/tuples-of-types.lagda.md +++ b/src/foundation/tuples-of-types.lagda.md @@ -39,5 +39,3 @@ tuple-types-complement-point : tuple-types-complement-point A i = {!!} -} ``` - --- Σ (x : Fin (n + 1)) (a ≠ x) ≃ -- Fin n diff --git a/src/foundation/type-arithmetic-cartesian-product-types.lagda.md b/src/foundation/type-arithmetic-cartesian-product-types.lagda.md index 8d0d3a992e..962a931597 100644 --- a/src/foundation/type-arithmetic-cartesian-product-types.lagda.md +++ b/src/foundation/type-arithmetic-cartesian-product-types.lagda.md @@ -2,6 +2,12 @@ ```agda module foundation.type-arithmetic-cartesian-product-types where +``` + +
Imports +```agda open import foundation-core.type-arithmetic-cartesian-product-types public ``` + +
diff --git a/src/foundation/type-arithmetic-dependent-function-types.lagda.md b/src/foundation/type-arithmetic-dependent-function-types.lagda.md index 3d8a8c0743..4b49449172 100644 --- a/src/foundation/type-arithmetic-dependent-function-types.lagda.md +++ b/src/foundation/type-arithmetic-dependent-function-types.lagda.md @@ -7,16 +7,17 @@ module foundation.type-arithmetic-dependent-function-types where
Imports ```agda -open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.equivalences open import foundation.functoriality-dependent-function-types -open import foundation.homotopies -open import foundation.identity-types open import foundation.type-arithmetic-unit-type open import foundation.unit-type -open import foundation.univalence -open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.dependent-pair-types +open import foundation-core.equivalences +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.univalence +open import foundation-core.universe-levels ```
diff --git a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md index 82053c1df6..9772777835 100644 --- a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md +++ b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md @@ -2,10 +2,16 @@ ```agda module foundation.type-arithmetic-dependent-pair-types where +``` + +
Imports +```agda open import foundation-core.type-arithmetic-dependent-pair-types public ``` +
+ ## Idea We prove laws for the manipulation of dependent pair types with respect to diff --git a/src/foundation/type-duality.lagda.md b/src/foundation/type-duality.lagda.md index aee42b13e7..0d815f59c5 100644 --- a/src/foundation/type-duality.lagda.md +++ b/src/foundation/type-duality.lagda.md @@ -7,41 +7,35 @@ module foundation.type-duality where
Imports ```agda -open import foundation.cartesian-product-types -open import foundation.contractible-maps -open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.embeddings -open import foundation.equality-cartesian-product-types -open import foundation.equality-dependent-pair-types open import foundation.equational-reasoning -open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.function-extensionality -open import foundation.functions -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopies -open import foundation.identity-types open import foundation.inhabited-types open import foundation.locally-small-types open import foundation.polynomial-endofunctors open import foundation.propositional-maps -open import foundation.propositional-truncations -open import foundation.propositions open import foundation.slice open import foundation.structure open import foundation.surjective-maps -open import foundation.transport -open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice open import foundation.unit-type open import foundation.univalence +open import foundation-core.contractible-maps +open import foundation-core.contractible-types +open import foundation-core.dependent-pair-types +open import foundation-core.embeddings open import foundation-core.fibers-of-maps +open import foundation-core.functions +open import foundation-core.functoriality-dependent-function-types +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.fundamental-theorem-of-identity-types +open import foundation-core.homotopies +open import foundation-core.identity-types open import foundation-core.injective-maps +open import foundation-core.propositions open import foundation-core.small-types +open import foundation-core.type-arithmetic-dependent-pair-types open import foundation-core.universe-levels ``` diff --git a/src/foundation/uniqueness-set-quotients.lagda.md b/src/foundation/uniqueness-set-quotients.lagda.md index 930f579637..f5cfeb21ef 100644 --- a/src/foundation/uniqueness-set-quotients.lagda.md +++ b/src/foundation/uniqueness-set-quotients.lagda.md @@ -191,7 +191,7 @@ module _ pr1 (center uniqueness-set-quotient) map-equiv-uniqueness-set-quotient : type-Set B → type-Set C - map-equiv-uniqueness-set-quotient = map-equiv equiv-uniqueness-set-quotient + map-equiv-uniqueness-set-quotient = map-equiv equiv-uniqueness-set-quotient triangle-uniqueness-set-quotient : ( map-equiv-uniqueness-set-quotient ∘ map-reflecting-map-Eq-Rel R f) ~ diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md index 9a59f52ee8..b070602f96 100644 --- a/src/foundation/universal-property-cartesian-product-types.lagda.md +++ b/src/foundation/universal-property-cartesian-product-types.lagda.md @@ -39,16 +39,20 @@ product module _ {l1 l2 : Level} (A : UU l1) (B : UU l2) where +``` - {- We construct the cone for two maps into the unit type. -} +We construct the cone for two maps into the unit type. +```agda cone-prod : cone (const A unit star) (const B unit star) (A × B) pr1 cone-prod = pr1 pr1 (pr2 cone-prod) = pr2 pr2 (pr2 cone-prod) = refl-htpy +``` - {- Cartesian products are a special case of pullbacks. -} +Cartesian products are a special case of pullbacks. +```agda gap-prod : A × B → canonical-pullback (const A unit star) (const B unit star) gap-prod = gap (const A unit star) (const B unit star) cone-prod @@ -79,10 +83,11 @@ module _ inv-gap-prod issec-inv-gap-prod isretr-inv-gap-prod +``` - {- We conclude that cartesian products satisfy the universal property of - pullbacks. -} +We conclude that cartesian products satisfy the universal property of pullbacks. +```agda abstract universal-property-pullback-prod : {l : Level} → diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md index 4ab64a7f8f..925c7387f8 100644 --- a/src/foundation/universal-property-fiber-products.lagda.md +++ b/src/foundation/universal-property-fiber-products.lagda.md @@ -42,11 +42,13 @@ module _ pr1 cone-fiberwise-prod = tot (λ x → pr1) pr1 (pr2 cone-fiberwise-prod) = tot (λ x → pr2) pr2 (pr2 cone-fiberwise-prod) = refl-htpy +``` - {- We will show that the fiberwise product is a pullback by showing that the - gap map is an equivalence. We do this by directly construct an inverse to - the gap map. -} +We will show that the fiberwise product is a pullback by showing that the gap +map is an equivalence. We do this by directly construct an inverse to the gap +map. +```agda gap-fiberwise-prod : Σ X (λ x → (P x) × (Q x)) → canonical-pullback (pr1 {B = P}) (pr1 {B = Q}) gap-fiberwise-prod = gap pr1 pr1 cone-fiberwise-prod diff --git a/src/foundation/universal-property-maybe.lagda.md b/src/foundation/universal-property-maybe.lagda.md index a3cbc0e522..b9c1f6c810 100644 --- a/src/foundation/universal-property-maybe.lagda.md +++ b/src/foundation/universal-property-maybe.lagda.md @@ -28,9 +28,9 @@ open import foundation-core.universe-levels We combine the universal property of coproducts and the unit type to obtain a universal property of the maybe modality. -```agda --- The universal property of Maybe +## Definitions +```agda module _ {l1 l2 : Level} {A : UU l1} {B : Maybe A → UU l2} where diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index dcf802b988..7b3fbcdb6f 100644 --- a/src/foundation/universal-property-propositional-truncation.lagda.md +++ b/src/foundation/universal-property-propositional-truncation.lagda.md @@ -62,7 +62,7 @@ universal-property-propositional-truncation : (P : Prop l2) (f : A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2) universal-property-propositional-truncation l {A = A} P f = (Q : Prop l) (g : A → type-Prop Q) → - is-contr (Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~ g)) + is-contr (Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~ g)) ``` ### Extension property of the propositional truncation @@ -207,7 +207,7 @@ abstract ( is-property-is-equiv) ( map-is-propositional-truncation P f is-ptr-f P' f') ( htpy-is-propositional-truncation P f is-ptr-f P' f') - ( is-equiv-is-ptruncation-is-ptruncation P P' f f' + ( is-equiv-is-ptruncation-is-ptruncation P P' f f' ( map-is-propositional-truncation P f is-ptr-f P' f') ( htpy-is-propositional-truncation P f is-ptr-f P' f') ( λ {l} → is-ptr-f) diff --git a/src/foundation/universal-property-set-truncation.lagda.md b/src/foundation/universal-property-set-truncation.lagda.md index 8e371ea0a9..ca715ea065 100644 --- a/src/foundation/universal-property-set-truncation.lagda.md +++ b/src/foundation/universal-property-set-truncation.lagda.md @@ -55,7 +55,7 @@ universal-property-set-truncation : (B : Set l2) (f : A → type-Set B) → UU (lsuc l ⊔ l1 ⊔ l2) universal-property-set-truncation l {A = A} B f = (C : Set l) (g : A → type-Set C) → - is-contr (Σ (type-hom-Set B C) (λ h → (h ∘ f) ~ g)) + is-contr (Σ (type-hom-Set B C) (λ h → (h ∘ f) ~ g)) ``` ### The dependent universal property of set truncations diff --git a/src/foundation/universal-property-unit-type.lagda.md b/src/foundation/universal-property-unit-type.lagda.md index 904a924cfc..4cff3d2a65 100644 --- a/src/foundation/universal-property-unit-type.lagda.md +++ b/src/foundation/universal-property-unit-type.lagda.md @@ -32,8 +32,6 @@ properties of contractible types. ## Properties ```agda --- We conclude that the properties in the exercise hold for the unit type - ev-star : {l : Level} (P : unit → UU l) → ((x : unit) → P x) → P star ev-star P f = f star diff --git a/src/foundation/universe-levels.lagda.md b/src/foundation/universe-levels.lagda.md index 72a4ea794f..fc554a0598 100644 --- a/src/foundation/universe-levels.lagda.md +++ b/src/foundation/universe-levels.lagda.md @@ -2,8 +2,13 @@ ```agda {-# OPTIONS --safe --no-import-sorts #-} - module foundation.universe-levels where +``` + +
Imports +```agda open import foundation-core.universe-levels public ``` + +
diff --git a/src/graph-theory/directed-graphs.lagda.md b/src/graph-theory/directed-graphs.lagda.md index f22b2228d9..1d7475275f 100644 --- a/src/graph-theory/directed-graphs.lagda.md +++ b/src/graph-theory/directed-graphs.lagda.md @@ -1,4 +1,4 @@ -# Graphs +# Directed graphs ```agda module graph-theory.directed-graphs where @@ -18,8 +18,8 @@ open import foundation.universe-levels ## Idea -A graph consists of a type of vertices equipped with a binary, type valued -relation of edges. +A directed graph consists of a type of vertices equipped with a binary, type +valued relation of edges. ## Definition @@ -63,8 +63,8 @@ module _ ```agda module alternative where - Directed-Graph' : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) - Directed-Graph' l1 l2 = Σ (UU l1) λ V → Σ (UU l2) (λ E → (E → V) × (E → V)) + Directed-Graph' : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) + Directed-Graph' l1 l2 = Σ (UU l1) λ V → Σ (UU l2) (λ E → (E → V) × (E → V)) module _ {l1 l2 : Level} (G : Directed-Graph' l1 l2) where @@ -90,7 +90,7 @@ module equiv {l1 l2 : Level} where pr1 (Directed-Graph-to-Directed-Graph' G) = vertex-Directed-Graph G pr1 (pr2 (Directed-Graph-to-Directed-Graph' G)) = Σ ( vertex-Directed-Graph G) - ( λ x → Σ (vertex-Directed-Graph G) λ y → edge-Directed-Graph G x y) + ( λ x → Σ (vertex-Directed-Graph G) λ y → edge-Directed-Graph G x y) pr1 (pr2 (pr2 (Directed-Graph-to-Directed-Graph' G))) = pr1 pr2 (pr2 (pr2 (Directed-Graph-to-Directed-Graph' G))) = pr1 ∘ pr2 diff --git a/src/graph-theory/regular-undirected-graphs.lagda.md b/src/graph-theory/regular-undirected-graphs.lagda.md index a1fdfa993e..0d2f93eb6d 100644 --- a/src/graph-theory/regular-undirected-graphs.lagda.md +++ b/src/graph-theory/regular-undirected-graphs.lagda.md @@ -2,7 +2,11 @@ ```agda module graph-theory.regular-undirected-graphs where +``` + +
Imports +```agda open import foundation.mere-equivalences open import foundation.propositions open import foundation.universe-levels @@ -11,6 +15,8 @@ open import graph-theory.neighbors-undirected-graphs open import graph-theory.undirected-graphs ``` +
+ ## Idea A regular undirected graph is a graph of which each vertex has the same number diff --git a/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md b/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md index 0ff64f8043..08cba53352 100644 --- a/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md +++ b/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md @@ -31,7 +31,7 @@ Note: It could be that we only want the shapes to be merely preserved. ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) + {l1 l2 l3 l4 l5 l6 : Level} (A : UU l1) (B : A → UU l2) (G : Enriched-Undirected-Graph l3 l4 A B) (H : Enriched-Undirected-Graph l5 l6 A B) where diff --git a/src/group-theory/category-of-concrete-groups.lagda.md b/src/group-theory/category-of-concrete-groups.lagda.md index 9798a40cfd..46a7dc1db5 100644 --- a/src/group-theory/category-of-concrete-groups.lagda.md +++ b/src/group-theory/category-of-concrete-groups.lagda.md @@ -16,5 +16,8 @@ module group-theory.category-of-concrete-groups where ### The category of concrete groups --- -`agda -- is-category-Concrete-Group-Large-Precat : -- is-category-Large-Precat Concrete-Group-Large-Precat -- is-category-Concrete-Group-Large-Precat = {!!} -- ` +```agda +-- is-category-Concrete-Group-Large-Precat : +-- is-category-Large-Precat Concrete-Group-Large-Precat +-- is-category-Concrete-Group-Large-Precat = {!!} +``` diff --git a/src/group-theory/central-elements-groups.lagda.md b/src/group-theory/central-elements-groups.lagda.md index b9751dd583..2cf04db784 100644 --- a/src/group-theory/central-elements-groups.lagda.md +++ b/src/group-theory/central-elements-groups.lagda.md @@ -9,7 +9,6 @@ module group-theory.central-elements-groups where ```agda open import foundation.identity-types open import foundation.propositions -open import foundation.sets open import foundation.subtypes open import foundation.universe-levels diff --git a/src/group-theory/central-elements-monoids.lagda.md b/src/group-theory/central-elements-monoids.lagda.md index 8fa7fc3582..741798c32d 100644 --- a/src/group-theory/central-elements-monoids.lagda.md +++ b/src/group-theory/central-elements-monoids.lagda.md @@ -9,7 +9,6 @@ module group-theory.central-elements-monoids where ```agda open import foundation.identity-types open import foundation.propositions -open import foundation.sets open import foundation.universe-levels open import group-theory.central-elements-semigroups diff --git a/src/group-theory/decidable-subgroups.lagda.md b/src/group-theory/decidable-subgroups.lagda.md index 15857ac6e9..84cc938ff7 100644 --- a/src/group-theory/decidable-subgroups.lagda.md +++ b/src/group-theory/decidable-subgroups.lagda.md @@ -210,7 +210,7 @@ module _ {l1 l2 : Level} (G : Group l1) (H : Decidable-Subgroup l2 G) where - type-group-Decidable-Subgroup : UU (l1 ⊔ l2) + type-group-Decidable-Subgroup : UU (l1 ⊔ l2) type-group-Decidable-Subgroup = type-group-Subgroup G (subgroup-Decidable-Subgroup G H) diff --git a/src/group-theory/dependent-products-commutative-monoids.lagda.md b/src/group-theory/dependent-products-commutative-monoids.lagda.md index 89346cef59..6d9fdd11e9 100644 --- a/src/group-theory/dependent-products-commutative-monoids.lagda.md +++ b/src/group-theory/dependent-products-commutative-monoids.lagda.md @@ -15,9 +15,7 @@ open import foundation.universe-levels open import group-theory.commutative-monoids open import group-theory.dependent-products-monoids -open import group-theory.dependent-products-semigroups open import group-theory.monoids -open import group-theory.semigroups ```
diff --git a/src/group-theory/function-abelian-groups.lagda.md b/src/group-theory/function-abelian-groups.lagda.md index c1e228ef14..6836e3eed4 100644 --- a/src/group-theory/function-abelian-groups.lagda.md +++ b/src/group-theory/function-abelian-groups.lagda.md @@ -7,8 +7,6 @@ module group-theory.function-abelian-groups where
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.identity-types open import foundation.sets open import foundation.universe-levels diff --git a/src/group-theory/function-commutative-monoids.lagda.md b/src/group-theory/function-commutative-monoids.lagda.md index 6655cc9ea3..cde7ec9930 100644 --- a/src/group-theory/function-commutative-monoids.lagda.md +++ b/src/group-theory/function-commutative-monoids.lagda.md @@ -7,17 +7,13 @@ module group-theory.function-commutative-monoids where
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.identity-types open import foundation.sets open import foundation.universe-levels open import group-theory.commutative-monoids open import group-theory.dependent-products-commutative-monoids -open import group-theory.dependent-products-semigroups open import group-theory.monoids -open import group-theory.semigroups ```
diff --git a/src/group-theory/function-groups.lagda.md b/src/group-theory/function-groups.lagda.md index c04798890e..c3dcabbead 100644 --- a/src/group-theory/function-groups.lagda.md +++ b/src/group-theory/function-groups.lagda.md @@ -8,13 +8,11 @@ module group-theory.function-groups where ```agda open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.identity-types open import foundation.sets open import foundation.universe-levels open import group-theory.dependent-products-groups -open import group-theory.function-semigroups open import group-theory.groups open import group-theory.monoids open import group-theory.semigroups diff --git a/src/group-theory/function-monoids.lagda.md b/src/group-theory/function-monoids.lagda.md index 04dac613fa..8f40b5f116 100644 --- a/src/group-theory/function-monoids.lagda.md +++ b/src/group-theory/function-monoids.lagda.md @@ -7,14 +7,11 @@ module group-theory.function-monoids where
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.identity-types open import foundation.sets open import foundation.universe-levels open import group-theory.dependent-products-monoids -open import group-theory.dependent-products-semigroups open import group-theory.monoids open import group-theory.semigroups ``` diff --git a/src/group-theory/function-semigroups.lagda.md b/src/group-theory/function-semigroups.lagda.md index 2ea2cc1388..06605fc58c 100644 --- a/src/group-theory/function-semigroups.lagda.md +++ b/src/group-theory/function-semigroups.lagda.md @@ -7,8 +7,6 @@ module group-theory.function-semigroups where
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.identity-types open import foundation.sets open import foundation.universe-levels diff --git a/src/group-theory/group-solver.lagda.md b/src/group-theory/group-solver.lagda.md index 9ac6aa546a..922ec27d31 100644 --- a/src/group-theory/group-solver.lagda.md +++ b/src/group-theory/group-solver.lagda.md @@ -53,7 +53,7 @@ data GroupSyntax (n : ℕ) : UU where gInv : GroupSyntax n → GroupSyntax n inner : Fin n → GroupSyntax n -data SimpleElem (n : ℕ) : UU where +data SimpleElem (n : ℕ) : UU where inv-SE : Fin n → SimpleElem n pure-SE : Fin n → SimpleElem n diff --git a/src/group-theory/homomorphisms-higher-groups.lagda.md b/src/group-theory/homomorphisms-higher-groups.lagda.md index 969417281d..809aee1e20 100644 --- a/src/group-theory/homomorphisms-higher-groups.lagda.md +++ b/src/group-theory/homomorphisms-higher-groups.lagda.md @@ -81,9 +81,13 @@ module _ preserves-inv-map-Ω ( classifying-pointed-type-∞-Group G) ( classifying-pointed-type-∞-Group H) +``` + +## Properties --- Homotopies of morphisms of ∞-groups +### Homotopies of morphisms of ∞-groups +```agda module _ {l1 l2 : Level} (G : ∞-Group l1) (H : ∞-Group l2) (f : hom-∞-Group G H) where @@ -107,9 +111,11 @@ module _ eq-htpy-hom-∞-Group : (g : hom-∞-Group G H) → (htpy-hom-∞-Group g) → Id f g eq-htpy-hom-∞-Group g = map-inv-equiv (extensionality-hom-∞-Group g) +``` --- Wild category structure on higher groups +### Wild category structure on higher groups +```agda module _ {l : Level} (G : ∞-Group l) where diff --git a/src/group-theory/homomorphisms-monoids.lagda.md b/src/group-theory/homomorphisms-monoids.lagda.md index 39e170ce34..41a987f6a6 100644 --- a/src/group-theory/homomorphisms-monoids.lagda.md +++ b/src/group-theory/homomorphisms-monoids.lagda.md @@ -57,7 +57,7 @@ module _ ( hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2)) ( preserves-unit-hom-semigroup-Prop) - type-hom-Monoid : UU (l1 ⊔ l2) + type-hom-Monoid : UU (l1 ⊔ l2) type-hom-Monoid = type-Set hom-Monoid module _ diff --git a/src/group-theory/homomorphisms-semigroups.lagda.md b/src/group-theory/homomorphisms-semigroups.lagda.md index 81841bc0e7..89753f3476 100644 --- a/src/group-theory/homomorphisms-semigroups.lagda.md +++ b/src/group-theory/homomorphisms-semigroups.lagda.md @@ -105,9 +105,11 @@ module _ preserves-mul-hom-Semigroup : (f : type-hom-Semigroup) → preserves-mul-Semigroup (map-hom-Semigroup f) preserves-mul-hom-Semigroup f = pr2 f +``` - {- We characterize the identity type of the semigroup homomorphisms. -} +### Characterizing the identity type of semigroup homomorphisms +```agda htpy-hom-Semigroup : (f g : type-hom-Semigroup) → UU (l1 ⊔ l2) htpy-hom-Semigroup f g = map-hom-Semigroup f ~ map-hom-Semigroup g diff --git a/src/group-theory/normal-subgroups.lagda.md b/src/group-theory/normal-subgroups.lagda.md index 107e065952..bda58d4b4f 100644 --- a/src/group-theory/normal-subgroups.lagda.md +++ b/src/group-theory/normal-subgroups.lagda.md @@ -82,7 +82,7 @@ is-normal-is-normal-Subgroup G H K x y = is-normal-is-normal-Subgroup' : {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) → is-normal-Subgroup' G H → is-normal-Subgroup G H -is-normal-is-normal-Subgroup' G H K x y = +is-normal-is-normal-Subgroup' G H K x y = tr ( is-in-Subgroup G H) ( inv (htpy-conjugation-Group' G x (inclusion-Subgroup G H y))) diff --git a/src/group-theory/normal-submonoids.lagda.md b/src/group-theory/normal-submonoids.lagda.md index 9d6489bb45..2d14f9ddae 100644 --- a/src/group-theory/normal-submonoids.lagda.md +++ b/src/group-theory/normal-submonoids.lagda.md @@ -23,6 +23,8 @@ open import group-theory.semigroups open import group-theory.submonoids ``` +
+ ## Idea A normal submonoid `N` of `M` is a monoid that corresponds uniquely to a diff --git a/src/group-theory/subgroups.lagda.md b/src/group-theory/subgroups.lagda.md index 6584d4a789..06cf4e3845 100644 --- a/src/group-theory/subgroups.lagda.md +++ b/src/group-theory/subgroups.lagda.md @@ -231,7 +231,7 @@ module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where - type-group-Subgroup : UU (l1 ⊔ l2) + type-group-Subgroup : UU (l1 ⊔ l2) type-group-Subgroup = type-subtype (subset-Subgroup G H) map-inclusion-Subgroup : type-group-Subgroup → type-Group G diff --git a/src/group-theory/torsors.lagda.md b/src/group-theory/torsors.lagda.md index 7d5ee63a0d..5b0e6e473f 100644 --- a/src/group-theory/torsors.lagda.md +++ b/src/group-theory/torsors.lagda.md @@ -2,7 +2,11 @@ ```agda module group-theory.torsors where +``` + +
Imports +```agda open import foundation.0-connected-types open import foundation.contractible-types open import foundation.dependent-pair-types @@ -18,9 +22,9 @@ open import foundation.sets open import foundation.subtype-identity-principle open import foundation.universe-levels -open import group-theory.group-actions open import group-theory.concrete-groups open import group-theory.equivalences-group-actions +open import group-theory.group-actions open import group-theory.groups open import group-theory.higher-groups open import group-theory.homomorphisms-groups @@ -28,7 +32,11 @@ open import group-theory.isomorphisms-groups open import group-theory.mere-equivalences-group-actions open import group-theory.principal-group-actions open import group-theory.symmetric-groups +``` +
+ +```agda module _ {l1 l2 : Level} (G : Group l1) (X : Abstract-Group-Action G l2) where diff --git a/src/linear-algebra/vectors.lagda.md b/src/linear-algebra/vectors.lagda.md index efca803495..ebd377a00e 100644 --- a/src/linear-algebra/vectors.lagda.md +++ b/src/linear-algebra/vectors.lagda.md @@ -161,7 +161,7 @@ module _ ( isretr-eq-Eq-vec n u v) extensionality-vec : (n : ℕ) → (u v : vec A n) → Id u v ≃ Eq-vec n u v - extensionality-vec n u v = (Eq-eq-vec n u v , is-equiv-Eq-eq-vec n u v) + extensionality-vec n u v = (Eq-eq-vec n u v , is-equiv-Eq-eq-vec n u v) ``` ### The types of listed vectors and functional vectors are equivalent diff --git a/src/order-theory/distributive-lattices.lagda.md b/src/order-theory/distributive-lattices.lagda.md index e650f64c69..7db86bd0f9 100644 --- a/src/order-theory/distributive-lattices.lagda.md +++ b/src/order-theory/distributive-lattices.lagda.md @@ -1,4 +1,4 @@ -# Distributive Lattices +# Distributive lattices ```agda module order-theory.distributive-lattices where diff --git a/src/order-theory/finite-posets.lagda.md b/src/order-theory/finite-posets.lagda.md index 6b45635171..060218d86b 100644 --- a/src/order-theory/finite-posets.lagda.md +++ b/src/order-theory/finite-posets.lagda.md @@ -19,7 +19,7 @@ open import univalent-combinatorics.finite-types
-## Finite Posets +## Definitions We say that a poset is finite if its underlying preorder is finite. diff --git a/src/order-theory/homomorphisms-frames.lagda.md b/src/order-theory/homomorphisms-frames.lagda.md index e2acb1b2c4..b881846de5 100644 --- a/src/order-theory/homomorphisms-frames.lagda.md +++ b/src/order-theory/homomorphisms-frames.lagda.md @@ -1,4 +1,4 @@ -# Homomorphisms Frames +# Homomorphisms of frames ```agda module order-theory.homomorphisms-frames where @@ -26,6 +26,8 @@ open import order-theory.order-preserving-maps-posets A frame homomorphism is an order preserving map between posets that additionally preserves binary meets and arbitrary joins. +## Definitions + ```agda module _ {l1 l2 l3 l4 l5 l6 : Level} (A : Frame l1 l2 l3) (B : Frame l4 l5 l6) diff --git a/src/order-theory/homomorphisms-meet-semilattices.lagda.md b/src/order-theory/homomorphisms-meet-semilattices.lagda.md index 89ab5e08ff..75645a352a 100644 --- a/src/order-theory/homomorphisms-meet-semilattices.lagda.md +++ b/src/order-theory/homomorphisms-meet-semilattices.lagda.md @@ -1,4 +1,4 @@ -# Homomorphisms Meet Semilattices +# Homomorphisms of meet semilattices ```agda module order-theory.homomorphisms-meet-semilattices where @@ -24,6 +24,8 @@ open import order-theory.order-preserving-maps-posets A meet semi-lattice homomorphism is an order preserving map between the underlying posets that also preserves meets. +## Definitions + ```agda module _ {l1 l2 l3 l4 : Level} (A : Meet-Semilattice l1 l2) (B : Meet-Semilattice l3 l4) diff --git a/src/order-theory/homomorphisms-meet-sup-lattices.lagda.md b/src/order-theory/homomorphisms-meet-sup-lattices.lagda.md index d2de5fb1de..48b6d24ca8 100644 --- a/src/order-theory/homomorphisms-meet-sup-lattices.lagda.md +++ b/src/order-theory/homomorphisms-meet-sup-lattices.lagda.md @@ -1,4 +1,4 @@ -# Homomorphisms Meet Sup Lattice +# Homomorphisms of meet sup lattices ```agda module order-theory.homomorphisms-meet-sup-lattices where @@ -28,6 +28,8 @@ neccesarily has binary meets but we have yet to give a proof of this fact in the library. Thus, we opt (for now) to treat the two structures as existing independently. +## Definitions + ```agda module _ {l1 l2 l3 l4 l5 l6 : Level} (A : Meet-Sup-Lattice l1 l2 l3) (B : Meet-Sup-Lattice l4 l5 l6) diff --git a/src/order-theory/homomorphisms-sup-lattices.lagda.md b/src/order-theory/homomorphisms-sup-lattices.lagda.md index b31bf63e86..7995ee7cec 100644 --- a/src/order-theory/homomorphisms-sup-lattices.lagda.md +++ b/src/order-theory/homomorphisms-sup-lattices.lagda.md @@ -1,4 +1,4 @@ -# Homomorphisms Sup Lattices +# Homomorphisms of sup lattices ```agda module order-theory.homomorphisms-sup-lattices where @@ -24,6 +24,8 @@ open import order-theory.sup-lattices A sup lattice homomorphism is a order preserving map between the underlying posets that additionally preserves sups (or arbitrary joins of subsets). +## Definitions + ```agda module _ {l1 l2 l3 l4 l5 l6 : Level} (A : Sup-Lattice l1 l2 l3) (B : Sup-Lattice l4 l5 l6) diff --git a/src/order-theory/large-posets.lagda.md b/src/order-theory/large-posets.lagda.md index 4f850574da..0277586e42 100644 --- a/src/order-theory/large-posets.lagda.md +++ b/src/order-theory/large-posets.lagda.md @@ -1,4 +1,4 @@ -# Large Posets +# Large posets ```agda module order-theory.large-posets where diff --git a/src/order-theory/largest-elements-preorders.lagda.md b/src/order-theory/largest-elements-preorders.lagda.md index e736597c3a..2161d0ea40 100644 --- a/src/order-theory/largest-elements-preorders.lagda.md +++ b/src/order-theory/largest-elements-preorders.lagda.md @@ -2,7 +2,11 @@ ```agda module order-theory.largest-elements-preorders where +``` + +
Imports +```agda open import foundation.dependent-pair-types open import foundation.propositions open import foundation.universe-levels @@ -10,6 +14,8 @@ open import foundation.universe-levels open import order-theory.preorders ``` +
+ ## Definition ```agda diff --git a/src/order-theory/posets.lagda.md b/src/order-theory/posets.lagda.md index c97aeae4fe..605ca4a67e 100644 --- a/src/order-theory/posets.lagda.md +++ b/src/order-theory/posets.lagda.md @@ -48,7 +48,7 @@ module _ leq-poset-Prop : (x y : element-Poset) → Prop l2 leq-poset-Prop = pr1 (pr2 X) - leq-Poset : (x y : element-Poset) → UU l2 + leq-Poset : (x y : element-Poset) → UU l2 leq-Poset x y = type-Prop (leq-poset-Prop x y) is-prop-leq-Poset : (x y : element-Poset) → is-prop (leq-Poset x y) diff --git a/src/order-theory/sup-lattices.lagda.md b/src/order-theory/sup-lattices.lagda.md index 67b5ee0a78..353eb0da06 100644 --- a/src/order-theory/sup-lattices.lagda.md +++ b/src/order-theory/sup-lattices.lagda.md @@ -1,4 +1,4 @@ -# Sup Lattices +# Sup lattices ```agda module order-theory.sup-lattices where @@ -65,7 +65,7 @@ module _ poset-Sup-Lattice : Poset l1 l2 poset-Sup-Lattice = pr1 A - element-Sup-Lattice : UU l1 {- could we use carrier instead of element? -} + element-Sup-Lattice : UU l1 element-Sup-Lattice = element-Poset poset-Sup-Lattice leq-sup-lattice-Prop : (x y : element-Sup-Lattice) → Prop l2 diff --git a/src/organic-chemistry/ethane.lagda.md b/src/organic-chemistry/ethane.lagda.md index ab6f3903b8..0513b7f88f 100644 --- a/src/organic-chemistry/ethane.lagda.md +++ b/src/organic-chemistry/ethane.lagda.md @@ -152,7 +152,7 @@ module _ is-contr-standard-edge-ethane : (c : vertex-ethane) → - is-contr (Σ (vertex-ethane) (λ c' → standard-edge-ethane c c')) + is-contr (Σ (vertex-ethane) (λ c' → standard-edge-ethane c c')) pr1 (pr1 (is-contr-standard-edge-ethane (inl (inr star)))) = one-Fin 1 pr1 (pr2 (pr1 (is-contr-standard-edge-ethane (inl (inr star))))) = unit-trunc-Prop (zero-Fin 1 , refl) diff --git a/src/organic-chemistry/hydrocarbons.lagda.md b/src/organic-chemistry/hydrocarbons.lagda.md index 6ffce46855..ec8fbcf5a5 100644 --- a/src/organic-chemistry/hydrocarbons.lagda.md +++ b/src/organic-chemistry/hydrocarbons.lagda.md @@ -93,7 +93,7 @@ module _ unordered-pair-vertices-hydrocarbon = unordered-pair vertex-hydrocarbon edge-hydrocarbon-𝔽 : unordered-pair-vertices-hydrocarbon → 𝔽 l2 - edge-hydrocarbon-𝔽 = pr2 finite-graph-hydrocarbon + edge-hydrocarbon-𝔽 = pr2 finite-graph-hydrocarbon edge-hydrocarbon : unordered-pair-vertices-hydrocarbon → UU l2 edge-hydrocarbon = edge-Undirected-Graph-𝔽 finite-graph-hydrocarbon diff --git a/src/ring-theory/central-elements-rings.lagda.md b/src/ring-theory/central-elements-rings.lagda.md index 322ff2bf1e..2499314b17 100644 --- a/src/ring-theory/central-elements-rings.lagda.md +++ b/src/ring-theory/central-elements-rings.lagda.md @@ -9,7 +9,6 @@ module ring-theory.central-elements-rings where ```agda open import foundation.identity-types open import foundation.propositions -open import foundation.sets open import foundation.universe-levels open import ring-theory.central-elements-semirings diff --git a/src/ring-theory/central-elements-semirings.lagda.md b/src/ring-theory/central-elements-semirings.lagda.md index d1088d2726..d991b52168 100644 --- a/src/ring-theory/central-elements-semirings.lagda.md +++ b/src/ring-theory/central-elements-semirings.lagda.md @@ -9,7 +9,6 @@ module ring-theory.central-elements-semirings where ```agda open import foundation.identity-types open import foundation.propositions -open import foundation.sets open import foundation.universe-levels open import group-theory.central-elements-monoids diff --git a/src/ring-theory/function-rings.lagda.md b/src/ring-theory/function-rings.lagda.md index abc009d145..4a3837e0ec 100644 --- a/src/ring-theory/function-rings.lagda.md +++ b/src/ring-theory/function-rings.lagda.md @@ -7,14 +7,11 @@ module ring-theory.function-rings where
Imports ```agda -open import foundation.function-extensionality open import foundation.identity-types open import foundation.sets open import foundation.universe-levels open import group-theory.abelian-groups -open import group-theory.function-abelian-groups -open import group-theory.function-monoids open import group-theory.monoids open import ring-theory.dependent-products-rings diff --git a/src/ring-theory/homomorphisms-rings.lagda.md b/src/ring-theory/homomorphisms-rings.lagda.md index aaa18347a8..3fed965f31 100644 --- a/src/ring-theory/homomorphisms-rings.lagda.md +++ b/src/ring-theory/homomorphisms-rings.lagda.md @@ -7,6 +7,8 @@ module ring-theory.homomorphisms-rings where
Imports ```agda +open import category-theory.precategories + open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types @@ -32,11 +34,9 @@ open import ring-theory.rings Ring homomorphisms are maps between rings that preserve the ring structure -## Definition +## Definitions ```agda -{- Ring homomorphisms -} - preserves-mul-hom-Ab : {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → type-hom-Ab (ab-Ring R1) (ab-Ring R2) → UU (l1 ⊔ l2) @@ -104,9 +104,11 @@ type-hom-Ring : {l1 l2 : Level} (R1 : Ring l1) (R : Ring l2) → UU (l1 ⊔ l2) type-hom-Ring R1 R2 = Σ (type-hom-Ab (ab-Ring R1) (ab-Ring R2)) (is-ring-homomorphism-hom-Ab R1 R2) +``` -{- Basic infrastructure for ring homomorphisms. -} +### Projections +```agda hom-ab-hom-Ring : {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → type-hom-Ring R1 R2 → type-hom-Ab (ab-Ring R1) (ab-Ring R2) @@ -159,9 +161,11 @@ is-ring-homomorphism-hom-Ring R1 R2 f = ( preserves-one-hom-Ring R1 R2 f) ``` -```agda -{- We characterize the identity type of ring homomorphisms -} +## Properties + +### Characterizing the identity type of ring homomorphisms +```agda htpy-hom-Ring : {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → type-hom-Ring R1 R2 → type-hom-Ring R1 R2 → UU (l1 ⊔ l2) @@ -225,9 +229,11 @@ hom-Ring : {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → Set (l1 ⊔ l2) pr1 (hom-Ring R1 R2) = type-hom-Ring R1 R2 pr2 (hom-Ring R1 R2) = is-set-type-hom-Ring R1 R2 +``` -{- We define the categorical structure of rings -} +### Rings form a precategory +```agda preserves-mul-id-hom-Ring : {l : Level} (R : Ring l) → preserves-mul-hom-Ab R R (id-hom-Ab (ab-Ring R)) preserves-mul-id-hom-Ring R x y = refl @@ -289,9 +295,9 @@ comp-hom-Ring : comp-hom-Ring R1 R2 R3 g f = pair ( hom-Ab-comp-hom-Ring R1 R2 R3 g f) ( is-ring-homomorphism-comp-hom-Ring R1 R2 R3 g f) +``` -{- We prove the laws of a category for Rings -} - +```agda is-associative-comp-hom-Ring : { l1 l2 l3 l4 : Level} ( R1 : Ring l1) (R2 : Ring l2) (R3 : Ring l3) (R4 : Ring l4) → @@ -348,4 +354,16 @@ comp-law-ab-Ring R1 R2 R3 g f = ( ab-Ring R1) ( ab-Ring R3) ( refl-htpy) + +Ring-Precat : (l : Level) → Precat (lsuc l) l +pr1 (Ring-Precat l) = Ring l +pr1 (pr2 (Ring-Precat l)) = hom-Ring +pr1 (pr1 (pr2 (pr2 (Ring-Precat l)))) {R1} {R2} {R3} = + comp-hom-Ring R1 R2 R3 +pr2 (pr1 (pr2 (pr2 (Ring-Precat l)))) {R1} {R2} {R3} {R4} = + is-associative-comp-hom-Ring R1 R2 R3 R4 +pr1 (pr2 (pr2 (pr2 (Ring-Precat l)))) = id-hom-Ring +pr1 (pr2 (pr2 (pr2 (pr2 (Ring-Precat l))))) {R1} {R2} f = + eq-htpy-hom-Ring R1 R2 (comp-hom-Ring R1 R2 R2 (id-hom-Ring R2) f) f refl-htpy +pr2 (pr2 (pr2 (pr2 (pr2 (Ring-Precat l))))) {R1} {R2} f = refl ``` diff --git a/src/ring-theory/ideals-rings.lagda.md b/src/ring-theory/ideals-rings.lagda.md index 08459a81cc..ae0e388de1 100644 --- a/src/ring-theory/ideals-rings.lagda.md +++ b/src/ring-theory/ideals-rings.lagda.md @@ -16,9 +16,7 @@ open import foundation.universe-levels open import group-theory.normal-subgroups open import group-theory.subgroups -open import group-theory.subgroups-abelian-groups -open import ring-theory.ideals-semirings open import ring-theory.rings open import ring-theory.subsets-rings ``` diff --git a/src/ring-theory/ideals-semirings.lagda.md b/src/ring-theory/ideals-semirings.lagda.md index 286517179c..2a15b13528 100644 --- a/src/ring-theory/ideals-semirings.lagda.md +++ b/src/ring-theory/ideals-semirings.lagda.md @@ -9,7 +9,6 @@ module ring-theory.ideals-semirings where ```agda open import foundation.cartesian-product-types open import foundation.dependent-pair-types -open import foundation.equational-reasoning open import foundation.identity-types open import foundation.propositions open import foundation.universe-levels diff --git a/src/ring-theory/isomorphisms-rings.lagda.md b/src/ring-theory/isomorphisms-rings.lagda.md index a88f972f87..bbe7b54992 100644 --- a/src/ring-theory/isomorphisms-rings.lagda.md +++ b/src/ring-theory/isomorphisms-rings.lagda.md @@ -38,8 +38,6 @@ open import ring-theory.rings ## Definition ```agda -{- We introduce ring isomorphisms -} - is-iso-hom-Ring : { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → type-hom-Ring R1 R2 → UU (l1 ⊔ l2) @@ -48,9 +46,11 @@ is-iso-hom-Ring R1 R2 f = ( λ g → ( Id (comp-hom-Ring R2 R1 R2 f g) (id-hom-Ring R2)) × ( Id (comp-hom-Ring R1 R2 R1 g f) (id-hom-Ring R1))) +``` -{- Infrastructure for invertible ring homomorphisms -} +### Projections +```agda inv-is-iso-hom-Ring : { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : type-hom-Ring R1 R2) → is-iso-hom-Ring R1 R2 f → type-hom-Ring R2 R1 @@ -95,9 +95,13 @@ is-retr-inv-map-is-iso-hom-Ring R1 R2 f is-iso-f = ( comp-hom-Ring R1 R2 R1 (inv-is-iso-hom-Ring R1 R2 f is-iso-f) f) ( id-hom-Ring R1) ( is-retr-inv-is-iso-hom-Ring R1 R2 f is-iso-f) +``` -{- Being invertible is a property -} +## Properties +### Being invertible is a property + +```agda all-elements-equal-is-iso-hom-Ring : { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (f : type-hom-Ring R1 R2) → all-elements-equal (is-iso-hom-Ring R1 R2 f) @@ -166,10 +170,12 @@ id-iso-Ring R1 = pair (id-hom-Ring R1) (is-iso-id-hom-Ring R1) iso-eq-Ring : { l : Level} (R1 R2 : Ring l) → Id R1 R2 → iso-Ring R1 R2 iso-eq-Ring R1 .R1 refl = id-iso-Ring R1 +``` -{- We first show that a ring homomorphism is an isomorphism if and only if - the underlying homomorphism of abelian groups is an isomorphism. -} +We first show that a ring homomorphism is an isomorphism if and only if the +underlying homomorphism of abelian groups is an isomorphism. +```agda is-iso-hom-Ab-hom-Ring : { l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) → type-hom-Ring R1 R2 → UU (l1 ⊔ l2) diff --git a/src/ring-theory/localizations-rings.lagda.md b/src/ring-theory/localizations-rings.lagda.md index 7ce4c47045..b40dfa7c81 100644 --- a/src/ring-theory/localizations-rings.lagda.md +++ b/src/ring-theory/localizations-rings.lagda.md @@ -2,7 +2,11 @@ ```agda module ring-theory.localizations-rings where +``` + +
Imports +```agda open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types @@ -11,20 +15,22 @@ open import foundation.fibers-of-maps open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositions -open import foundation.subtype-identity-principle open import foundation.subtypes open import foundation.universe-levels -open import group-theory.invertible-elements-monoids - open import ring-theory.homomorphisms-rings -open import ring-theory.ideals-rings open import ring-theory.invertible-elements-rings open import ring-theory.rings open import ring-theory.subsets-rings +``` + +
-{- We introduce homomorphism that invert specific elements -} +## Localization at a specific element +We introduce homomorphisms that invert specific elements. + +```agda module _ {l1 l2 : Level} (R1 : Ring l1) (R2 : Ring l2) (x : type-Ring R1) (f : type-hom-Ring R1 R2) @@ -64,7 +70,9 @@ is-right-inverse-inv-inverts-element-hom-Ring : ( inv-inverts-element-hom-Ring R S x f H)) ( one-Ring S) is-right-inverse-inv-inverts-element-hom-Ring R S x f H = pr2 (pr2 H) +``` +```agda inverts-element-comp-hom-Ring : {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R) (g : type-hom-Ring S T) (f : type-hom-Ring R S) → @@ -90,10 +98,11 @@ inverts-element-comp-hom-Ring R S T x g f H = ( map-hom-Ring S T g) ( is-right-inverse-inv-inverts-element-hom-Ring R S x f H)) ∙ ( preserves-one-hom-Ring S T g)))) +``` -{- We state the universal property of the localization of a Ring at a single - element x ∈ R. -} +### The universal property of the localization of a ring at a single element +```agda precomp-universal-property-localization-Ring : {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (x : type-Ring R) (f : type-hom-Ring R S) (H : inverts-element-hom-Ring R S x f) → @@ -134,7 +143,8 @@ center-unique-extension-universal-property-localization-Ring : universal-property-localization-Ring l3 R S x f H → (h : type-hom-Ring R T) (K : inverts-element-hom-Ring R T x h) → Σ (type-hom-Ring S T) (λ g → htpy-hom-Ring R T (comp-hom-Ring R S T g f) h) -center-unique-extension-universal-property-localization-Ring R S T x f H up-f h K = +center-unique-extension-universal-property-localization-Ring + R S T x f H up-f h K = center ( unique-extension-universal-property-localization-Ring R S T x f H up-f h K) @@ -173,10 +183,11 @@ is-equiv-up-localization-up-localization-Ring : is-iso-hom-Ring S T h is-equiv-up-localization-up-localization-Ring R S T x f inverts-f g inverts-g h H up-f up-g = {!is-iso-is-equiv-hom-Ring!} -} --------------------------------------------------------------------------------- +``` -{- We introduce homomorphisms that invert all elements of a subset of a ring -} +## Localization at a subset of a ring +```agda inverts-subset-hom-Ring : {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R) → (f : type-hom-Ring R S) → UU (l1 ⊔ l2 ⊔ l3) @@ -219,10 +230,11 @@ inverts-subset-comp-hom-Ring : inverts-subset-hom-Ring R T P (comp-hom-Ring R S T g f) inverts-subset-comp-hom-Ring R S T P g f H x p = inverts-element-comp-hom-Ring R S T x g f (H x p) +``` -{- We state the universal property of the localization of a Ring at a subset - of R. -} +### The universal property of the localization of a ring at a subset +```agda precomp-universal-property-localization-subset-Ring : {l1 l2 l3 l4 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3) (P : subset-Ring l4 R) → diff --git a/src/ring-theory/maximal-ideals-rings.lagda.md b/src/ring-theory/maximal-ideals-rings.lagda.md index d6d1e41f6e..40b63a592f 100644 --- a/src/ring-theory/maximal-ideals-rings.lagda.md +++ b/src/ring-theory/maximal-ideals-rings.lagda.md @@ -4,6 +4,14 @@ module ring-theory.maximal-ideals-rings where ``` +
Imports + +```agda + +``` + +
+ ## Idea A maximal ideal in a ring `R` is a proper ideal `I` of `R` such that for any diff --git a/src/ring-theory/nilpotent-elements-rings.lagda.md b/src/ring-theory/nilpotent-elements-rings.lagda.md index 98a388e331..e89ef733c9 100644 --- a/src/ring-theory/nilpotent-elements-rings.lagda.md +++ b/src/ring-theory/nilpotent-elements-rings.lagda.md @@ -7,8 +7,6 @@ module ring-theory.nilpotent-elements-rings where
Imports ```agda -open import elementary-number-theory.natural-numbers - open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.identity-types @@ -16,7 +14,6 @@ open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels -open import ring-theory.central-elements-rings open import ring-theory.nilpotent-elements-semirings open import ring-theory.powers-of-elements-rings open import ring-theory.rings diff --git a/src/ring-theory/nilpotent-elements-semirings.lagda.md b/src/ring-theory/nilpotent-elements-semirings.lagda.md index 379e97d3b7..ff5751db94 100644 --- a/src/ring-theory/nilpotent-elements-semirings.lagda.md +++ b/src/ring-theory/nilpotent-elements-semirings.lagda.md @@ -8,9 +8,6 @@ module ring-theory.nilpotent-elements-semirings where ```agda open import elementary-number-theory.addition-natural-numbers -open import elementary-number-theory.binomial-coefficients -open import elementary-number-theory.distance-natural-numbers -open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types @@ -24,11 +21,6 @@ open import foundation.universe-levels open import ring-theory.binomial-theorem-semirings open import ring-theory.powers-of-elements-semirings open import ring-theory.semirings -open import ring-theory.subsets-semirings -open import ring-theory.sums-semirings - -open import univalent-combinatorics.coproduct-types -open import univalent-combinatorics.standard-finite-types ```
diff --git a/src/ring-theory/quotient-rings.lagda.md b/src/ring-theory/quotient-rings.lagda.md index eeb63bba22..6627f40c9a 100644 --- a/src/ring-theory/quotient-rings.lagda.md +++ b/src/ring-theory/quotient-rings.lagda.md @@ -1,4 +1,4 @@ -# Qutoient Rings +# Qutoient rings ```agda module ring-theory.quotient-rings where diff --git a/src/ring-theory/rings.lagda.md b/src/ring-theory/rings.lagda.md index 3ada9ebdbc..ebfe43558d 100644 --- a/src/ring-theory/rings.lagda.md +++ b/src/ring-theory/rings.lagda.md @@ -454,7 +454,7 @@ module _ right-zero-law-mul-nat-scalar-Semiring (semiring-Ring R) left-unit-law-mul-nat-scalar-Ring : - (x : type-Ring R) → mul-nat-scalar-Ring 1 x ＝ x + (x : type-Ring R) → mul-nat-scalar-Ring 1 x ＝ x left-unit-law-mul-nat-scalar-Ring = left-unit-law-mul-nat-scalar-Semiring (semiring-Ring R) diff --git a/src/ring-theory/semirings.lagda.md b/src/ring-theory/semirings.lagda.md index 158eb70c1f..f1e5c14a83 100644 --- a/src/ring-theory/semirings.lagda.md +++ b/src/ring-theory/semirings.lagda.md @@ -306,7 +306,7 @@ module _ ( right-zero-law-mul-nat-scalar-Semiring n) left-unit-law-mul-nat-scalar-Semiring : - (x : type-Semiring R) → mul-nat-scalar-Semiring 1 x ＝ x + (x : type-Semiring R) → mul-nat-scalar-Semiring 1 x ＝ x left-unit-law-mul-nat-scalar-Semiring x = left-unit-law-add-Semiring R x left-nat-scalar-law-mul-Semiring : diff --git a/src/ring-theory/subsets-rings.lagda.md b/src/ring-theory/subsets-rings.lagda.md index 258c3df73d..56beb13180 100644 --- a/src/ring-theory/subsets-rings.lagda.md +++ b/src/ring-theory/subsets-rings.lagda.md @@ -7,7 +7,6 @@ module ring-theory.subsets-rings where
Imports ```agda -open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositional-extensionality open import foundation.propositions diff --git a/src/ring-theory/subsets-semirings.lagda.md b/src/ring-theory/subsets-semirings.lagda.md index ea3aa3d64c..ad4957c9e1 100644 --- a/src/ring-theory/subsets-semirings.lagda.md +++ b/src/ring-theory/subsets-semirings.lagda.md @@ -7,7 +7,6 @@ module ring-theory.subsets-semirings where
Imports ```agda -open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositional-extensionality open import foundation.propositions diff --git a/src/ring-theory/sums-rings.lagda.md b/src/ring-theory/sums-rings.lagda.md index 8f30f986d2..87002ca0c1 100644 --- a/src/ring-theory/sums-rings.lagda.md +++ b/src/ring-theory/sums-rings.lagda.md @@ -182,7 +182,7 @@ module _ sum-zero-Ring = sum-zero-Semiring (semiring-Ring R) ``` -### Splitting Sums +### Splitting sums ```agda split-sum-Ring : diff --git a/src/ring-theory/sums-semirings.lagda.md b/src/ring-theory/sums-semirings.lagda.md index 1657d6938d..2f25d986cd 100644 --- a/src/ring-theory/sums-semirings.lagda.md +++ b/src/ring-theory/sums-semirings.lagda.md @@ -247,7 +247,7 @@ module _ right-unit-law-add-Semiring R _ ∙ sum-zero-Semiring n ``` -### Splitting Sums +### Splitting sums ```agda split-sum-Semiring : diff --git a/src/set-theory/cumulative-hierarchy.lagda.md b/src/set-theory/cumulative-hierarchy.lagda.md index 8c8d3de3d6..a242d43523 100644 --- a/src/set-theory/cumulative-hierarchy.lagda.md +++ b/src/set-theory/cumulative-hierarchy.lagda.md @@ -15,7 +15,6 @@ open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equational-reasoning -open import foundation.equivalences open import foundation.existential-quantification open import foundation.functions open import foundation.functoriality-propositional-truncation @@ -30,8 +29,6 @@ open import foundation.sets open import foundation.truncated-types open import foundation.unit-type open import foundation.universe-levels - -open import orthogonal-factorization-systems.lifts-of-maps ```
@@ -465,7 +462,7 @@ needed. id-∈-cumulative-hierarchy x f = ap pr1 (compute-simple-prop-recursion-principle-cumulative-hierarchy _ _ f) - ∈-cumulative-hierarchy-mere-preimage : + ∈-cumulative-hierarchy-mere-preimage : { x : type-pseudo-cumulative-hierarchy V} → { A : UU l1} { f : A → type-pseudo-cumulative-hierarchy V} → diff --git a/src/species/composition-species-of-finite-inhabited-types.lagda.md b/src/species/composition-species-of-finite-inhabited-types.lagda.md index 0cf388b35e..979e7a97e3 100644 --- a/src/species/composition-species-of-finite-inhabited-types.lagda.md +++ b/src/species/composition-species-of-finite-inhabited-types.lagda.md @@ -26,7 +26,6 @@ open import foundation.universe-levels open import species.composition-species-of-subuniverse open import species.species-of-finite-inhabited-types -open import species.species-of-types-in-subuniverse open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.decidable-propositions diff --git a/src/species/composition-species-of-subuniverse.lagda.md b/src/species/composition-species-of-subuniverse.lagda.md index 8091fc5889..4210fcda89 100644 --- a/src/species/composition-species-of-subuniverse.lagda.md +++ b/src/species/composition-species-of-subuniverse.lagda.md @@ -9,21 +9,14 @@ module species.composition-species-of-subuniverse where ```agda open import foundation.cartesian-product-types open import foundation.contractible-types -open import foundation.decidable-types open import foundation.dependent-pair-types -open import foundation.diagonal-maps-of-types open import foundation.equality-cartesian-product-types -open import foundation.equality-dependent-pair-types open import foundation.equivalences -open import foundation.function-extensionality -open import foundation.functions open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types -open import foundation.inhabited-types -open import foundation.propositional-truncations open import foundation.propositions open import foundation.raising-universe-levels open import foundation.relaxed-sigma-decompositions @@ -35,19 +28,10 @@ open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice open import foundation.unit-type open import foundation.univalence -open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels open import species.large-composition-species-of-types -open import species.species-of-types open import species.species-of-types-in-subuniverse - -open import univalent-combinatorics.cartesian-product-types -open import univalent-combinatorics.decidable-propositions -open import univalent-combinatorics.dependent-function-types -open import univalent-combinatorics.dependent-sum-finite-types -open import univalent-combinatorics.finite-types -open import univalent-combinatorics.inhabited-finite-types ```
diff --git a/src/species/cycle-index-series-species-of-types.lagda.md b/src/species/cycle-index-series-species-of-types.lagda.md index 14d1d537ed..7eff2d1988 100644 --- a/src/species/cycle-index-series-species-of-types.lagda.md +++ b/src/species/cycle-index-series-species-of-types.lagda.md @@ -13,7 +13,6 @@ open import foundation.dependent-pair-types open import foundation.universe-levels open import univalent-combinatorics.cyclic-types -open import univalent-combinatorics.finite-types ```
diff --git a/src/species/derivatives-species-of-types.lagda.md b/src/species/derivatives-species-of-types.lagda.md index bda4cbadf0..089dca1f20 100644 --- a/src/species/derivatives-species-of-types.lagda.md +++ b/src/species/derivatives-species-of-types.lagda.md @@ -12,8 +12,6 @@ open import foundation.unit-type open import foundation.universe-levels open import species.species-of-types - -open import univalent-combinatorics.finite-types ```
diff --git a/src/species/equivalences-species-of-types.lagda.md b/src/species/equivalences-species-of-types.lagda.md index ff49cfbd99..1e0fac4234 100644 --- a/src/species/equivalences-species-of-types.lagda.md +++ b/src/species/equivalences-species-of-types.lagda.md @@ -13,8 +13,6 @@ open import foundation.univalence open import foundation.universe-levels open import species.species-of-types - -open import univalent-combinatorics.finite-types ```
diff --git a/src/species/exponents-species-of-types.lagda.md b/src/species/exponents-species-of-types.lagda.md index 9db10b6f3a..f6a748ac09 100644 --- a/src/species/exponents-species-of-types.lagda.md +++ b/src/species/exponents-species-of-types.lagda.md @@ -7,13 +7,9 @@ module species.exponents-species-of-types where
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.subuniverses -open import foundation.unit-type open import foundation.universe-levels open import species.species-of-types -open import species.species-of-types-in-subuniverse ```
diff --git a/src/species/large-composition-species-of-types.lagda.md b/src/species/large-composition-species-of-types.lagda.md index 25f607a6d1..52f862f0fe 100644 --- a/src/species/large-composition-species-of-types.lagda.md +++ b/src/species/large-composition-species-of-types.lagda.md @@ -18,16 +18,12 @@ open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types -open import foundation.inhabited-types -open import foundation.propositional-truncations open import foundation.relaxed-sigma-decompositions open import foundation.trivial-relaxed-sigma-decompositions open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-function-types open import foundation.type-arithmetic-dependent-pair-types -open import foundation.type-arithmetic-unit-type open import foundation.type-theoretic-principle-of-choice -open import foundation.unit-type open import foundation.univalence open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels diff --git a/src/species/morphisms-finite-species.lagda.md b/src/species/morphisms-finite-species.lagda.md index 45b5e36b98..c7d8084536 100644 --- a/src/species/morphisms-finite-species.lagda.md +++ b/src/species/morphisms-finite-species.lagda.md @@ -19,7 +19,6 @@ open import foundation.propositions open import foundation.sets open import foundation.universe-levels -open import species.morphisms-species-of-types open import species.species-of-finite-types open import univalent-combinatorics.finite-types diff --git a/src/species/morphisms-species-of-types.lagda.md b/src/species/morphisms-species-of-types.lagda.md index 9fb0d11455..4f7a6a35db 100644 --- a/src/species/morphisms-species-of-types.lagda.md +++ b/src/species/morphisms-species-of-types.lagda.md @@ -18,9 +18,6 @@ open import foundation.identity-types open import foundation.universe-levels open import species.species-of-types -open import species.species-of-types-in-subuniverse - -open import univalent-combinatorics.finite-types ``` diff --git a/src/species/species-of-finite-types.lagda.md b/src/species/species-of-finite-types.lagda.md index 7ee406b013..b50a012db7 100644 --- a/src/species/species-of-finite-types.lagda.md +++ b/src/species/species-of-finite-types.lagda.md @@ -14,7 +14,7 @@ open import species.species-of-types-in-subuniverse open import univalent-combinatorics.finite-types ``` -<\details> + ## Idea diff --git a/src/species/species-of-types-in-subuniverse.lagda.md b/src/species/species-of-types-in-subuniverse.lagda.md index 30d67ef0fa..944e5bb2af 100644 --- a/src/species/species-of-types-in-subuniverse.lagda.md +++ b/src/species/species-of-types-in-subuniverse.lagda.md @@ -12,7 +12,6 @@ open import foundation.equivalences open import foundation.functions open import foundation.identity-types open import foundation.subuniverses -open import foundation.unit-type open import foundation.universe-levels open import species.species-of-types diff --git a/src/structured-types/morphisms-coherent-h-spaces.lagda.md b/src/structured-types/morphisms-coherent-h-spaces.lagda.md index 2be2a4623b..c900d3c70c 100644 --- a/src/structured-types/morphisms-coherent-h-spaces.lagda.md +++ b/src/structured-types/morphisms-coherent-h-spaces.lagda.md @@ -205,9 +205,11 @@ hom-Coherent-H-Space : hom-Coherent-H-Space M N = Σ ( pointed-type-Coherent-H-Space M →* pointed-type-Coherent-H-Space N) ( preserves-unital-mul M N) +``` --- Homotopies of morphisms of wild unital magmas +### Homotopies of morphisms of wild unital magmas +```agda preserves-mul-htpy : {l1 l2 : Level} {A : UU l1} {B : UU l2} (μA : A → A → A) (μB : B → B → B) → {f g : A → B} (μf : preserves-mul μA μB f) (μg : preserves-mul μA μB g) → diff --git a/src/structured-types/pointed-homotopies.lagda.md b/src/structured-types/pointed-homotopies.lagda.md index e52f971eba..3a3dd4193d 100644 --- a/src/structured-types/pointed-homotopies.lagda.md +++ b/src/structured-types/pointed-homotopies.lagda.md @@ -57,8 +57,8 @@ module _ ( refl-htpy) ( inv (right-inv (preserves-point-function-pointed-Π A B f))) ( λ g → equiv-funext) - ( λ p → equiv-con-inv refl p (preserves-point-function-pointed-Π A B f) - ∘e equiv-inv (preserves-point-function-pointed-Π A B f) p) + ( λ p → equiv-con-inv refl p (preserves-point-function-pointed-Π A B f) ∘e + equiv-inv (preserves-point-function-pointed-Π A B f) p) eq-htpy-pointed-Π : (g : pointed-Π A B) → (htpy-pointed-Π g) → Id f g @@ -87,9 +87,11 @@ module _ eq-htpy-pointed-map : (g : A →* B) → (htpy-pointed-map g) → Id f g eq-htpy-pointed-map g = map-inv-equiv (extensionality-pointed-map g) +``` --- The category laws for pointed maps +### The category laws for pointed maps +```agda module _ {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) (f : A →* B) where diff --git a/src/structured-types/types-equipped-with-automorphisms.lagda.md b/src/structured-types/types-equipped-with-automorphisms.lagda.md index a6d6a9bdf5..a980311d50 100644 --- a/src/structured-types/types-equipped-with-automorphisms.lagda.md +++ b/src/structured-types/types-equipped-with-automorphisms.lagda.md @@ -4,6 +4,14 @@ module structured-types.types-equipped-with-automorphisms where ``` +
Imports + +```agda + +``` + +
+ ## Idea A type equipped with an automorphism is a pair consisting of a type `A` and an diff --git a/src/structured-types/wild-monoids.lagda.md b/src/structured-types/wild-monoids.lagda.md index bc797437df..2e4379158a 100644 --- a/src/structured-types/wild-monoids.lagda.md +++ b/src/structured-types/wild-monoids.lagda.md @@ -143,12 +143,14 @@ module _ ( ap (mul-Wild-Monoid x) (right-unit-law-mul-Wild-Monoid y))) ( right-unit-law-mul-Wild-Monoid (mul-Wild-Monoid x y)) unit-law-110-assoc-Wild-Monoid = pr1 (pr2 (pr2 (pr2 (pr2 M)))) +``` --- In the definition of morphisms of wild monoids we only require the unit and --- multiplication to be preserved. This is because we would need further --- coherence in wild monoids if we want morphisms list X → M to preserve the --- unital associator. +In the definition of morphisms of wild monoids we only require the unit and +multiplication to be preserved. This is because we would need further coherence +in wild monoids if we want morphisms list $X → M$ to preserve the unital +associator. +```agda module _ {l1 l2 : Level} (M : Wild-Monoid l1) (N : Wild-Monoid l2) where diff --git a/src/synthetic-homotopy-theory/26-descent.lagda.md b/src/synthetic-homotopy-theory/26-descent.lagda.md index 2151678883..c3110eff38 100644 --- a/src/synthetic-homotopy-theory/26-descent.lagda.md +++ b/src/synthetic-homotopy-theory/26-descent.lagda.md @@ -644,7 +644,7 @@ abstract {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) (f : A → B) → Id ( coherence-triangle-precompose-lifts P (refl-htpy' f)) - ( coherence-triangle-precompose-lifts-refl-htpy P f) + ( coherence-triangle-precompose-lifts-refl-htpy P f) compute-coherence-triangle-precompose-lifts P f = comp-htpy f ( λ g H → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P H) diff --git a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md index ca33de2903..4be5186191 100644 --- a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md @@ -66,7 +66,7 @@ naturality-right-unit : naturality-right-unit {p = refl} refl = refl naturality-right-unit-Ω² : - {l : Level} {A : UU l} {x : A} (α : type-Ω² x) → + {l : Level} {A : UU l} {x : A} (α : type-Ω² x) → Id (ap (concat' x refl) α) α naturality-right-unit-Ω² α = inv right-unit ∙ naturality-right-unit α diff --git a/src/synthetic-homotopy-theory/loop-spaces.lagda.md b/src/synthetic-homotopy-theory/loop-spaces.lagda.md index 581de1bdb6..4cfc200079 100644 --- a/src/synthetic-homotopy-theory/loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/loop-spaces.lagda.md @@ -119,7 +119,7 @@ module _ associative-mul-Ω x y z = assoc x y z ``` --- We compute transport of type-Ω +We compute transport of `type-Ω`. ```agda module _ diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index d090dbb1d8..5f9719f30d 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -187,7 +187,7 @@ module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c : suspension-structure X Z} where - refl-htpy-suspension-structure : htpy-suspension-structure c c + refl-htpy-suspension-structure : htpy-suspension-structure c c refl-htpy-suspension-structure = refl , (refl , right-unit-htpy) is-refl-refl-htpy-suspension-structure : refl-htpy-suspension-structure ＝ htpy-eq-suspension-structure refl @@ -457,7 +457,7 @@ module _ {l1 l2 : Level} (X : Pointed-Type l1) (Y : Pointed-Type l2) where - equiv-susp-loop-adj : (suspension-Pointed-Type X →* Y) ≃ (X →* Ω Y) + equiv-susp-loop-adj : (suspension-Pointed-Type X →* Y) ≃ (X →* Ω Y) equiv-susp-loop-adj = ( left-unit-law-Σ-is-contr ( is-contr-total-path (pt-Pointed-Type Y)) diff --git a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md index e326f1a9bd..b8931b7652 100644 --- a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md @@ -20,6 +20,8 @@ open import synthetic-homotopy-theory.iterated-loop-spaces +## Definition + ```agda module _ {l : Level} @@ -35,6 +37,8 @@ module _ refl-Ω³ = refl ``` +## Operations + ```agda x-concat-Ω³ : {l : Level} {A : UU l} {a : A} → type-Ω³ a → type-Ω³ a → type-Ω³ a @@ -62,9 +66,13 @@ ap-z-concat-Ω³ : {l : Level} {A : UU l} {a : A} {α α' β β' : type-Ω³ a} (s : Id α α') (t : Id β β') → Id (z-concat-Ω³ α β) (z-concat-Ω³ α' β') ap-z-concat-Ω³ s t = k-concat-Id⁴ s t +``` --- The unit laws for the three concatenations on Ω³ +## Properties +### The unit laws for the three concatenations on Ω³ + +```agda left-unit-law-x-concat-Ω³ : {l : Level} {A : UU l} {a : A} (α : type-Ω³ a) → Id (x-concat-Ω³ refl-Ω³ α) α @@ -111,6 +119,7 @@ right-unit-law-z-concat-Ω³ : right-unit-law-z-concat-Ω³ α = ( right-unit-law-z-concat-Id³ α) ∙ {!!} +-} {- ( ( inv right-unit) ∙ ( ( inv-nat-htpy (λ ω → right-unit-law-horizontal-concat-Id² ω) α) ∙ @@ -122,10 +131,11 @@ right-unit-law-z-concat-Ω³ α = ( inv-nat-htpy (λ ω → right-unit) z) ∙ ( ap-id z)) α) ∙ ( ap-id α)))))) -} --} +``` --- The interchange laws for Ω³ +### The interchange laws for Ω³ +```agda interchange-x-y-concat-Ω³ : {l : Level} {A : UU l} {a : A} (α β γ δ : type-Ω³ a) → Id ( y-concat-Ω³ (x-concat-Ω³ α β) (x-concat-Ω³ γ δ)) @@ -144,9 +154,11 @@ interchange-y-z-concat-Ω³ : ( y-concat-Ω³ (z-concat-Ω³ α γ) (z-concat-Ω³ β δ)) interchange-y-z-concat-Ω³ α β γ δ = inv right-unit ∙ interchange-y-z-concat-Id³ α β γ δ +``` --- The Eckmann-Hilton connections in Ω³ +### The Eckmann-Hilton connections in Ω³ +```agda outer-eckmann-hilton-connection-x-y-concat-Ω³ : {l : Level} {A : UU l} {a : A} (α δ : type-Ω³ a) → Id (y-concat-Ω³ α δ) (x-concat-Ω³ α δ) diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md index 5cccc10020..2e2774dbf5 100644 --- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md @@ -667,9 +667,11 @@ abstract ( λ k → Id (pr1 s k) (pr1 t k)) ( (pr1 (pr2 s)) ∙ (inv (pr1 (pr2 t)))) ( equiv-comparison-map-Eq-ELIM-ℤ P p0 pS s t))) +``` --- We finally arrive at the dependent universal property of ℤ +We finally arrive at the dependent universal property of ℤ +```agda abstract is-contr-ELIM-ℤ : { l1 : Level} (P : ℤ → UU l1) → @@ -677,9 +679,11 @@ abstract is-contr (ELIM-ℤ P p0 pS) is-contr-ELIM-ℤ P p0 pS = is-proof-irrelevant-is-prop (is-prop-ELIM-ℤ P p0 pS) (Elim-ℤ P p0 pS) +``` --- The universal property of ℤ is now just a special case +The universal property of ℤ is now just a special case +```agda ELIM-ℤ' : { l1 : Level} {X : UU l1} (x : X) (e : X ≃ X) → UU l1 ELIM-ℤ' {X = X} x e = ELIM-ℤ (λ k → X) x (λ k → e) diff --git a/src/trees/extensional-w-types.lagda.md b/src/trees/extensional-w-types.lagda.md index 026370074e..ce254d5489 100644 --- a/src/trees/extensional-w-types.lagda.md +++ b/src/trees/extensional-w-types.lagda.md @@ -181,5 +181,5 @@ module _ ( fundamental-theorem-id' ( λ z → extensional-Eq-eq-𝕎) ( H (tree-𝕎 x (λ y → w))))) - ( λ y → equiv-tr B {y = y})) + ( λ y → equiv-tr B {y = y})) ``` diff --git a/src/trees/functoriality-w-types.lagda.md b/src/trees/functoriality-w-types.lagda.md index 3330772010..cc27f60a68 100644 --- a/src/trees/functoriality-w-types.lagda.md +++ b/src/trees/functoriality-w-types.lagda.md @@ -86,7 +86,7 @@ abstract ( λ α → equiv-Π ( λ (b : B a) → - map-𝕎 D f e (α b) ＝ γ (tr D p (map-equiv (e a) b))) + map-𝕎 D f e (α b) ＝ γ (tr D p (map-equiv (e a) b))) ( inv-equiv (e a)) ( λ d → ( equiv-concat' diff --git a/src/trees/undirected-trees.lagda.md b/src/trees/undirected-trees.lagda.md index 67b153f1ef..f93370e834 100644 --- a/src/trees/undirected-trees.lagda.md +++ b/src/trees/undirected-trees.lagda.md @@ -363,29 +363,45 @@ has-decidable-equality-node-Undirected-Tree T x y = ### Any trail in a tree is a path --- ```agda -- module \_ -- {l1 l2 : Level} (T : Tree l1 l2) -- where - --- is-path-is-trail-walk-Undirected-Tree : -- {x y : node-Undirected-Tree T} (w -: walk-Undirected-Tree T x y) → -- is-trail-walk-Undirected-Tree T w → -is-path-walk-Undirected-Tree T w -- is-path-is-trail-walk-Undirected-Tree {x} -{y} w H {pair u KU} {pair v K} p with -- -is-vertex-on-first-or-second-segment-walk-Undirected-Graph -- -(undirected-graph-Undirected-Tree T) w (pair u KU) (pair v K) -- ... | inl L = -{!!} -- where -- w1' : walk-Undirected-Tree T x u -- w1' = -- -first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w (pair -u KU) -- w1 : walk-Undirected-Tree T x v -- w1 = -- -first-segment-walk-Undirected-Graph -- ( undirected-graph-Undirected-Tree T) -- -( w1') -- ( pair v L) -- w' : walk-Undirected-Tree T v u -- w' = {!!} -- ... | -inr L = {!!} -- where -- w1 : walk-Undirected-Tree T x u -- w1 = -- -first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w (pair -u KU) - --- {- -- where -- w1 : walk-Undirected-Tree T x -(node-node-on-walk-Undirected-Tree T w u) -- w1 = -- -first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w u -- -w2' : walk-Undirected-Tree T (node-node-on-walk-Undirected-Tree T w u) y -- w2' -= -- second-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w -u -- w2 : walk-Undirected-Tree T (node-node-on-walk-Undirected-Tree T w u) -(node-node-on-walk-Undirected-Tree T w v) -- w2 = -{!first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w2' -!} -- -} -- ``` +```agda +-- module _ +-- {l1 l2 : Level} (T : Tree l1 l2) +-- where + +-- is-path-is-trail-walk-Undirected-Tree : +-- {x y : node-Undirected-Tree T} (w : walk-Undirected-Tree T x y) → +-- is-trail-walk-Undirected-Tree T w → is-path-walk-Undirected-Tree T w +-- is-path-is-trail-walk-Undirected-Tree {x} {y} w H {pair u KU} {pair v K} p with +-- is-vertex-on-first-or-second-segment-walk-Undirected-Graph +-- (undirected-graph-Undirected-Tree T) w (pair u KU) (pair v K) +-- ... | inl L = {!!} +-- where +-- w1' : walk-Undirected-Tree T x u +-- w1' = +-- first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w (pair u KU) +-- w1 : walk-Undirected-Tree T x v +-- w1 = +-- first-segment-walk-Undirected-Graph +-- ( undirected-graph-Undirected-Tree T) +-- ( w1') +-- ( pair v L) +-- w' : walk-Undirected-Tree T v u +-- w' = {!!} +-- ... | inr L = {!!} +-- where +-- w1 : walk-Undirected-Tree T x u +-- w1 = +-- first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w (pair u KU) + +-- {- +-- where +-- w1 : walk-Undirected-Tree T x (node-node-on-walk-Undirected-Tree T w u) +-- w1 = +-- first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w u +-- w2' : walk-Undirected-Tree T (node-node-on-walk-Undirected-Tree T w u) y +-- w2' = +-- second-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w u +-- w2 : walk-Undirected-Tree T (node-node-on-walk-Undirected-Tree T w u) (node-node-on-walk-Undirected-Tree T w v) +-- w2 = {!first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Tree T) w2' !} +-- -} +``` diff --git a/src/trees/w-types.lagda.md b/src/trees/w-types.lagda.md index 55ad7aaca9..b970c28610 100644 --- a/src/trees/w-types.lagda.md +++ b/src/trees/w-types.lagda.md @@ -296,7 +296,7 @@ structure-htpy-hom-𝕎-Alg : ( structure-hom-algebra-polynomial-endofunctor (𝕎-Alg A B) X f)) structure-htpy-hom-𝕎-Alg {A = A} {B} X (pair f μ-f) (pair x α) = ( ( ( compute-structure-htpy-hom-𝕎-Alg X x α - ( htpy-htpy-hom-𝕎-Alg X (pair f μ-f))) ∙ + ( htpy-htpy-hom-𝕎-Alg X (pair f μ-f))) ∙ ( inv right-unit)) ∙ ( ap ( concat ( ap diff --git a/src/type-theories/fibered-dependent-type-theories.lagda.md b/src/type-theories/fibered-dependent-type-theories.lagda.md index 1ba2e047ca..57acb1b025 100644 --- a/src/type-theories/fibered-dependent-type-theories.lagda.md +++ b/src/type-theories/fibered-dependent-type-theories.lagda.md @@ -336,11 +336,11 @@ module fibered where ### Generic element structures on fibered systems equipped with a weakening structure -```agda - {- We define what it means for a fibered system equipped with fibered - weakening structure over a system equipped with weakening structure and - the structure of generic elements to be equipped with generic elements. -} +We define what it means for a fibered system equipped with fibered weakening +structure over a system equipped with weakening structure and the structure of +generic elements to be equipped with generic elements. +```agda record fibered-generic-element {l1 l2 l3 l4 : Level} {A : system l1 l2} {B : fibered-system l3 l4 A} {WA : weakening A} (W : fibered-weakening B WA) (δ : generic-element WA) : diff --git a/src/type-theories/sections-dependent-type-theories.lagda.md b/src/type-theories/sections-dependent-type-theories.lagda.md index 51320fc6d7..fd4754a43e 100644 --- a/src/type-theories/sections-dependent-type-theories.lagda.md +++ b/src/type-theories/sections-dependent-type-theories.lagda.md @@ -47,7 +47,7 @@ module sections-dtt where section-system.slice (precomp-section-system g f) X = precomp-section-system ( section-system.slice g (section-system.type f X)) - ( section-system.slice f X) + ( section-system.slice f X) transpose-bifibered-system : {l1 l2 l3 l4 l5 l6 l7 l8 : Level} {A : system l1 l2} diff --git a/src/type-theories/simple-type-theories.lagda.md b/src/type-theories/simple-type-theories.lagda.md index b95238fc56..a4f2db995c 100644 --- a/src/type-theories/simple-type-theories.lagda.md +++ b/src/type-theories/simple-type-theories.lagda.md @@ -430,7 +430,7 @@ module simple where ( generic-element.slice δ X) record type-theory - (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2) + (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2) where field typ : UU l1 diff --git a/src/univalent-combinatorics/counting-fibers-of-maps.lagda.md b/src/univalent-combinatorics/counting-fibers-of-maps.lagda.md index 9b9b84f807..7bf347e7c7 100644 --- a/src/univalent-combinatorics/counting-fibers-of-maps.lagda.md +++ b/src/univalent-combinatorics/counting-fibers-of-maps.lagda.md @@ -2,14 +2,12 @@ ```agda module univalent-combinatorics.counting-fibers-of-maps where +``` -open import elementary-number-theory.sums-of-natural-numbers +
Imports -open import foundation.fibers-of-maps -open import foundation.identity-types -open import foundation.universe-levels +```agda -open import univalent-combinatorics.counting -open import univalent-combinatorics.counting-dependent-pair-types -open import univalent-combinatorics.double-counting ``` + +
diff --git a/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md b/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md index 24d4d962bf..ac5b32af17 100644 --- a/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md +++ b/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md @@ -16,8 +16,6 @@ open import foundation.decidable-equivalence-relations open import foundation.decidable-relations open import foundation.decidable-types open import foundation.dependent-pair-types -open import foundation.diagonal-maps-of-types -open import foundation.embeddings open import foundation.equivalence-relations open import foundation.equivalences open import foundation.functions @@ -25,7 +23,6 @@ open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.propositional-truncations open import foundation.propositions -open import foundation.surjective-maps open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels diff --git a/src/univalent-combinatorics/decidable-propositions.lagda.md b/src/univalent-combinatorics/decidable-propositions.lagda.md index db60e9e946..366b59b2bc 100644 --- a/src/univalent-combinatorics/decidable-propositions.lagda.md +++ b/src/univalent-combinatorics/decidable-propositions.lagda.md @@ -17,12 +17,10 @@ open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types -open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels open import univalent-combinatorics.counting -open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` diff --git a/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md b/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md index 9e8274e5bc..534bcd69f1 100644 --- a/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md +++ b/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md @@ -39,9 +39,11 @@ open import univalent-combinatorics.standard-finite-types -```agda --- trunc-Set distributes over Π indexed by Fin +## Theorem + +`trunc-Set` distributes over `Π` indexed by `Fin`. +```agda abstract distributive-trunc-Π-Fin-Set : {l : Level} (k : ℕ) (A : Fin k → UU l) → diff --git a/src/univalent-combinatorics/embeddings-standard-finite-types.lagda.md b/src/univalent-combinatorics/embeddings-standard-finite-types.lagda.md index 6b20fe54a1..a139c74528 100644 --- a/src/univalent-combinatorics/embeddings-standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/embeddings-standard-finite-types.lagda.md @@ -61,7 +61,7 @@ abstract (k l : ℕ) (f : Fin (succ-ℕ k) ↪ Fin (succ-ℕ l)) (d : is-decidable (is-inl-Fin l (map-emb f (inr star)))) (x : Fin k) (e : is-decidable (is-inl-Fin l (map-emb f (inl x)))) - (x' : Fin k) (e' : is-decidable (is-inl-Fin l (map-emb f (inl x')))) → + (x' : Fin k) (e' : is-decidable (is-inl-Fin l (map-emb f (inl x')))) → Id ( cases-map-reduce-emb-Fin k l f d x e) ( cases-map-reduce-emb-Fin k l f d x' e') → Id x x' @@ -124,5 +124,9 @@ pr2 (reduce-emb-Fin k l f) = is-emb-map-reduce-emb-Fin k l f ### Any embedding from `Fin k` into itself is surjective --- -`agda -- is-split-surjective-is-emb-Fin : -- {k : ℕ} {f : Fin k → Fin k} → is-emb f → is-split-surjective f -- is-split-surjective-is-emb-Fin {zero-ℕ} {f} H () -- is-split-surjective-is-emb-Fin {succ-ℕ k} {f} H y = {!!} -- ` +```agda +-- is-split-surjective-is-emb-Fin : +-- {k : ℕ} {f : Fin k → Fin k} → is-emb f → is-split-surjective f +-- is-split-surjective-is-emb-Fin {zero-ℕ} {f} H () +-- is-split-surjective-is-emb-Fin {succ-ℕ k} {f} H y = {!!} -- +``` diff --git a/src/univalent-combinatorics/embeddings.lagda.md b/src/univalent-combinatorics/embeddings.lagda.md index c190af550c..86803268b1 100644 --- a/src/univalent-combinatorics/embeddings.lagda.md +++ b/src/univalent-combinatorics/embeddings.lagda.md @@ -11,7 +11,6 @@ open import foundation.embeddings public open import elementary-number-theory.natural-numbers -open import foundation.contractible-types open import foundation.coproduct-types open import foundation.decidable-embeddings open import foundation.decidable-types diff --git a/src/univalent-combinatorics/finite-presentations.lagda.md b/src/univalent-combinatorics/finite-presentations.lagda.md index 5560b14977..94f2f33ec7 100644 --- a/src/univalent-combinatorics/finite-presentations.lagda.md +++ b/src/univalent-combinatorics/finite-presentations.lagda.md @@ -4,6 +4,14 @@ module univalent-combinatorics.finite-presentations where ``` +
Imports + +```agda + +``` + +
+ ## Idea Finitely presented types are types A equipped with a map f : Fin k → A such that diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index 20c18f4cf8..33d43958b6 100644 --- a/src/univalent-combinatorics/finite-types.lagda.md +++ b/src/univalent-combinatorics/finite-types.lagda.md @@ -30,12 +30,10 @@ open import foundation.raising-universe-levels open import foundation.sets open import foundation.subtypes open import foundation.subuniverses -open import foundation.surjective-maps open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-empty-type open import foundation.unit-type open import foundation.univalence -open import foundation.universal-property-propositional-truncation open import foundation.universe-levels open import univalent-combinatorics.counting diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md index af41ca2596..6936699bf5 100644 --- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md @@ -11,7 +11,6 @@ open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functions open import foundation.functoriality-dependent-function-types -open import foundation.homotopies open import foundation.identity-types open import foundation.inhabited-types open import foundation.propositions diff --git a/src/univalent-combinatorics/lists.lagda.md b/src/univalent-combinatorics/lists.lagda.md index 9d723e491f..6099f9a890 100644 --- a/src/univalent-combinatorics/lists.lagda.md +++ b/src/univalent-combinatorics/lists.lagda.md @@ -87,8 +87,15 @@ reverse-list (cons a l) = concat-list (reverse-list l) (in-list a) data _∈-list_ {l : Level} {A : UU l} : A → list A → UU l where is-head : (a : A) (l : list A) → a ∈-list (cons a l) is-in-tail : (a x : A) (l : list A) → a ∈-list l → a ∈-list (cons x l) + +unit-list : {l : Level} {A : UU l} → A → list A +unit-list a = cons a nil ``` +## Properties + +### Characterizing the identity type of lists + ```agda Eq-list : {l1 : Level} {A : UU l1} → list A → list A → UU l1 Eq-list {l1} nil nil = raise-unit l1 @@ -232,16 +239,14 @@ has-decidable-equality-has-decidable-equality-list d x y = ( eq-Eq-list (cons x nil) (cons y nil)) ( d (cons x nil) (cons y nil))) ( raise-star) +``` --------------------------------------------------------------------------------- - -unit-list : - {l1 : Level} {A : UU l1} → A → list A -unit-list a = cons a nil +### Functoriality of the list operation -{- First we introduce the functoriality of the list operation, because it will - come in handy when we try to define and prove more advanced things. -} +First we introduce the functoriality of the list operation, because it will come +in handy when we try to define and prove more advanced things. +```agda functor-list : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → list A → list B @@ -262,10 +267,14 @@ composition-law-functor-list : composition-law-functor-list f g nil = refl composition-law-functor-list f g (cons a x) = ap (cons (g (f a))) (composition-law-functor-list f g x) +``` + +### List concatenation is associative and unital -{- Concatenation of lists is an associative operation and nil is the unit for - list concatenation. -} +Concatenation of lists is an associative operation and nil is the unit for list +concatenation. +```agda assoc-concat-list : {l1 : Level} {A : UU l1} (x y z : list A) → Id (concat-list (concat-list x y) z) (concat-list x (concat-list y z)) @@ -289,10 +298,11 @@ list-Monoid X = pair ( pair (list-Set X) (pair concat-list assoc-concat-list)) ( pair nil (pair left-unit-law-concat-list right-unit-law-concat-list)) +``` -{- The length operation or course behaves well with respect to the other list - operations. -} +### The length operation behaves well with respect to the other list operations +```agda length-nil : {l1 : Level} {A : UU l1} → Id (length-list {A = A} nil) zero-ℕ @@ -312,9 +322,11 @@ length-functor-list : length-functor-list f nil = refl length-functor-list f (cons x l) = ap succ-ℕ (length-functor-list f l) +``` -{- We now prove the properties of flattening. -} +### Properties of flattening +```agda flatten-unit-list : {l1 : Level} {A : UU l1} (x : list A) → Id (flatten-list (unit-list x)) x @@ -346,9 +358,11 @@ flatten-flatten-list nil = refl flatten-flatten-list (cons a x) = ( flatten-concat-list a (flatten-list x)) ∙ ( ap (concat-list (flatten-list a)) (flatten-flatten-list x)) +``` -{- Next, we prove the basic properties of list reversal. -} +### Properties of list reversal +```agda reverse-unit-list : {l1 : Level} {A : UU l1} (a : A) → Id (reverse-list (unit-list a)) (unit-list a) @@ -396,12 +410,14 @@ reverse-reverse-list nil = refl reverse-reverse-list (cons a x) = ( reverse-concat-list (reverse-list x) (unit-list a)) ∙ ( ap (concat-list (unit-list a)) (reverse-reverse-list x)) +``` --------------------------------------------------------------------------------- +## Head and tail operations -{- Next we define the head and tail operations, and we define the operations - of picking and removing the last element from a list. -} +We define the head and tail operations, and we define the operations of picking +and removing the last element from a list. +```agda head-list : {l1 : Level} {A : UU l1} → list A → list A head-list nil = nil @@ -428,9 +444,11 @@ remove-last-element-list (cons a (cons b x)) = cons' : {l1 : Level} {A : UU l1} → list A → A → list A cons' x a = concat-list x (unit-list a) +``` -{- We prove the basic properties about heads and tails and their duals. -} +### Properties of heads and tails and their duals +```agda eta-list : {l1 : Level} {A : UU l1} (x : list A) → Id (concat-list (head-list x) (tail-list x)) x diff --git a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md index b6dcb012cc..1344b4ff0c 100644 --- a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md +++ b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md @@ -1441,7 +1441,7 @@ module _ ( ( inv (eq-orientation-two-elements-count i j np)) ∙ ( ap ( λ Y' → pr1 (orientation-two-elements-count i j np Y')) - ( eq-equal-elements-standard-2-Element-Decidable-Subtype + ( eq-equal-elements-standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) ( np) ( λ p → np' (inv p)) @@ -1545,7 +1545,7 @@ module _ ( np))) ( x)) ( x)))))) ∙ - ( ap + ( ap ( λ w → pr1 ( cases-orientation-two-elements-count i j Y @@ -2277,7 +2277,7 @@ module _ ( np)))))) ( nq) ( nr)) ∙ - ( is-fixed-point-standard-transposition + ( is-fixed-point-standard-transposition ( has-decidable-equality-count eX) ( np) ( x) @@ -2658,7 +2658,7 @@ module _ ex-falso ( pr2 T ( eq-pair-Σ - ( inward-edge-right-two-elements-orientation-count i j np + ( inward-edge-right-two-elements-orientation-count i j np ( pr1 T) ( y) ( tr diff --git a/src/univalent-combinatorics/pi-finite-types.lagda.md b/src/univalent-combinatorics/pi-finite-types.lagda.md index 764c76cb69..8cb1d3d6ef 100644 --- a/src/univalent-combinatorics/pi-finite-types.lagda.md +++ b/src/univalent-combinatorics/pi-finite-types.lagda.md @@ -335,7 +335,7 @@ pr2 (coprod-π-Finite k A B) = ```agda Maybe-π-Finite : - {l : Level} (k : ℕ) → π-Finite l k → π-Finite l k + {l : Level} (k : ℕ) → π-Finite l k → π-Finite l k Maybe-π-Finite k A = coprod-π-Finite k A (unit-π-Finite k) diff --git a/src/univalent-combinatorics/presented-pi-finite-types.lagda.md b/src/univalent-combinatorics/presented-pi-finite-types.lagda.md index fab71141cf..2edfa3492b 100644 --- a/src/univalent-combinatorics/presented-pi-finite-types.lagda.md +++ b/src/univalent-combinatorics/presented-pi-finite-types.lagda.md @@ -4,6 +4,14 @@ module univalent-combinatorics.presented-pi-finite-types where ``` +
Imports + +```agda + +``` + +
+ ## Idea A type `A` is said to be finitely `π_0`-presented if there is a standard pruned diff --git a/src/univalent-combinatorics/ramsey-theory.lagda.md b/src/univalent-combinatorics/ramsey-theory.lagda.md index 3fe2990016..ac00df2e90 100644 --- a/src/univalent-combinatorics/ramsey-theory.lagda.md +++ b/src/univalent-combinatorics/ramsey-theory.lagda.md @@ -2,7 +2,11 @@ ```agda module univalent-combinatorics.ramsey-theory where +``` + +
Imports +```agda open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types @@ -13,7 +17,11 @@ open import foundation.universe-levels open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types +``` + +
+```agda coloring : {l : Level} (k : ℕ) → UU l → UU l coloring k X = X → Fin k diff --git a/src/univalent-combinatorics/sigma-decompositions.lagda.md b/src/univalent-combinatorics/sigma-decompositions.lagda.md index bbcb8d7935..15b8d6ffc2 100644 --- a/src/univalent-combinatorics/sigma-decompositions.lagda.md +++ b/src/univalent-combinatorics/sigma-decompositions.lagda.md @@ -10,22 +10,13 @@ module univalent-combinatorics.sigma-decompositions where open import foundation.sigma-decompositions public open import foundation.cartesian-product-types -open import foundation.contractible-types -open import foundation.decidable-propositions open import foundation.dependent-pair-types open import foundation.embeddings -open import foundation.empty-types -open import foundation.equality-dependent-pair-types -open import foundation.equational-reasoning open import foundation.equivalences -open import foundation.fibers-of-maps -open import foundation.functions open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types -open import foundation.functoriality-propositional-truncation open import foundation.homotopies open import foundation.identity-types -open import foundation.images open import foundation.inhabited-types open import foundation.propositions open import foundation.relaxed-sigma-decompositions @@ -39,7 +30,6 @@ open import univalent-combinatorics.decidable-equivalence-relations open import univalent-combinatorics.dependent-sum-finite-types open import univalent-combinatorics.finite-types open import univalent-combinatorics.inhabited-finite-types -open import univalent-combinatorics.quotients-finite-types open import univalent-combinatorics.type-duality ``` diff --git a/src/univalent-combinatorics/small-types.lagda.md b/src/univalent-combinatorics/small-types.lagda.md index dd90638d11..b561abbe2b 100644 --- a/src/univalent-combinatorics/small-types.lagda.md +++ b/src/univalent-combinatorics/small-types.lagda.md @@ -13,11 +13,8 @@ open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.propositional-truncations -open import foundation.raising-universe-levels -open import foundation.univalence open import foundation.universe-levels -open import univalent-combinatorics.counting open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index a267d18322..91e017bfce 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -310,22 +310,26 @@ is-injective-succ-Fin (succ-ℕ k) {inr star} {inl y} p = is-injective-succ-Fin (succ-ℕ k) {inr star} {inr star} p = refl ``` -```agda --- We define a function skip-neg-two-Fin in order to define pred-Fin. +We define a function `skip-neg-two-Fin` in order to define `pred-Fin`. +```agda skip-neg-two-Fin : (k : ℕ) → Fin k → Fin (succ-ℕ k) skip-neg-two-Fin (succ-ℕ k) (inl x) = inl (inl x) skip-neg-two-Fin (succ-ℕ k) (inr x) = neg-one-Fin (succ-ℕ k) +``` --- We define the predecessor function on Fin k. +We define the predecessor function on `Fin k`. +```agda pred-Fin : (k : ℕ) → Fin k → Fin k pred-Fin (succ-ℕ k) (inl x) = skip-neg-two-Fin k (pred-Fin k x) pred-Fin (succ-ℕ k) (inr x) = neg-two-Fin k +``` --- We now turn to the exercise. +We now turn to the exercise. +```agda pred-zero-Fin : (k : ℕ) → is-neg-one-Fin (succ-ℕ k) (pred-Fin (succ-ℕ k) (zero-Fin k)) pred-zero-Fin (zero-ℕ) = refl diff --git a/src/univalent-combinatorics/surjective-maps.lagda.md b/src/univalent-combinatorics/surjective-maps.lagda.md index b3f11e197e..c72c82b577 100644 --- a/src/univalent-combinatorics/surjective-maps.lagda.md +++ b/src/univalent-combinatorics/surjective-maps.lagda.md @@ -17,26 +17,18 @@ open import foundation.decidable-equality open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.functions -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.inhabited-types open import foundation.propositional-truncations open import foundation.propositions -open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types -open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels open import univalent-combinatorics.counting open import univalent-combinatorics.counting-decidable-subtypes open import univalent-combinatorics.counting-dependent-pair-types open import univalent-combinatorics.decidable-dependent-function-types -open import univalent-combinatorics.dependent-sum-finite-types open import univalent-combinatorics.embeddings open import univalent-combinatorics.fibers-of-maps open import univalent-combinatorics.finite-types -open import univalent-combinatorics.inhabited-finite-types open import univalent-combinatorics.standard-finite-types ``` diff --git a/src/univalent-combinatorics/symmetric-difference.lagda.md b/src/univalent-combinatorics/symmetric-difference.lagda.md index ddee0c7021..98c32e4d1e 100644 --- a/src/univalent-combinatorics/symmetric-difference.lagda.md +++ b/src/univalent-combinatorics/symmetric-difference.lagda.md @@ -2,7 +2,11 @@ ```agda module univalent-combinatorics.symmetric-difference where +``` + +
Imports +```agda open import foundation.symmetric-difference public open import elementary-number-theory.addition-natural-numbers @@ -10,22 +14,21 @@ open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers open import foundation.coproduct-types -open import foundation.decidable-subtypes open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types open import foundation.intersections-subtypes open import foundation.mere-equivalences open import foundation.propositional-truncations -open import foundation.subtypes open import foundation.universe-levels -open import foundation.xor open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.decidable-subtypes open import univalent-combinatorics.finite-types ``` +
+ ```agda module _ {l l1 l2 : Level} (X : UU l) (F : is-finite X) @@ -52,24 +55,24 @@ module _ ( F))))) eq-symmetric-difference = ( ( coprod-eq-is-finite - ( is-finite-type-decidable-subtype P F) - ( is-finite-type-decidable-subtype Q F))) ∙ + ( is-finite-type-decidable-subtype P F) + ( is-finite-type-decidable-subtype Q F))) ∙ ( ( ap - ( number-of-elements-has-finite-cardinality) - ( all-elements-equal-has-finite-cardinality - ( has-finite-cardinality-is-finite - ( is-finite-coprod - ( is-finite-type-decidable-subtype P F) - ( is-finite-type-decidable-subtype Q F))) - ( pair - ( number-of-elements-is-finite - ( is-finite-coprod-symmetric-difference)) - ( transitive-mere-equiv - ( mere-equiv-has-finite-cardinality - ( has-finite-cardinality-is-finite - ( is-finite-coprod-symmetric-difference))) - ( unit-trunc-Prop - ( inv-equiv (equiv-symmetric-difference P Q))))))) ∙ + ( number-of-elements-has-finite-cardinality) + ( all-elements-equal-has-finite-cardinality + ( has-finite-cardinality-is-finite + ( is-finite-coprod + ( is-finite-type-decidable-subtype P F) + ( is-finite-type-decidable-subtype Q F))) + ( pair + ( number-of-elements-is-finite + ( is-finite-coprod-symmetric-difference)) + ( transitive-mere-equiv + ( mere-equiv-has-finite-cardinality + ( has-finite-cardinality-is-finite + ( is-finite-coprod-symmetric-difference))) + ( unit-trunc-Prop + ( inv-equiv (equiv-symmetric-difference P Q))))))) ∙ ( inv ( coprod-eq-is-finite ( is-finite-type-decidable-subtype @@ -82,9 +85,9 @@ module _ ( symmetric-difference-decidable-subtype P Q)) ( n)) ( ( inv - ( coprod-eq-is-finite - ( is-finite-intersection) - ( is-finite-intersection))) ∙ + ( coprod-eq-is-finite + ( is-finite-intersection) + ( is-finite-intersection))) ∙ ( ap ( λ n → add-ℕ diff --git a/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md b/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md index 682f160866..6c2c1e6e81 100644 --- a/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md +++ b/src/univalent-combinatorics/trivial-sigma-decompositions.lagda.md @@ -11,15 +11,10 @@ open import foundation.trivial-sigma-decompositions public open import foundation.contractible-types open import foundation.dependent-pair-types -open import foundation.empty-types -open import foundation.equivalences -open import foundation.functions -open import foundation.functoriality-propositional-truncation open import foundation.identity-types open import foundation.inhabited-types open import foundation.propositions open import foundation.subtypes -open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import univalent-combinatorics.finite-types diff --git a/src/univalent-combinatorics/type-duality.lagda.md b/src/univalent-combinatorics/type-duality.lagda.md index 954415829d..4fdfa10207 100644 --- a/src/univalent-combinatorics/type-duality.lagda.md +++ b/src/univalent-combinatorics/type-duality.lagda.md @@ -12,13 +12,10 @@ open import foundation.type-duality public open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.fibers-of-maps open import foundation.full-subtypes -open import foundation.functions open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-function-types -open import foundation.identity-types open import foundation.inhabited-types open import foundation.propositions open import foundation.structure @@ -26,7 +23,6 @@ open import foundation.surjective-maps open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice -open import foundation.univalence open import foundation.universe-levels open import univalent-combinatorics.fibers-of-maps diff --git a/src/univalent-combinatorics/unions-subtypes.lagda.md b/src/univalent-combinatorics/unions-subtypes.lagda.md index 15d516c46f..7699e3db66 100644 --- a/src/univalent-combinatorics/unions-subtypes.lagda.md +++ b/src/univalent-combinatorics/unions-subtypes.lagda.md @@ -12,7 +12,6 @@ open import foundation.unions-subtypes public open import foundation.decidable-equality open import foundation.propositional-truncations open import foundation.subtypes -open import foundation.universal-property-propositional-truncation open import foundation.universe-levels open import univalent-combinatorics.coproduct-types diff --git a/src/univalent-combinatorics/unlabeled-partitions.lagda.md b/src/univalent-combinatorics/unlabeled-partitions.lagda.md index 8fdd2cfc02..9bcf6793f4 100644 --- a/src/univalent-combinatorics/unlabeled-partitions.lagda.md +++ b/src/univalent-combinatorics/unlabeled-partitions.lagda.md @@ -4,6 +4,14 @@ module univalent-combinatorics.unlabeled-partitions where ``` +
Imports + +```agda + +``` + +
+ ## Idea Unlabeled partitions are diff --git a/src/universal-algebra/quotient-algebras.lagda.md b/src/universal-algebra/quotient-algebras.lagda.md index 22c8c2ceb6..6addaecb85 100644 --- a/src/universal-algebra/quotient-algebras.lagda.md +++ b/src/universal-algebra/quotient-algebras.lagda.md @@ -1,4 +1,4 @@ -# Quotient Algebras +# Quotient algebras ```agda module universal-algebra.quotient-algebras where @@ -11,18 +11,11 @@ open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.equivalence-classes -open import foundation.equivalence-relations open import foundation.equivalences -open import foundation.function-extensionality -open import foundation.functions open import foundation.functoriality-propositional-truncation -open import foundation.identity-types open import foundation.propositional-truncations -open import foundation.propositions -open import foundation.reflecting-maps-equivalence-relations open import foundation.set-quotients open import foundation.sets -open import foundation.unit-type open import foundation.universe-levels open import linear-algebra.vectors @@ -30,7 +23,6 @@ open import linear-algebra.vectors open import universal-algebra.algebraic-theories open import universal-algebra.algebras-of-theories open import universal-algebra.congruences -open import universal-algebra.models-of-signatures open import universal-algebra.signatures ``` diff --git a/src/universal-algebra/terms-over-signatures.lagda.md b/src/universal-algebra/terms-over-signatures.lagda.md index 01ef74c537..2aecee3a2a 100644 --- a/src/universal-algebra/terms-over-signatures.lagda.md +++ b/src/universal-algebra/terms-over-signatures.lagda.md @@ -9,9 +9,7 @@ module universal-algebra.terms-over-signatures where ```agda open import elementary-number-theory.natural-numbers -open import foundation.dependent-pair-types open import foundation.identity-types -open import foundation.sets open import foundation.universe-levels open import linear-algebra.vectors