From 071533a1c366e2da89ef3f33052933a6460a3a69 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 22 Feb 2024 18:01:24 +0100 Subject: [PATCH 01/10] Profile typechecking performance (#1031) - [X] Set up `make`-hook for profiling - [X] Set up GitHub workflow for profiling - [x] Generate pretty graphs based on profiling data - [x] Host graphs on a webpage ~I'm not yet completely sure I set up the workflow correctly.~ Also note that 4GB memory is not enough for this profiler to work (#985). Resolves #1030.
Example output ```text Total 90,422ms Miscellaneous 26,895ms category-theory.category-of-maps-from-small-to-large-categories 7,846ms everything 3,827ms synthetic-homotopy-theory.functoriality-sequential-colimits 2,399ms trees.underlying-trees-elements-coalgebras-polynomial-endofunctors 2,299ms finite-group-theory.simpson-delooping-sign-homomorphism 1,900ms category-theory.slice-precategories 1,878ms synthetic-homotopy-theory.26-id-pushout 1,728ms synthetic-homotopy-theory.universal-cover-circle 1,570ms set-theory.cumulative-hierarchy 1,560ms polytopes.abstract-polytopes 1,459ms synthetic-homotopy-theory.hatchers-acyclic-type 1,446ms trees.equivalences-enriched-directed-trees 1,164ms trees.combinator-enriched-directed-trees 1,161ms trees.underlying-trees-of-elements-of-w-types 1,143ms synthetic-homotopy-theory.acyclic-maps 1,034ms finite-group-theory.abstract-quaternion-group 1,012ms commutative-algebra.joins-radical-ideals-commutative-rings 1,006ms order-theory.galois-connections 928ms category-theory.adjunctions-large-precategories 881ms group-theory.torsors 814ms group-theory.normal-submonoids 794ms ring-theory.left-ideals-generated-by-subsets-rings 665ms commutative-algebra.euclidean-domains 586ms synthetic-homotopy-theory.sections-descent-circle 540ms trees.functoriality-combinator-directed-trees 535ms synthetic-homotopy-theory.sequential-colimits 522ms finite-group-theory.subgroups-finite-groups 509ms reflection.group-solver 506ms order-theory.nuclei-large-locales 493ms category-theory.natural-transformations-functors-from-small-to-large-categories 472ms commutative-algebra.integral-domains 465ms category-theory.adjunctions-large-categories 460ms ring-theory.localizations-rings 408ms group-theory.abelianization-groups 399ms synthetic-homotopy-theory.descent-circle-equivalence-types 380ms synthetic-homotopy-theory.dependent-pushout-products 380ms graph-theory.equivalences-enriched-undirected-graphs 369ms lists.universal-property-lists-wild-monoids 359ms category-theory.full-subcategories 355ms synthetic-homotopy-theory.descent-circle-function-types 350ms commutative-algebra.joins-ideals-commutative-rings 349ms category-theory.groupoids 343ms category-theory.function-precategories 330ms commutative-algebra.zariski-locale 307ms synthetic-homotopy-theory.interval-type 291ms trees.undirected-trees 285ms orthogonal-factorization-systems.functoriality-higher-modalities 280ms linear-algebra.vectors-on-euclidean-domains 280ms group-theory.normal-cores-subgroups 280ms synthetic-homotopy-theory.descent-circle-subtypes 278ms category-theory.opposite-preunivalent-categories 274ms group-theory.substitution-functor-group-actions 269ms finite-group-theory.cartier-delooping-sign-homomorphism 260ms structured-types.dependent-products-wild-monoids 254ms ring-theory.joins-ideals-rings 253ms category-theory.restrictions-functors-cores-precategories 253ms ring-theory.joins-left-ideals-rings 243ms commutative-algebra.function-commutative-rings 240ms set-theory.cardinalities 236ms commutative-algebra.integer-multiples-of-elements-commutative-rings 233ms synthetic-homotopy-theory.descent-circle-dependent-pair-types 232ms group-theory.normalizer-subgroups 223ms category-theory.coproducts-in-precategories 219ms category-theory.opposite-large-precategories 210ms category-theory.opposite-categories 192ms group-theory.saturated-congruence-relations-monoids 189ms group-theory 186ms ring-theory.products-left-ideals-rings 178ms lists.quicksort-lists 178ms ring-theory.products-right-ideals-rings 176ms orthogonal-factorization-systems.extensions-lifts-families-of-elements 172ms category-theory 163ms modal-type-theory.flat-sharp-adjunction 159ms category-theory.yoneda-lemma-categories 154ms category-theory.representing-arrow-category 148ms group-theory.quotient-groups-concrete-groups 146ms synthetic-homotopy-theory.powers-of-loops 140ms linear-algebra.scalar-multiplication-vectors-on-rings 132ms synthetic-homotopy-theory.coequalizers 130ms category-theory.augmented-simplex-category 124ms synthetic-homotopy-theory.1-acyclic-types 124ms ring-theory.algebras-rings 123ms higher-group-theory.iterated-cartesian-products-higher-groups 123ms group-theory.cartesian-products-abelian-groups 121ms category-theory.cores-categories 121ms orthogonal-factorization-systems.local-maps 118ms commutative-algebra.function-commutative-semirings 116ms commutative-algebra.dependent-products-commutative-semirings 114ms category-theory.representable-functors-large-precategories 112ms category-theory.split-essentially-surjective-functors-precategories 112ms ring-theory.function-semirings 111ms graph-theory.trails-undirected-graphs 110ms finite-group-theory.finite-commutative-monoids 109ms commutative-algebra.ideals-commutative-semirings 109ms trees.raising-universe-levels-directed-trees 106ms category-theory.natural-numbers-object-precategories 104ms synthetic-homotopy-theory.cocartesian-morphisms-arrows 104ms order-theory 103ms group-theory.category-of-orbits-groups 101ms category-theory.products-of-precategories 99ms category-theory.exponential-objects-precategories 98ms group-theory.category-of-group-actions 97ms organic-chemistry.alcohols 96ms synthetic-homotopy-theory.spectra 90ms group-theory.representations-monoids-precategories 88ms category-theory.homotopies-natural-transformations-large-precategories 88ms structured-types.function-wild-monoids 87ms real-numbers.dedekind-real-numbers 83ms graph-theory.faithful-morphisms-undirected-graphs 83ms structured-types.pointed-universal-property-contractible-types 81ms synthetic-homotopy-theory 80ms ring-theory 79ms orthogonal-factorization-systems.factorization-operations-global-function-classes 79ms group-theory.function-abelian-groups 77ms graph-theory.raising-universe-levels-directed-graphs 77ms order-theory.accessible-elements-relations 77ms order-theory.chains-preorders 76ms category-theory.essentially-surjective-functors-precategories 74ms commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings 74ms orthogonal-factorization-systems.functoriality-pullback-hom 72ms modal-type-theory.flat-dependent-pair-types 72ms synthetic-homotopy-theory.tangent-spheres 72ms group-theory.kernels-homomorphisms-concrete-groups 71ms order-theory.chains-posets 68ms ring-theory.precategory-of-semirings 65ms graph-theory.complete-bipartite-graphs 64ms ring-theory.quotient-rings 64ms commutative-algebra 63ms group-theory.cayleys-theorem 63ms synthetic-homotopy-theory.premanifolds 61ms category-theory.monomorphisms-in-large-precategories 61ms category-theory.initial-objects-precategories 60ms group-theory.intersections-subgroups-abelian-groups 58ms group-theory.inverse-semigroups 57ms commutative-algebra.multiples-of-elements-commutative-rings 53ms modal-type-theory.flat-discrete-types 53ms order-theory.well-founded-relations 52ms trees 52ms group-theory.centers-monoids 51ms category-theory.sieves-in-categories 50ms trees.rooted-undirected-trees 50ms organic-chemistry.methane 50ms order-theory.maximal-chains-posets 50ms order-theory.maximal-chains-preorders 50ms synthetic-homotopy-theory.acyclic-types 50ms category-theory.endomorphisms-in-categories 49ms group-theory.centers-semigroups 48ms group-theory.precategory-of-concrete-groups 47ms group-theory.monomorphisms-groups 46ms orthogonal-factorization-systems 45ms structured-types.finite-multiplication-magmas 43ms group-theory.function-monoids 43ms higher-group-theory.subgroups-higher-groups 41ms orthogonal-factorization-systems.local-families-of-types 40ms commutative-algebra.local-commutative-rings 39ms category-theory.representable-functors-categories 39ms synthetic-homotopy-theory.descent-circle-constant-families 39ms structured-types.cyclic-types 37ms trees.bounded-multisets 36ms orthogonal-factorization-systems.lifting-operations 36ms group-theory.precategory-of-commutative-monoids 36ms commutative-algebra.trivial-commutative-rings 35ms order-theory.lower-types-preorders 35ms group-theory.conjugation-concrete-groups 34ms graph-theory.paths-undirected-graphs 34ms ring-theory.invariant-basis-property-rings 32ms order-theory.well-founded-orders 31ms group-theory.monomorphisms-concrete-groups 31ms structured-types 31ms linear-algebra.diagonal-matrices-on-rings 30ms category-theory.essential-fibers-of-functors-precategories 30ms graph-theory 30ms group-theory.function-semigroups 30ms group-theory.transitive-group-actions 29ms group-theory.orbit-stabilizer-theorem-concrete-groups 29ms trees.empty-multisets 28ms group-theory.concrete-monoids 28ms ring-theory.radical-ideals-rings 27ms group-theory.products-of-tuples-of-elements-commutative-monoids 27ms group-theory.perfect-subgroups 26ms graph-theory.trails-directed-graphs 26ms finite-group-theory 25ms category-theory.equivalences-of-large-precategories 25ms graph-theory.vertex-covers 25ms group-theory.elements-of-finite-order-groups 25ms order-theory.directed-complete-posets 25ms graph-theory.eulerian-circuits-undirected-graphs 25ms group-theory.exponents-groups 24ms graph-theory.regular-undirected-graphs 24ms order-theory.locally-finite-posets 24ms order-theory.precategory-of-decidable-total-orders 24ms orthogonal-factorization-systems.identity-modality 24ms graph-theory.voltage-graphs 23ms finite-group-theory.alternating-groups 23ms finite-group-theory.alternating-concrete-groups 23ms order-theory.precategory-of-finite-posets 23ms modal-type-theory.sharp-codiscrete-maps 23ms orthogonal-factorization-systems.raise-modalities 22ms group-theory.mere-equivalences-group-actions 22ms reflection.boolean-reflection 21ms synthetic-homotopy-theory.mere-spheres 21ms ring-theory.characteristics-rings 21ms synthetic-homotopy-theory.morphisms-descent-data-circle 21ms group-theory.furstenberg-groups 20ms structured-types.morphisms-magmas 20ms order-theory.ideals-preorders 20ms group-theory.principal-group-actions 20ms trees.coalgebra-of-enriched-directed-trees 19ms order-theory.interval-subposets 19ms group-theory.sheargroups 19ms ring-theory.free-rings-with-one-generator 19ms trees.planar-binary-trees 18ms group-theory.normal-subgroups-concrete-groups 18ms structured-types.fibers-of-pointed-maps 18ms modal-type-theory.crisp-identity-types 18ms group-theory.dihedral-groups 17ms organic-chemistry.alkynes 17ms group-theory.exponents-abelian-groups 17ms group-theory.perfect-cores 17ms set-theory.infinite-sets 17ms group-theory.perfect-groups 17ms group-theory.orbits-group-actions 17ms orthogonal-factorization-systems.zero-modality 16ms synthetic-homotopy-theory.sequentially-compact-types 16ms group-theory.stabilizer-groups 16ms trees.coalgebra-of-directed-trees 15ms structured-types.contractible-pointed-types 15ms orthogonal-factorization-systems.separated-types 15ms trees.rooted-quasitrees 15ms ring-theory.generating-elements-rings 14ms graph-theory.hypergraphs 14ms set-theory.cantor-space 14ms orthogonal-factorization-systems.sigma-closed-modalities 14ms commutative-algebra.boolean-rings 13ms linear-algebra 13ms synthetic-homotopy-theory.join-powers-of-types 13ms lists 13ms graph-theory.directed-graph-structures-on-standard-finite-sets 12ms orthogonal-factorization-systems.sigma-closed-reflective-modalities 12ms reflection 11ms trees.multiset-indexed-dependent-products-of-types 11ms graph-theory.closed-walks-undirected-graphs 11ms higher-group-theory 10ms synthetic-homotopy-theory.category-of-connected-set-bundles-circle 10ms group-theory.isomorphisms-concrete-groups 10ms linear-algebra.scalar-multiplication-matrices 10ms graph-theory.acyclic-undirected-graphs 10ms 209,027,633,416 bytes allocated in the heap 20,208,785,744 bytes copied during GC 1,709,639,904 bytes maximum residency (28 sample(s)) 2,508,576 bytes maximum slop 3121 MiB total memory in use (0 MiB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 48930 colls, 0 par 18.386s 19.088s 0.0004s 0.0485s Gen 1 28 colls, 0 par 0.691s 1.009s 0.0360s 0.2568s TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1) SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled) INIT time 0.001s ( 0.001s elapsed) MUT time 71.440s ( 71.424s elapsed) GC time 19.077s ( 20.097s elapsed) EXIT time 0.210s ( 0.002s elapsed) Total time 90.727s ( 91.525s elapsed) Alloc rate 2,925,929,451 bytes per MUT second Productivity 78.7% of total user, 78.0% of total elapsed ```
--------- Co-authored-by: VojtechStep --- .github/workflows/ci.yaml | 2 +- .github/workflows/clean-up.yaml | 2 +- .github/workflows/pages.yaml | 2 +- .github/workflows/profiling.yaml | 76 +++++++ .gitignore | 1 + Makefile | 7 +- scripts/typechecking_profile_parser.py | 135 ++++++++++++ website/benchmarks/index.html | 281 +++++++++++++++++++++++++ 8 files changed, 502 insertions(+), 4 deletions(-) create mode 100644 .github/workflows/profiling.yaml create mode 100644 scripts/typechecking_profile_parser.py create mode 100644 website/benchmarks/index.html diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 1799f381a9..94db54052b 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -54,7 +54,7 @@ jobs: ${{ runner.os }}-check-${{ github.ref }}-${{ matrix.agda }}- ${{ runner.os }}-check-refs/heads/master-${{ matrix.agda }}- - - name: Typecheck the whole formalization + - name: Typecheck library run: | cd master make check diff --git a/.github/workflows/clean-up.yaml b/.github/workflows/clean-up.yaml index d1905234d0..6ed7f6058c 100644 --- a/.github/workflows/clean-up.yaml +++ b/.github/workflows/clean-up.yaml @@ -1,4 +1,4 @@ -name: cleanup caches generated by pull requests +name: Clean up caches generated by pull requests on: pull_request: types: diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml index ef2bb396f3..0f1cefe472 100644 --- a/.github/workflows/pages.yaml +++ b/.github/workflows/pages.yaml @@ -1,4 +1,4 @@ -name: Formalization website +name: Build and deploy library website on: # To run this workflow manually workflow_dispatch: diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml new file mode 100644 index 0000000000..c1238dd53d --- /dev/null +++ b/.github/workflows/profiling.yaml @@ -0,0 +1,76 @@ +name: Profile library typechecking +on: + push: + branches: + - master + +# Don't cancel previous runs of the same branch +concurrency: + group: '${{ github.workflow }}' + cancel-in-progress: false + +jobs: + typecheck-performance: + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest] + agda: ['2.6.4'] + steps: + - name: Checkout our repository + uses: actions/checkout@v3 + with: + path: master + + - name: Setup Agda + uses: wenkokke/setup-agda@v2.1.0 + with: + agda-version: ${{ matrix.agda }} + + - name: Typecheck library with profiling + run: | + cd master + make check-profile 2> temp/memory-results.txt | tee temp/benchmark-results.txt + + - name: Download previous typechecking profile + run: | + mkdir benchmark-cache + curl 'https://agda-unimath-benchmarks.netlify.app/data.json' -o benchmark-cache/data.json + # Stop if there is no initial data (the server gave us an HTML instead of a JSON) + (head -1 benchmark-cache/data.json | grep -v DOCTYPE) || (rm benchmark-cache/data.json; exit 0) + curl 'https://agda-unimath-benchmarks.netlify.app/data.csv' -o benchmark-cache/data.csv + + - name: Process new profiling data + run: | + cd master + python3 scripts/typechecking_profile_parser.py \ + temp/benchmark-results.txt temp/memory-results.txt \ + temp/benchmark-results.json benchmark-cache/data.csv \ + ${{ github.sha }} + + - name: Merge JSON profiling data + uses: rhysd/github-action-benchmark@v1 + with: + tool: 'customSmallerIsBetter' + # Location of the new data + output-file-path: './master/temp/benchmark-results.json' + # Location of the aggregate data + external-data-json-path: './benchmark-cache/data.json' + + - name: Publish the profiling CSV as an artifact + uses: actions/upload-artifact@v4 + with: + name: 'Library profiling history' + path: './benchmark-cache/data.csv' + + - name: Prepare new revision of the profiling website + run: | + cd master + mkdir benchmark-website + cp website/benchmarks/index.html benchmark-website/ + cp ../benchmark-cache/data.* benchmark-website/ + echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json >benchmark-website/data.js + + - name: Deploy the new profiling website + run: | + npx netlify-cli deploy --dir=benchmark-website diff --git a/.gitignore b/.gitignore index ffbeeca2cb..7a4e564e4c 100644 --- a/.gitignore +++ b/.gitignore @@ -423,6 +423,7 @@ package-lock.json docs/ html/ book/ +temp/ src/temp/ src/everything.lagda.md SUMMARY.md diff --git a/Makefile b/Makefile index e2ed2f507d..91e96b4c5c 100644 --- a/Makefile +++ b/Makefile @@ -7,7 +7,7 @@ everythingOpts := --guardedness --cohesion --flat-split # use "$ export AGDAVERBOSE=-v20" if you want to see all AGDAVERBOSE ?= -v1 -AGDARTS := +RTS -M4.0G -RTS +AGDARTS := +RTS -M6.0G -RTS AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print) CONTRIBUTORS_FILE := CONTRIBUTORS.toml @@ -20,6 +20,7 @@ CONTRIBUTORS_FILE := CONTRIBUTORS.toml # at is at least in a proper code block with syntax highlighting, albeit without # the agda-unimath chrome. AGDAHTMLFLAGS ?= --html --html-highlight=auto --html-dir=docs --css=website/css/Agda.css --only-scope-checking +AGDAPROFILEFLAGS ?= --profile=modules +RTS -s -RTS AGDA ?= agda $(AGDAVERBOSE) $(AGDARTS) TIME ?= time @@ -70,6 +71,10 @@ src/everything.lagda.md: agdaFiles check: ./src/everything.lagda.md ${TIME} ${AGDA} $? +.PHONY: check-profile +check-profile: ./src/everything.lagda.md + ${AGDA} ${AGDAPROFILEFLAGS} $? + agda-html: ./src/everything.lagda.md @rm -rf ./docs/ @mkdir -p ./docs/ diff --git a/scripts/typechecking_profile_parser.py b/scripts/typechecking_profile_parser.py new file mode 100644 index 0000000000..6291b9ca8b --- /dev/null +++ b/scripts/typechecking_profile_parser.py @@ -0,0 +1,135 @@ +import json +import re +import argparse +import csv + + +def parse_memory_profiling_data(filepath): + results = dict() + + # Define patterns to match each line and their corresponding unit + patterns = { + "memory_allocated_in_heap": (r"(\d+(?:,\d+)*) bytes allocated in the heap", "B"), + "memory_copied_during_GC": (r"(\d+(?:,\d+)*) bytes copied during GC", "B"), + "maximum_residency": (r"(\d+(?:,\d+)*) bytes maximum residency", "B"), + "memory_maximum_slop": (r"(\d+(?:,\d+)*) bytes maximum slop", "B"), + "total_memory_in_use": (r"(\d+) MiB total memory in use", "MiB") + } + + with open(filepath, 'r') as file: + for line in file: + for key, (pattern, unit) in patterns.items(): + match = re.search(pattern, line) + if match: + value = int(match.group(1).replace(",", "")) + if key == "memory_maximum_slop": # Convert maximum slo to KiB and truncate + value //= 1024 + unit = "KiB" + elif unit == "B": # Convert bytes to MiB and truncate + value //= 1024 * 1024 + unit = "MiB" + results[key] = {"value": value, "unit": unit} + + return results + +def parse_benchmark_results(input_path): + benchmarks = dict() + with open(input_path, 'r') as file: + for line in file: + # Match lines that end with "ms" indicating a timing result + match = re.fullmatch(r'^\s*(\S+)\s+(\d+(?:,\d+)*)ms\s*$', line) + if match: + name = match.group(1).strip() + # Correctly parse and combine the number groups to handle commas in numbers + milliseconds = int(match.group(2).replace(',','')) + benchmarks[name] = {'value': milliseconds, 'unit':'ms'} + return benchmarks + + +def subdict(original_dict, keys_to_extract): + if keys_to_extract is None: + return original_dict + else: + return {key: original_dict[key] for key in keys_to_extract if key in original_dict} + +def convert_dict_to_list(data, keys_to_extract=None): + return [{'name': name, **details} for name, details in subdict(data, keys_to_extract).items()] + +def save_github_action_benchmark_json(output_path, benchmarks, memory_stats, benchmark_keys, memory_keys): + with open(output_path, 'w') as file: + json.dump(convert_dict_to_list(benchmarks, benchmark_keys) + convert_dict_to_list(memory_stats, memory_keys) , file, indent=2) + +def read_existing_csv_to_dict(csv_path, commit_hash): + # Initialize a dictionary to hold the CSV data + data_dict = {} + fieldnames = ['name', 'unit', commit_hash] + + try: + # Attempt to open the file, which will fail if the file doesn't exist + with open(csv_path, mode='r', newline='') as csvfile: + reader = csv.DictReader(csvfile) + # Update fieldnames with those found in the existing CSV, plus the new commit hash if necessary + fieldnames = reader.fieldnames + [commit_hash] if commit_hash not in reader.fieldnames else reader.fieldnames + for row in reader: + data_dict[row['name']] = row + except FileNotFoundError: + # File doesn't exist, proceed without modifying data_dict or fieldnames + pass + + return data_dict, fieldnames + +def update_csv_data(data_dict, benchmarks, memory_stats, commit_hash): + # Combine benchmarks and memory stats for easier processing + combined_data = {**memory_stats, **benchmarks} + + # Update the data_dict with new or updated values + for name, details in combined_data.items(): + if name not in data_dict: + data_dict[name] = {'name': name, 'unit': details['unit']} + data_dict[name][commit_hash] = int(details['value']) + +def write_csv_from_dict(csv_path, data_dict, fieldnames, commit_hash): + def custom_sort(item): + # Sort all items that do not have unit "ms" first, then sort based on whether the name is capitalized, and then based on worst newest benchmark + is_not_ms_unit = item['unit'] != "ms" + + if is_not_ms_unit: + # If the unit is not `ms`, preserve order + return (False, False, 0) + else: + # If the unit is `ms`, sort based on capitalization, then on newest benchmark + return (True , item['name'][0].islower(), 0 if commit_hash not in item.keys() else -item[commit_hash]) + + + + with open(csv_path, mode='w', newline='') as csvfile: + writer = csv.DictWriter(csvfile, fieldnames=fieldnames) + writer.writeheader() + # Sort the data based on the custom sort function before writing + sorted_data = sorted(data_dict.values(), key=custom_sort) + for row in sorted_data: + writer.writerow(row) + +def save_as_csv(benchmarks, memory_stats, csv_path, commit_hash): + data_dict, fieldnames = read_existing_csv_to_dict(csv_path, commit_hash) + update_csv_data(data_dict, benchmarks, memory_stats, commit_hash) + write_csv_from_dict(csv_path, data_dict, fieldnames, commit_hash) + +if __name__ == "__main__": + # Set up argument parsing + parser = argparse.ArgumentParser(description='Convert benchmark results to JSON format.') + parser.add_argument('input_times_path', help='Path to the input file containing typechecking times.') + parser.add_argument('input_memory_path', help='Path to the input file containing memory statistics.') + parser.add_argument('output_json_path', help='Path to the output JSON file.') + parser.add_argument('csv_path', help='Path to the profiling CSV file.') + parser.add_argument('commit_hash', help='Commit hash for current commit.') + + # Parse arguments from command line + args = parser.parse_args() + + # Use the provided command-line arguments + benchmarks = parse_benchmark_results(args.input_times_path) + memory_stats = parse_memory_profiling_data(args.input_memory_path) + + save_github_action_benchmark_json(args.output_json_path, benchmarks, memory_stats, ["Total",], ["total_memory_in_use",]) + save_as_csv(benchmarks, memory_stats, args.csv_path, args.commit_hash) diff --git a/website/benchmarks/index.html b/website/benchmarks/index.html new file mode 100644 index 0000000000..6c887805e8 --- /dev/null +++ b/website/benchmarks/index.html @@ -0,0 +1,281 @@ + + + + + + + Benchmarks + + + + +
+ + + + + + + From b8bcd7e415005299cf67aeb58e0cff8a8803643d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 22 Feb 2024 18:06:13 +0100 Subject: [PATCH 02/10] Bugfix profiling workflow - `mkdir temp` (#1036) --- .github/workflows/profiling.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index c1238dd53d..abac88c9ee 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -30,6 +30,7 @@ jobs: - name: Typecheck library with profiling run: | cd master + mkdir temp make check-profile 2> temp/memory-results.txt | tee temp/benchmark-results.txt - name: Download previous typechecking profile From d4d3e8b4f1736defdbb913d666fb7dee5c01e904 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Thu, 22 Feb 2024 18:33:13 +0100 Subject: [PATCH 03/10] Fixups for the profiling workflow (#1037) #1031 --- .github/workflows/profiling.yaml | 2 +- website/benchmarks/index.html | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index abac88c9ee..6c59fcdb14 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -46,7 +46,7 @@ jobs: cd master python3 scripts/typechecking_profile_parser.py \ temp/benchmark-results.txt temp/memory-results.txt \ - temp/benchmark-results.json benchmark-cache/data.csv \ + temp/benchmark-results.json ../benchmark-cache/data.csv \ ${{ github.sha }} - name: Merge JSON profiling data diff --git a/website/benchmarks/index.html b/website/benchmarks/index.html index 6c887805e8..eb3f31ca72 100644 --- a/website/benchmarks/index.html +++ b/website/benchmarks/index.html @@ -214,7 +214,7 @@ afterTitle: items => { const {index} = items[0]; const data = dataset[index]; - return '\n' + data.commit.message + '\n\n' + data.commit.timestamp + ' committed by @' + data.commit.committer.username + '\n'; + return '\n' + data.commit.message + '\n\n' + data.commit.timestamp + '\n'; }, label: item => { let label = item.value; From 45c7fd842bd2437e831d46c31fe1ffa147f9177a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 22 Feb 2024 18:52:31 +0100 Subject: [PATCH 04/10] Another fix for the profiling workflow (#1038) --- .github/workflows/profiling.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 6c59fcdb14..d323f1be5a 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -38,7 +38,7 @@ jobs: mkdir benchmark-cache curl 'https://agda-unimath-benchmarks.netlify.app/data.json' -o benchmark-cache/data.json # Stop if there is no initial data (the server gave us an HTML instead of a JSON) - (head -1 benchmark-cache/data.json | grep -v DOCTYPE) || (rm benchmark-cache/data.json; exit 0) + (head -1 benchmark-cache/data.json | grep -v DOCTYPE) || {rm benchmark-cache/data.json; exit 0} curl 'https://agda-unimath-benchmarks.netlify.app/data.csv' -o benchmark-cache/data.csv - name: Process new profiling data From f7b5f91c6b3ac65313b0fb746a1ede049110b388 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 22 Feb 2024 22:13:18 +0100 Subject: [PATCH 05/10] Another fix to the profiling workflow (#1039) #1030 --- .github/workflows/profiling.yaml | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index d323f1be5a..6f2beafcd0 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -1,12 +1,12 @@ -name: Profile library typechecking +name: Profile Library Typechecking + on: push: branches: - master -# Don't cancel previous runs of the same branch concurrency: - group: '${{ github.workflow }}' + group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: false jobs: @@ -16,11 +16,12 @@ jobs: matrix: os: [ubuntu-latest] agda: ['2.6.4'] + steps: - name: Checkout our repository uses: actions/checkout@v3 with: - path: master + path: repo - name: Setup Agda uses: wenkokke/setup-agda@v2.1.0 @@ -29,21 +30,21 @@ jobs: - name: Typecheck library with profiling run: | - cd master - mkdir temp + cd repo + mkdir -p temp make check-profile 2> temp/memory-results.txt | tee temp/benchmark-results.txt - name: Download previous typechecking profile run: | - mkdir benchmark-cache + mkdir -p benchmark-cache curl 'https://agda-unimath-benchmarks.netlify.app/data.json' -o benchmark-cache/data.json # Stop if there is no initial data (the server gave us an HTML instead of a JSON) - (head -1 benchmark-cache/data.json | grep -v DOCTYPE) || {rm benchmark-cache/data.json; exit 0} + (head -1 benchmark-cache/data.json | grep -v DOCTYPE) || { rm benchmark-cache/data.json; exit 0; } curl 'https://agda-unimath-benchmarks.netlify.app/data.csv' -o benchmark-cache/data.csv - name: Process new profiling data run: | - cd master + cd repo python3 scripts/typechecking_profile_parser.py \ temp/benchmark-results.txt temp/memory-results.txt \ temp/benchmark-results.json ../benchmark-cache/data.csv \ @@ -54,7 +55,7 @@ jobs: with: tool: 'customSmallerIsBetter' # Location of the new data - output-file-path: './master/temp/benchmark-results.json' + output-file-path: './repo/temp/benchmark-results.json' # Location of the aggregate data external-data-json-path: './benchmark-cache/data.json' @@ -66,11 +67,11 @@ jobs: - name: Prepare new revision of the profiling website run: | - cd master - mkdir benchmark-website + cd repo + mkdir -p benchmark-website cp website/benchmarks/index.html benchmark-website/ cp ../benchmark-cache/data.* benchmark-website/ - echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json >benchmark-website/data.js + echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js - name: Deploy the new profiling website run: | From 18bc065f458e2182eef9b0616698b6d7ceffafa0 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 23 Feb 2024 11:43:06 +0100 Subject: [PATCH 06/10] Infinitely and finitely coherent equivalences and infinitely and finitely coherently invertible maps (#1028) This PR is part of the diploma project of @maybemabeline. We add some new definitions to the library, and we found some ways to express infinite coherence. --------- Co-authored-by: maybemabeline --- src/foundation-core/equivalences.lagda.md | 6 + src/foundation.lagda.md | 9 + src/foundation/equivalences.lagda.md | 6 + .../finitely-coherent-equivalences.lagda.md | 86 +++++ ...nitely-coherently-invertible-maps.lagda.md | 91 +++++ .../infinitely-coherent-equivalences.lagda.md | 362 ++++++++++++++++++ src/foundation/retractions.lagda.md | 58 --- src/foundation/sections.lagda.md | 57 --- ...tal-concatenation-identifications.lagda.md | 6 +- ...dentifications-along-equivalences.lagda.md | 4 + ...identifications-along-retractions.lagda.md | 111 ++++++ ...on-identifications-along-sections.lagda.md | 109 ++++++ src/group-theory/conjugation.lagda.md | 10 +- 13 files changed, 793 insertions(+), 122 deletions(-) create mode 100644 src/foundation/finitely-coherent-equivalences.lagda.md create mode 100644 src/foundation/finitely-coherently-invertible-maps.lagda.md create mode 100644 src/foundation/infinitely-coherent-equivalences.lagda.md create mode 100644 src/foundation/transposition-identifications-along-retractions.lagda.md create mode 100644 src/foundation/transposition-identifications-along-sections.lagda.md diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index 843b2ae090..7cbf23c397 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -748,6 +748,12 @@ syntax step-equivalence-reasoning e Z f = e ≃ Z by f [`foundation.contractible-maps`](foundation.contractible-maps.md). - For the notion of path-split maps see [`foundation.path-split-maps`](foundation.path-split-maps.md). +- For the notion of finitely coherent equivalence, see + [`foundation.finitely-coherent-equivalence`)(foundation.finitely-coherent-equivalence.md). +- For the notion of finitely coherently invertible map, see + [`foundation.finitely-coherently-invertible-map`)(foundation.finitely-coherently-invertible-map.md). +- For the notion of infinitely coherent equivalence, see + [`foundation.infinitely-coherent-equivalences`](foundation.infinitely-coherent-equivalences.md). ### Table of files about function types, composition, and equivalences diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 00cfe1d5a0..827eff16f9 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -1,5 +1,9 @@ # Foundation +```agda +{-# OPTIONS --guardedness #-} +``` + ## Files in the foundation folder ```agda @@ -161,6 +165,8 @@ open import foundation.fibered-equivalences public open import foundation.fibered-involutions public open import foundation.fibered-maps public open import foundation.fibers-of-maps public +open import foundation.finitely-coherent-equivalences public +open import foundation.finitely-coherently-invertible-maps public open import foundation.full-subtypes public open import foundation.function-extensionality public open import foundation.function-types public @@ -195,6 +201,7 @@ open import foundation.implicit-function-types public open import foundation.impredicative-encodings public open import foundation.impredicative-universes public open import foundation.induction-principle-propositional-truncation public +open import foundation.infinitely-coherent-equivalences public open import foundation.inhabited-subtypes public open import foundation.inhabited-types public open import foundation.injective-maps public @@ -363,6 +370,8 @@ open import foundation.transport-along-homotopies public open import foundation.transport-along-identifications public open import foundation.transport-split-type-families public open import foundation.transposition-identifications-along-equivalences public +open import foundation.transposition-identifications-along-retractions public +open import foundation.transposition-identifications-along-sections public open import foundation.transposition-span-diagrams public open import foundation.trivial-relaxed-sigma-decompositions public open import foundation.trivial-sigma-decompositions public diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index 9ebb42a77a..e589682754 100644 --- a/src/foundation/equivalences.lagda.md +++ b/src/foundation/equivalences.lagda.md @@ -615,6 +615,12 @@ module _ [`foundation.contractible-maps`](foundation.contractible-maps.md). - For the notion of path-split maps see [`foundation.path-split-maps`](foundation.path-split-maps.md). +- For the notion of finitely coherent equivalence, see + [`foundation.finitely-coherent-equivalence`)(foundation.finitely-coherent-equivalence.md). +- For the notion of finitely coherently invertible map, see + [`foundation.finitely-coherently-invertible-map`)(foundation.finitely-coherently-invertible-map.md). +- For the notion of infinitely coherent equivalence, see + [`foundation.infinitely-coherent-equivalences`](foundation.infinitely-coherent-equivalences.md). ### Table of files about function types, composition, and equivalences diff --git a/src/foundation/finitely-coherent-equivalences.lagda.md b/src/foundation/finitely-coherent-equivalences.lagda.md new file mode 100644 index 0000000000..ad8dcd5167 --- /dev/null +++ b/src/foundation/finitely-coherent-equivalences.lagda.md @@ -0,0 +1,86 @@ +# Finitely coherent equivalences + +```agda +module foundation.finitely-coherent-equivalences where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.identity-types +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +The condition of being a +{{#concept "finitely coherent equivalence" Agda=is-finitely-coherent-equivalence}} +is introduced by induction on the +[natural numbers](elementary-number-theory.natural-numbers.md). In the base +case, we say that any map `f : A → B` is a +{{#concept "`0`-coherent equivalence" Agda=is-finitely-coherent-equivalence}}. +Recursively, we say that a map `f : A → B` is an +{{#concept "`n + 1`-coherent equivalence" Agda=is-finitely-coherent-equivalence}} +if it comes equipped with a map `g : B → A` and a family of maps + +```text + r x y : (f x ＝ y) → (x ＝ g y) +``` + +indexed by `x : A` and `y : B`, such that each `r x y` is an `n`-coherent +equivalence. + +By the equivalence of [retracting homotopies](foundation-core.retractions.md) +and +[transposition operations of identifications](foundation.transposition-identifications-along-retractions.md) +it therefore follows that a `1`-coherent equivalence is equivalently described +as a map equipped with a retraction. A `2`-coherent equivalence is a map +`f : A → B` equipped with `g : B → A` and for each `x : A` and `y : B` a map +`r x y : (f x ＝ y) → (x ＝ g y)`, equipped with + +```text + s x y : (x ＝ g y) → (f x ＝ y) +``` + +and for each `p : f x ＝ y` and `q : x ＝ g y` a map + +```text + t p q : (r x y p ＝ q) → (p ＝ s x y q). +``` + +This data is equivalent to the data of a +[coherently invertible map](foundation-core.coherently-invertible-maps.md) + +```text + r : (x : A) → g (f x) ＝ x + s : (y : B) → f (g y) ＝ y + t : (x : A) → ap f (r x) ＝ s (f x). +``` + +The condition of being an `n`-coherent equivalence is a +[proposition](foundation-core.propositions.md) for each `n ≥ 2`, and this +proposition is equivalent to being an equivalence. + +## Definitions + +### The predicate of being an `n`-coherent equivalence + +```agda +data + is-finitely-coherent-equivalence + {l1 l2 : Level} {A : UU l1} {B : UU l2} : + (n : ℕ) (f : A → B) → UU (l1 ⊔ l2) + where + is-zero-coherent-equivalence : + (f : A → B) → is-finitely-coherent-equivalence 0 f + is-succ-coherent-equivalence : + (n : ℕ) + (f : A → B) (g : B → A) (H : (x : A) (y : B) → (f x ＝ y) → (x ＝ g y)) → + ((x : A) (y : B) → is-finitely-coherent-equivalence n (H x y)) → + is-finitely-coherent-equivalence (succ-ℕ n) f +``` diff --git a/src/foundation/finitely-coherently-invertible-maps.lagda.md b/src/foundation/finitely-coherently-invertible-maps.lagda.md new file mode 100644 index 0000000000..a48d827c1e --- /dev/null +++ b/src/foundation/finitely-coherently-invertible-maps.lagda.md @@ -0,0 +1,91 @@ +# Finitely coherently invertible maps + +```agda +module foundation.finitely-coherently-invertible-maps where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.identity-types +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +We introduce the concept of being a +{{#concept "finitely coherently invertible map" Agda=is-finitely-coherently-invertible}} +by induction on the +[natural numbers](elementary-number-theory.natural-numbers.md). In the base +case, we say that a map `f : A → B` is a +{{#concept "`0`-coherently invertible map" Agda=is-finitely-coherently-invertible}} +if it comes equipped with a map `g : B → A`. Recursively, we say that a map +`f : A → B` is an +{{#concept "`n + 1`-coherently invertible map" Agda=is-finitely-coherently-invertible}} +if it comes equipped with map `g : B → A` and a family of maps + +```text + r x y : (f x ＝ y) → (x ＝ g y) +``` + +indexed by `x : A` and `y : B`, such that each `r x y` is `n`-coherently +invertible. + +A `1`-coherently invertible map `f : A → B` is therefore equivalently described +as a map equipped with an inverse `g : B → A` which is simultaneously a +[retraction](foundation-core.retractions.md) and a +[section](foundation-core.sections.md) of `f`. In other words, a `1`-coherently +invertible map is just an [invertible map](foundation-core.invertible-maps.md). + +A `2`-coherently invertible map `f : A → B` comes equipped with `g : B → A` and +for each `x : A` and `y : B` two maps + +```text + r : (f x ＝ y) → (x ＝ g y) + s : (x ＝ g y) → (f x ＝ y) +``` + +and for each `p : f x ＝ y` and `q : x ＝ g y` a map + +```text + t p q : (r p ＝ q) → (p ＝ s q) + u p q : (p ＝ s q) → (r p ＝ q). +``` + +This data is equivalent to the data of + +```text + r : (x : A) → g (f x) ＝ x + s : (y : B) → f (g y) ＝ y + t : (x : A) → ap f (r x) ＝ s (f x) + u : (y : B) → ap g (s y) ＝ r (f y). +``` + +The condition of being a `n`-coherently invertible map is not a +[proposition](foundation-core.propositions.md) for any `n`. In fact, for `n ≥ 1` +the type of all `n`-coherently invertible maps in a universe `𝒰` is equivalent +to the type of maps `sphere (n + 1) → 𝒰` of `n + 1`-spheres in the universe `𝒰`. + +## Definitions + +### The predicate of being an `n`-coherently invertible map + +```agda +data + is-finitely-coherently-invertible + {l1 l2 : Level} {A : UU l1} {B : UU l2} : + (n : ℕ) (f : A → B) → UU (l1 ⊔ l2) + where + is-zero-coherently-invertible : + (f : A → B) → (B → A) → is-finitely-coherently-invertible 0 f + is-succ-coherently-invertible : + (n : ℕ) + (f : A → B) (g : B → A) (H : (x : A) (y : B) → (f x ＝ y) → (x ＝ g y)) → + ((x : A) (y : B) → is-finitely-coherently-invertible n (H x y)) → + is-finitely-coherently-invertible (succ-ℕ n) f +``` diff --git a/src/foundation/infinitely-coherent-equivalences.lagda.md b/src/foundation/infinitely-coherent-equivalences.lagda.md new file mode 100644 index 0000000000..a650beffa9 --- /dev/null +++ b/src/foundation/infinitely-coherent-equivalences.lagda.md @@ -0,0 +1,362 @@ +# Infinitely coherent equivalences + +```agda +{-# OPTIONS --guardedness --lossy-unification #-} + +module foundation.infinitely-coherent-equivalences where +``` + +
Imports + +```agda +open import foundation.commuting-triangles-of-maps +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.transposition-identifications-along-equivalences +open import foundation.universe-levels +``` + +
+ +## Idea + +An {{#concept "infinitely coherent equivalence" Agda=_≃∞_}} `e : A ≃∞ B` from +`A` to `B` consists of maps + +```text + f : A → B + g : B → A +``` + +and for each `x : A` and `y : B` an infinitely coherent equivalence + +```text + ∞-equiv-transpose-eq-∞-equiv : (f x ＝ y) ≃∞ (x ＝ g y). +``` + +Since this definition is infinite, it follows that for any `x : A` and `y : B` +we have maps + +```text + f' : (f x ＝ y) → (x ＝ g y) + g' : (x ＝ g y) → (f x ＝ y) +``` + +and for each `p : f x ＝ y` and `q : g y ＝ x` an infinitely coherent +equivalence + +```text +∞-equiv-transpose-eq-∞-equiv : (f' p ＝ q) ≃∞ (p ＝ g' q). +``` + +In particular, we have identifications + +```text + inv (f' x (f x) refl) : x = g (f x) + g' y (g y) refl : f (g y) ＝ y, +``` + +which are the usual homotopies witnessing that `g` is a retraction and a section +of `f`. By infinitely imposing the structure of a coherent equivalence, we have +stated an infinite hierarchy of coherence conditions. In other words, the +infinite condition on infinitely coherent equivalences is a way of stating +infinite coherence for equivalences. + +Being an infinitely coherent equivalence is an inverse sequential limit of the +diagram + +```text + ... ---> is-finitely-coherent-equivalence 1 f ---> is-finitely-coherent-equivalence 0 f. +``` + +## Definitions + +### The predicate of being an infinitely coherent equivalence + +```agda +record is-∞-equiv + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) : UU (l1 ⊔ l2) + where + coinductive + field + map-inv-is-∞-equiv : B → A + map-transpose-is-∞-equiv : + (x : A) (y : B) → f x ＝ y → x ＝ map-inv-is-∞-equiv y + is-∞-equiv-map-transpose-is-∞-equiv : + (x : A) (y : B) → is-∞-equiv (map-transpose-is-∞-equiv x y) + +open is-∞-equiv public +``` + +### Infinitely coherent equivalences + +```agda +record + ∞-equiv + {l1 l2 : Level} (A : UU l1) (B : UU l2) : UU (l1 ⊔ l2) + where + coinductive + field + map-∞-equiv : A → B + map-inv-∞-equiv : B → A + ∞-equiv-transpose-eq-∞-equiv : + (x : A) (y : B) → ∞-equiv (map-∞-equiv x ＝ y) (x ＝ map-inv-∞-equiv y) + +open ∞-equiv public + +module _ + {l1 l2 : Level} (A : UU l1) (B : UU l2) + where + + infix 6 _≃∞_ + + _≃∞_ : UU (l1 ⊔ l2) + _≃∞_ = ∞-equiv A B + +∞-equiv-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → is-∞-equiv f → A ≃∞ B +map-∞-equiv (∞-equiv-is-∞-equiv {f = f} H) = f +map-inv-∞-equiv (∞-equiv-is-∞-equiv H) = map-inv-is-∞-equiv H +∞-equiv-transpose-eq-∞-equiv (∞-equiv-is-∞-equiv H) x y = + ∞-equiv-is-∞-equiv (is-∞-equiv-map-transpose-is-∞-equiv H x y) + +map-transpose-eq-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃∞ B) → + (x : A) (y : B) → (map-∞-equiv e x ＝ y) → (x ＝ map-inv-∞-equiv e y) +map-transpose-eq-∞-equiv e x y = + map-∞-equiv (∞-equiv-transpose-eq-∞-equiv e x y) + +is-∞-equiv-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃∞ B) → + is-∞-equiv (map-∞-equiv e) +map-inv-is-∞-equiv (is-∞-equiv-∞-equiv e) = + map-inv-∞-equiv e +map-transpose-is-∞-equiv (is-∞-equiv-∞-equiv e) = + map-transpose-eq-∞-equiv e +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-∞-equiv e) x y = + is-∞-equiv-∞-equiv (∞-equiv-transpose-eq-∞-equiv e x y) + +is-∞-equiv-map-transpose-eq-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃∞ B) (x : A) (y : B) → + is-∞-equiv (map-transpose-eq-∞-equiv e x y) +is-∞-equiv-map-transpose-eq-∞-equiv e x y = + is-∞-equiv-∞-equiv (∞-equiv-transpose-eq-∞-equiv e x y) +``` + +### Infinitely coherent identity equivalences + +```agda +is-∞-equiv-id : {l1 : Level} {A : UU l1} → is-∞-equiv (id {A = A}) +map-inv-is-∞-equiv is-∞-equiv-id = id +map-transpose-is-∞-equiv is-∞-equiv-id x y = id +is-∞-equiv-map-transpose-is-∞-equiv is-∞-equiv-id x y = is-∞-equiv-id + +id-∞-equiv : {l1 : Level} {A : UU l1} → A ≃∞ A +id-∞-equiv = ∞-equiv-is-∞-equiv is-∞-equiv-id +``` + +### Composition of infinitely coherent equivalences + +```agda +is-∞-equiv-comp : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {g : B → C} {f : A → B} + (G : is-∞-equiv g) + (F : is-∞-equiv f) → + is-∞-equiv (g ∘ f) +map-inv-is-∞-equiv (is-∞-equiv-comp G F) = + map-inv-is-∞-equiv F ∘ map-inv-is-∞-equiv G +map-transpose-is-∞-equiv (is-∞-equiv-comp G F) x z p = + map-transpose-is-∞-equiv F x _ (map-transpose-is-∞-equiv G _ z p) +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-comp G F) x z = + is-∞-equiv-comp + ( is-∞-equiv-map-transpose-is-∞-equiv F x _) + ( is-∞-equiv-map-transpose-is-∞-equiv G _ z) + +comp-∞-equiv : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} → + B ≃∞ C → A ≃∞ B → A ≃∞ C +comp-∞-equiv f e = + ∞-equiv-is-∞-equiv + ( is-∞-equiv-comp (is-∞-equiv-∞-equiv f) (is-∞-equiv-∞-equiv e)) +``` + +### Infinitely coherent equivalences obtained from equivalences + +Since +[transposing identifications along an equivalence](foundation.transposition-identifications-along-equivalences.md) +is an equivalence, it follows immediately that equivalences are infinitely +coherent equivalences. This argument does not require +[function extensionality](foundation.function-extensionality.md). + +```agda +is-∞-equiv-is-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → + is-equiv f → is-∞-equiv f +map-inv-is-∞-equiv (is-∞-equiv-is-equiv H) = + map-inv-is-equiv H +map-transpose-is-∞-equiv (is-∞-equiv-is-equiv H) x y = + map-eq-transpose-equiv (_ , H) +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-is-equiv H) x y = + is-∞-equiv-is-equiv (is-equiv-map-equiv (eq-transpose-equiv (_ , H) x y)) + +∞-equiv-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → A ≃ B → A ≃∞ B +∞-equiv-equiv e = + ∞-equiv-is-∞-equiv (is-∞-equiv-is-equiv (is-equiv-map-equiv e)) +``` + +## Properties + +### Any map homotopic to an infinitely coherent equivalence is an infinitely coherent equivalence + +```agda +is-∞-equiv-htpy : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} → + f ~ g → + is-∞-equiv f → is-∞-equiv g +map-inv-is-∞-equiv (is-∞-equiv-htpy H K) = + map-inv-is-∞-equiv K +map-transpose-is-∞-equiv (is-∞-equiv-htpy H K) x y = + map-transpose-is-∞-equiv K x y ∘ concat (H x) _ +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-htpy H K) x y = + is-∞-equiv-comp + ( is-∞-equiv-map-transpose-is-∞-equiv K x y) + ( is-∞-equiv-is-equiv (is-equiv-concat (H x) _)) +``` + +### Homotopies of elements of type `is-∞-equiv f` + +Consider a map `f : A → B` and consider two elements + +```text + H K : is-∞-equiv f. +``` + +A {{#concept "homotopy of elments of type `is-∞-equiv`" Agda=htpy-is-∞-equiv}} +from `H := (h , s , H')` to `K := (k , t , K')` consists of a homotopy + +```text + α₀ : h ~ k, +``` + +for each `x : A` and `y : B` a homotopy `α₁` witnessing that the triangle + +```text + (f x = y) + / \ + s x y / \ t x y + / \ + ∨ ∨ + (x = h y) --------------> (x = k y) + p ↦ p ∙ α₀ y +``` + +commutes, and finally a homotopy of elements of type + +```text + is-infinitely-coherent-equivalence + ( is-∞-equiv-htpy α₁ + ( is-∞-equiv-comp + ( is-∞-equiv-is-equiv + ( is-equiv-concat' _ (α₀ y))) + ( H' x y)) + ( K' x y). +``` + +In other words, there are by the previous data two witnesses of the fact that +`t x y` is an infinitely coherent equivalence. The second (easiest) element is +the given element `K' x y`. The first element is from the homotopy witnessing +that the above triangle commutes. On the left we compose two infinitely coherent +equivalences, which results in an infinitely coherent equivalence, and the +element witnessing that the composite is an infinitely coherent equivalence +transports along the homotopy to a new element witnessing that `t x y` is an +infinitely coherent equivalence. + +```agda +record + htpy-is-∞-equiv + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + (H K : is-∞-equiv f) : UU (l1 ⊔ l2) + where + coinductive + field + htpy-map-inv-htpy-is-∞-equiv : + map-inv-is-∞-equiv H ~ map-inv-is-∞-equiv K + htpy-map-transpose-htpy-is-∞-equiv : + (x : A) (y : B) → + coherence-triangle-maps + ( map-transpose-is-∞-equiv K x y) + ( concat' _ (htpy-map-inv-htpy-is-∞-equiv y)) + ( map-transpose-is-∞-equiv H x y) + infinitely-htpy-htpy-is-∞-equiv : + (x : A) (y : B) → + htpy-is-∞-equiv + ( map-transpose-is-∞-equiv K x y) + ( is-∞-equiv-htpy + ( inv-htpy (htpy-map-transpose-htpy-is-∞-equiv x y)) + ( is-∞-equiv-comp + ( is-∞-equiv-is-equiv (is-equiv-concat' _ _)) + ( is-∞-equiv-map-transpose-is-∞-equiv H x y))) + ( is-∞-equiv-map-transpose-is-∞-equiv K x y) +``` + +### Being an infinitely coherent equivalence implies being an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + is-equiv-is-∞-equiv : is-∞-equiv f → is-equiv f + is-equiv-is-∞-equiv H = + is-equiv-is-invertible + ( map-inv-is-∞-equiv H) + ( λ y → + map-inv-is-∞-equiv (is-∞-equiv-map-transpose-is-∞-equiv H _ y) refl) + ( λ x → inv (map-transpose-is-∞-equiv H x (f x) refl)) +``` + +### Computing the type `is-∞-equiv f` + +```agda +type-compute-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → UU (l1 ⊔ l2) +type-compute-is-∞-equiv {A = A} {B} f = + Σ (B → A) (λ g → (x : A) (y : B) → Σ ((f x ＝ y) → (x ＝ g y)) is-∞-equiv) + +map-compute-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + type-compute-is-∞-equiv f → is-∞-equiv f +map-inv-is-∞-equiv (map-compute-is-∞-equiv f H) = + pr1 H +map-transpose-is-∞-equiv (map-compute-is-∞-equiv f H) x y = + pr1 (pr2 H x y) +is-∞-equiv-map-transpose-is-∞-equiv (map-compute-is-∞-equiv f H) x y = + pr2 (pr2 H x y) + +map-inv-compute-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + is-∞-equiv f → type-compute-is-∞-equiv f +pr1 (map-inv-compute-is-∞-equiv f H) = + map-inv-is-∞-equiv H +pr1 (pr2 (map-inv-compute-is-∞-equiv f H) x y) = + map-transpose-is-∞-equiv H x y +pr2 (pr2 (map-inv-compute-is-∞-equiv f H) x y) = + is-∞-equiv-map-transpose-is-∞-equiv H x y +``` + +### Being an infinitely coherent equivalence is a property + +```text +is-prop-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + is-prop (is-∞-equiv f) +is-prop-is-∞-equiv = {!!} +``` diff --git a/src/foundation/retractions.lagda.md b/src/foundation/retractions.lagda.md index 3c51b23ceb..b412a82210 100644 --- a/src/foundation/retractions.lagda.md +++ b/src/foundation/retractions.lagda.md @@ -12,7 +12,6 @@ open import foundation-core.retractions public open import foundation.action-on-identifications-functions open import foundation.coslice open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.retracts-of-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -102,60 +101,3 @@ abstract retraction f → is-injective f is-injective-retraction f (h , H) {x} {y} p = inv (H x) ∙ (ap h p ∙ H y) ``` - -### Transposing identifications along retractions - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) - where - - transpose-eq-is-retraction : - g ∘ f ~ id → {x : B} {y : A} → x ＝ f y → g x ＝ y - transpose-eq-is-retraction H {x} {y} p = ap g p ∙ H y - - transpose-eq-is-retraction' : - g ∘ f ~ id → {x : A} {y : B} → f x ＝ y → x ＝ g y - transpose-eq-is-retraction' H {x} refl = inv (H x) - - is-retraction-transpose-eq : - ({x : B} {y : A} → x ＝ f y → g x ＝ y) → g ∘ f ~ id - is-retraction-transpose-eq H x = H refl - - is-retraction-transpose-eq' : - ({x : A} {y : B} → f x ＝ y → x ＝ g y) → g ∘ f ~ id - is-retraction-transpose-eq' H x = inv (H refl) - - is-retraction-is-retraction-transpose-eq : - is-retraction-transpose-eq ∘ transpose-eq-is-retraction ~ id - is-retraction-is-retraction-transpose-eq H = refl - - htpy-is-section-is-retraction-transpose-eq : - (H : {x : B} {y : A} → x ＝ f y → g x ＝ y) - (x : B) (y : A) → - transpose-eq-is-retraction (is-retraction-transpose-eq H) {x} {y} ~ - H {x} {y} - htpy-is-section-is-retraction-transpose-eq H x y refl = refl - - abstract - is-section-is-retraction-transpose-eq : - transpose-eq-is-retraction ∘ is-retraction-transpose-eq ~ id - is-section-is-retraction-transpose-eq H = - eq-htpy-implicit - ( λ x → - eq-htpy-implicit - ( λ y → eq-htpy (htpy-is-section-is-retraction-transpose-eq H x y))) - - is-equiv-transpose-eq-is-retraction : - is-equiv transpose-eq-is-retraction - is-equiv-transpose-eq-is-retraction = - is-equiv-is-invertible - ( is-retraction-transpose-eq) - ( is-section-is-retraction-transpose-eq) - ( is-retraction-is-retraction-transpose-eq) - - equiv-transpose-eq-is-retraction : - (g ∘ f ~ id) ≃ ({x : B} {y : A} → x ＝ f y → g x ＝ y) - equiv-transpose-eq-is-retraction = - (transpose-eq-is-retraction , is-equiv-transpose-eq-is-retraction) -``` diff --git a/src/foundation/sections.lagda.md b/src/foundation/sections.lagda.md index ca2ce02401..9a000d7e96 100644 --- a/src/foundation/sections.lagda.md +++ b/src/foundation/sections.lagda.md @@ -187,60 +187,3 @@ is-injective-map-section-family : is-injective (map-section-family b) is-injective-map-section-family b = ap pr1 ``` - -### Transposing identifications along sections - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) - where - - transpose-eq-is-section : - f ∘ g ~ id → {x : A} {y : B} → x ＝ g y → f x ＝ y - transpose-eq-is-section H {x} {y} p = ap f p ∙ H y - - transpose-eq-is-section' : - f ∘ g ~ id → {x : B} {y : A} → g x ＝ y → x ＝ f y - transpose-eq-is-section' H {x} refl = inv (H x) - - is-section-transpose-eq : - ({x : A} {y : B} → x ＝ g y → f x ＝ y) → f ∘ g ~ id - is-section-transpose-eq H x = H refl - - is-section-transpose-eq' : - ({x : B} {y : A} → g x ＝ y → x ＝ f y) → f ∘ g ~ id - is-section-transpose-eq' H x = inv (H refl) - - is-retraction-is-section-transpose-eq : - is-section-transpose-eq ∘ transpose-eq-is-section ~ id - is-retraction-is-section-transpose-eq H = refl - - htpy-is-section-is-section-transpose-eq : - (H : {x : A} {y : B} → x ＝ g y → f x ＝ y) → - (x : A) (y : B) → - transpose-eq-is-section (is-section-transpose-eq H) {x} {y} ~ H {x} {y} - htpy-is-section-is-section-transpose-eq H x y refl = refl - - abstract - is-section-is-section-transpose-eq : - transpose-eq-is-section ∘ is-section-transpose-eq ~ id - is-section-is-section-transpose-eq H = - eq-htpy-implicit - ( λ x → - eq-htpy-implicit - ( λ y → - eq-htpy (htpy-is-section-is-section-transpose-eq H x y))) - - is-equiv-transpose-eq-is-section : - is-equiv transpose-eq-is-section - is-equiv-transpose-eq-is-section = - is-equiv-is-invertible - ( is-section-transpose-eq) - ( is-section-is-section-transpose-eq) - ( is-retraction-is-section-transpose-eq) - - equiv-transpose-eq-is-section : - (f ∘ g ~ id) ≃ ({x : A} {y : B} → x ＝ g y → f x ＝ y) - equiv-transpose-eq-is-section = - (transpose-eq-is-section , is-equiv-transpose-eq-is-section) -``` diff --git a/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md b/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md index f3f4dce0d8..e28331de4b 100644 --- a/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md +++ b/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md @@ -17,9 +17,9 @@ open import foundation-core.identity-types ## Idea -The -{{#concept "concatenation operation on identifications" Agda=_∙_ Agda=_∙'_ Agda=concat}} -is a family of binary operations +The concatenation operation on +[identifications](foundation-core.identity-types.md) is a family of binary +operations ```text _∙_ : x ＝ y → y ＝ z → x ＝ z diff --git a/src/foundation/transposition-identifications-along-equivalences.lagda.md b/src/foundation/transposition-identifications-along-equivalences.lagda.md index 2ed786e907..140374a3ff 100644 --- a/src/foundation/transposition-identifications-along-equivalences.lagda.md +++ b/src/foundation/transposition-identifications-along-equivalences.lagda.md @@ -109,6 +109,10 @@ It is sometimes useful to consider identifications `y ＝ e x` instead of `e x ＝ y`, so we include an inverted equivalence for that as well. ```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) + where + eq-transpose-equiv-inv : (x : A) (y : B) → (y ＝ map-equiv e x) ≃ (map-inv-equiv e y ＝ x) eq-transpose-equiv-inv x y = diff --git a/src/foundation/transposition-identifications-along-retractions.lagda.md b/src/foundation/transposition-identifications-along-retractions.lagda.md new file mode 100644 index 0000000000..2dfe11e3cb --- /dev/null +++ b/src/foundation/transposition-identifications-along-retractions.lagda.md @@ -0,0 +1,111 @@ +# Transposing identifications along retractions + +```agda +module foundation.transposition-identifications-along-retractions where +``` + +
+ +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.retractions +``` + +
+ +## Idea + +Consider a map `f : A → B` and a map `g : B → A` in the converse direction. Then +there is an [equivalence](foundation-core.equivalences.md) + +```text + is-retraction f g ≃ ((x : A) (y : B) → (f x ＝ y) ≃ (x ＝ g y)) +``` + +In other words, any [retracting homotopy](foundation-core.retractions.md) +`g ∘ f ~ id` induces a unique family of +{{#concept "transposition" Disambiguation="identifications along retractions" Agda=eq-transpose-is-retraction}} +maps + +```text + f x ＝ y → x ＝ g y +``` + +indexed by `x : A` and `y : B`. + +## Definitions + +### Transposing identifications along retractions + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + eq-transpose-is-retraction : + is-retraction f g → {x : B} {y : A} → x ＝ f y → g x ＝ y + eq-transpose-is-retraction H {x} {y} p = ap g p ∙ H y + + eq-transpose-is-retraction' : + is-retraction f g → {x : A} {y : B} → f x ＝ y → x ＝ g y + eq-transpose-is-retraction' H {x} refl = inv (H x) +``` + +## Properties + +### The map that assings to each retracting homotopy a family of transposition functions of identifications is an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + is-retraction-eq-transpose : + ({x : B} {y : A} → x ＝ f y → g x ＝ y) → is-retraction f g + is-retraction-eq-transpose H x = H refl + + is-retraction-eq-transpose' : + ({x : A} {y : B} → f x ＝ y → x ＝ g y) → is-retraction f g + is-retraction-eq-transpose' H x = inv (H refl) + + is-retraction-is-retraction-eq-transpose : + is-retraction-eq-transpose ∘ eq-transpose-is-retraction f g ~ id + is-retraction-is-retraction-eq-transpose H = refl + + htpy-is-section-is-retraction-eq-transpose : + (H : {x : B} {y : A} → x ＝ f y → g x ＝ y) + (x : B) (y : A) → + eq-transpose-is-retraction f g (is-retraction-eq-transpose H) {x} {y} ~ + H {x} {y} + htpy-is-section-is-retraction-eq-transpose H x y refl = refl + + abstract + is-section-is-retraction-eq-transpose : + eq-transpose-is-retraction f g ∘ is-retraction-eq-transpose ~ id + is-section-is-retraction-eq-transpose H = + eq-htpy-implicit + ( λ x → + eq-htpy-implicit + ( λ y → eq-htpy (htpy-is-section-is-retraction-eq-transpose H x y))) + + is-equiv-eq-transpose-is-retraction : + is-equiv (eq-transpose-is-retraction f g) + is-equiv-eq-transpose-is-retraction = + is-equiv-is-invertible + ( is-retraction-eq-transpose) + ( is-section-is-retraction-eq-transpose) + ( is-retraction-is-retraction-eq-transpose) + + equiv-eq-transpose-is-retraction : + is-retraction f g ≃ ({x : B} {y : A} → x ＝ f y → g x ＝ y) + equiv-eq-transpose-is-retraction = + ( eq-transpose-is-retraction f g , is-equiv-eq-transpose-is-retraction) +``` diff --git a/src/foundation/transposition-identifications-along-sections.lagda.md b/src/foundation/transposition-identifications-along-sections.lagda.md new file mode 100644 index 0000000000..9cffc6452a --- /dev/null +++ b/src/foundation/transposition-identifications-along-sections.lagda.md @@ -0,0 +1,109 @@ +# Transposing identifications along sections + +```agda +module foundation.transposition-identifications-along-sections where +``` + +
+ +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.sections +``` + +
+ +## Idea + +Consider a map `f : A → B` and a map `g : B → A` in the converse direction. Then +there is an [equivalence](foundation-core.equivalences.md) + +```text + is-section f g ≃ ((x : A) (y : B) → (x ＝ g y) ≃ (f x ＝ y)) +``` + +In other words, any [section homotopy](foundation-core.sections.md) `f ∘ g ~ id` +induces a unique family of +{{#concept "transposition" Disambiguation="identifications along sections" Agda=eq-transpose-is-section}} +maps + +```text + x ＝ g y → f x ＝ y +``` + +indexed by `x : A` and `y : B`. + +### Transposing identifications along sections + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + eq-transpose-is-section : + f ∘ g ~ id → {x : A} {y : B} → x ＝ g y → f x ＝ y + eq-transpose-is-section H {x} {y} p = ap f p ∙ H y + + eq-transpose-is-section' : + f ∘ g ~ id → {x : B} {y : A} → g x ＝ y → x ＝ f y + eq-transpose-is-section' H {x} refl = inv (H x) +``` + +## Properties + +### The map that assings to each section homotopy a family of transposition functions of identifications is an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + is-section-eq-transpose : + ({x : A} {y : B} → x ＝ g y → f x ＝ y) → f ∘ g ~ id + is-section-eq-transpose H x = H refl + + is-section-eq-transpose' : + ({x : B} {y : A} → g x ＝ y → x ＝ f y) → f ∘ g ~ id + is-section-eq-transpose' H x = inv (H refl) + + is-retraction-is-section-eq-transpose : + is-section-eq-transpose ∘ eq-transpose-is-section f g ~ id + is-retraction-is-section-eq-transpose H = refl + + htpy-is-section-is-section-eq-transpose : + (H : {x : A} {y : B} → x ＝ g y → f x ＝ y) → + (x : A) (y : B) → + eq-transpose-is-section f g (is-section-eq-transpose H) {x} {y} ~ H {x} {y} + htpy-is-section-is-section-eq-transpose H x y refl = refl + + abstract + is-section-is-section-eq-transpose : + eq-transpose-is-section f g ∘ is-section-eq-transpose ~ id + is-section-is-section-eq-transpose H = + eq-htpy-implicit + ( λ x → + eq-htpy-implicit + ( λ y → + eq-htpy (htpy-is-section-is-section-eq-transpose H x y))) + + is-equiv-eq-transpose-is-section : + is-equiv (eq-transpose-is-section f g) + is-equiv-eq-transpose-is-section = + is-equiv-is-invertible + ( is-section-eq-transpose) + ( is-section-is-section-eq-transpose) + ( is-retraction-is-section-eq-transpose) + + equiv-eq-transpose-is-section : + (f ∘ g ~ id) ≃ ({x : A} {y : B} → x ＝ g y → f x ＝ y) + equiv-eq-transpose-is-section = + (eq-transpose-is-section f g , is-equiv-eq-transpose-is-section) +``` diff --git a/src/group-theory/conjugation.lagda.md b/src/group-theory/conjugation.lagda.md index 8ab1d3121c..e1534c847c 100644 --- a/src/group-theory/conjugation.lagda.md +++ b/src/group-theory/conjugation.lagda.md @@ -19,6 +19,8 @@ open import foundation.identity-types open import foundation.retractions open import foundation.sections open import foundation.subtypes +open import foundation.transposition-identifications-along-retractions +open import foundation.transposition-identifications-along-sections open import foundation.universe-levels open import group-theory.group-actions @@ -333,7 +335,7 @@ module _ {x y z : type-Group G} → y ＝ conjugation-Group G (inv-Group G x) z → conjugation-Group G x y ＝ z transpose-eq-conjugation-Group {x} {y} {z} = - transpose-eq-is-section + eq-transpose-is-section ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-section-conjugation-inv-Group x) @@ -342,7 +344,7 @@ module _ {x y z : type-Group G} → conjugation-Group G (inv-Group G x) y ＝ z → y ＝ conjugation-Group G x z transpose-eq-conjugation-Group' {x} {y} {z} = - transpose-eq-is-section' + eq-transpose-is-section' ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-section-conjugation-inv-Group x) @@ -351,7 +353,7 @@ module _ {x y z : type-Group G} → y ＝ conjugation-Group G x z → conjugation-Group G (inv-Group G x) y ＝ z transpose-eq-conjugation-inv-Group {x} {y} {z} = - transpose-eq-is-retraction + eq-transpose-is-retraction ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-retraction-conjugation-inv-Group x) @@ -360,7 +362,7 @@ module _ {x y z : type-Group G} → conjugation-Group G x y ＝ z → y ＝ conjugation-Group G (inv-Group G x) z transpose-eq-conjugation-inv-Group' {x} {y} {z} = - transpose-eq-is-retraction' + eq-transpose-is-retraction' ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-retraction-conjugation-inv-Group x) From b5ec17ab5587f14c3ce8656f9478bdfcb2c960f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Tue, 27 Feb 2024 17:13:25 +0100 Subject: [PATCH 07/10] Add netlify environment variables to benchmark deployment action (#1044) This _should_ enable deployments of the benchmarking website --- .github/workflows/profiling.yaml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 6f2beafcd0..5f265e1e34 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -74,5 +74,8 @@ jobs: echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js - name: Deploy the new profiling website + env: + NETLIFY_SITE_ID: ${{ secrets.PERF_SITE_ID }} + NETLIFY_AUTH_TOKEN: ${{ secrets.PERF_SITE_KEY }} run: | - npx netlify-cli deploy --dir=benchmark-website + npx netlify-cli deploy --prod --dir=benchmark-website From d5f63de0ff6f01f6df97a4c1909aa1dd012f2553 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 27 Feb 2024 17:16:58 +0100 Subject: [PATCH 08/10] Track user analytics for website (#1035) This simple addition tracks some anonymous user data using GoatCounter. - [x] Create `agda-unimath` user at [GoatCounter](https://www.goatcounter.com/) - [x] Inject GoatCounter script Resolves #1029 --- theme/index.hbs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theme/index.hbs b/theme/index.hbs index 13935f31c1..fb365846a4 100644 --- a/theme/index.hbs +++ b/theme/index.hbs @@ -332,6 +332,8 @@ {{/if}} + + From b5985b52cb65fa9b2da4b961983ee1a1f5c4f6dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Tue, 27 Feb 2024 17:34:04 +0100 Subject: [PATCH 09/10] Fix benchmark deployment directory (#1045) --- .github/workflows/profiling.yaml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 5f265e1e34..e153d46398 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -67,11 +67,10 @@ jobs: - name: Prepare new revision of the profiling website run: | - cd repo mkdir -p benchmark-website - cp website/benchmarks/index.html benchmark-website/ - cp ../benchmark-cache/data.* benchmark-website/ - echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js + cp repo/website/benchmarks/index.html benchmark-website/ + cp benchmark-cache/data.* benchmark-website/ + echo 'window.BENCHMARK_DATA =' | cat - benchmark-cache/data.json > benchmark-website/data.js - name: Deploy the new profiling website env: From 053072398cd5a6a50c82518dfa0caa60c8342969 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 27 Feb 2024 17:52:21 +0100 Subject: [PATCH 10/10] A small optimization to equivalence relations (#1040) - Makes equivalence relations typecheck in about half the time. I also had a look at `category-of-functors-from-small-to-large-categories`, and I really can't find anything wrong, so I'm a bit puzzled. - Adds a make hook for more streamlined profiling of individual modules. --- .vscode/settings.json | 10 +- Makefile | 77 ++++++-- .../abstract-quaternion-group.lagda.md | 32 +-- .../descent-coproduct-types.lagda.md | 2 + src/foundation/equivalence-relations.lagda.md | 184 ++++++++---------- src/foundation/partitions.lagda.md | 179 ++++++++--------- .../type-arithmetic-unit-type.lagda.md | 40 ++-- .../higher-modalities.lagda.md | 2 +- .../universal-cover-circle.lagda.md | 2 + ...tations-complete-undirected-graph.lagda.md | 100 +++++----- 10 files changed, 335 insertions(+), 293 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index b26a54f715..c4b4244f33 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -27,10 +27,7 @@ "files.exclude": { "MAlonzo/": true, "**/MAlonzo/": true, - "_build/": true, - "**/_build/": true, - "agdaFiles": true, - "src/temp/": true + "agdaFiles": true }, // Snippet setup @@ -94,6 +91,11 @@ "editor.autoClosingBrackets": "never" }, + "[makefile]": { + "editor.insertSpaces": false, + "editor.detectIndentation": true + }, + "[markdown]": { "editor.rulers": [80], "editor.quickSuggestions": { diff --git a/Makefile b/Makefile index 91e96b4c5c..02ea8b2885 100644 --- a/Makefile +++ b/Makefile @@ -25,24 +25,24 @@ AGDA ?= agda $(AGDAVERBOSE) $(AGDARTS) TIME ?= time METAFILES := \ - ART.md \ - CITE-THIS-LIBRARY.md \ - CODINGSTYLE.md \ - CONTRIBUTING.md \ - CONTRIBUTORS.md \ - FILE-CONVENTIONS.md \ - DESIGN-PRINCIPLES.md \ - GRANT-ACKNOWLEDGEMENTS.md \ - HOME.md \ - HOWTO-INSTALL.md \ - LICENSE.md \ - MIXFIX-OPERATORS.md \ - MAINTAINERS.md \ - README.md \ - STATEMENT-OF-INCLUSION.md \ - SUMMARY.md \ - TEMPLATE.lagda.md \ - USERS.md \ + ART.md \ + CITE-THIS-LIBRARY.md \ + CODINGSTYLE.md \ + CONTRIBUTING.md \ + CONTRIBUTORS.md \ + FILE-CONVENTIONS.md \ + DESIGN-PRINCIPLES.md \ + GRANT-ACKNOWLEDGEMENTS.md \ + HOME.md \ + HOWTO-INSTALL.md \ + LICENSE.md \ + MIXFIX-OPERATORS.md \ + MAINTAINERS.md \ + README.md \ + STATEMENT-OF-INCLUSION.md \ + SUMMARY.md \ + TEMPLATE.lagda.md \ + USERS.md \ .PHONY: agdaFiles agdaFiles: @@ -75,6 +75,47 @@ check: ./src/everything.lagda.md check-profile: ./src/everything.lagda.md ${AGDA} ${AGDAPROFILEFLAGS} $? +# Base directory where Agda interface files are stored +BUILD_DIR := ./_build +# Directory for temporary files +TEMP_DIR := ./temp +# Convert module path to directory path (replace dots with slashes) +MODULE_DIR = $(subst .,/,$(MODULE)) + + +# Default agda arguments for `profile-module` +PROFILE_MODULE_AGDA_ARGS ?= --profile=definitions +# Target for profiling the typechecking a single module +.PHONY: profile-module +profile-module: + @if [ -z "$(MODULE)" ]; then \ + echo "\033[0;31mError: MODULE variable is not set.\033[0m"; \ + echo "\033[0;31mUsage: make check-module MODULE=\"YourModuleName\"\033[0m"; \ + exit 1; \ + fi + @# Attempt to delete the interface file only if the build directory exists + @echo "\033[0;32mAttempting to delete interface file for $(MODULE)\033[0m" + @find $(BUILD_DIR) -type f -path "*/agda/src/$(MODULE_DIR).agdai" -exec rm -f {} \+ 2>/dev/null || \ + echo "\033[0;31m$(BUILD_DIR) directory does not exist, skipping deletion of interface files.\033[0m" + @# Ensure the temporary directory exists + @mkdir -p $(TEMP_DIR) + @# Profile typechecking the module and capture the output in the temp directory, also display on terminal + @echo "\033[0;32mProfiling typechecking of $(MODULE)\033[0m" + @$(AGDA) $(PROFILE_MODULE_AGDA_ARGS) src/$(MODULE_DIR).lagda.md 2>&1 | tee $(TEMP_DIR)/typecheck_output.txt + @# Check for additional modules being typechecked by looking for any indented "Checking" line + @if grep -E "^\s+Checking " $(TEMP_DIR)/typecheck_output.txt > /dev/null; then \ + echo "\033[0;31mOther modules were also checked. Repeating profiling after deleting interface file again.\033[0m"; \ + find $(BUILD_DIR) -type f -path "*/agda/src/$(MODULE_DIR).agdai" -exec rm -f {} \+; \ + $(AGDA) $(PROFILE_MODULE_AGDA_ARGS) src/$(MODULE_DIR).lagda.md; \ + else \ + echo "\033[0;32mOnly $(MODULE) was checked. Profiling complete.\033[0m"; \ + fi + + @# Cleanup + @rm -f $(TEMP_DIR)/typecheck_output.txt + + + agda-html: ./src/everything.lagda.md @rm -rf ./docs/ @mkdir -p ./docs/ diff --git a/src/finite-group-theory/abstract-quaternion-group.lagda.md b/src/finite-group-theory/abstract-quaternion-group.lagda.md index e995599b64..e550600c66 100644 --- a/src/finite-group-theory/abstract-quaternion-group.lagda.md +++ b/src/finite-group-theory/abstract-quaternion-group.lagda.md @@ -866,14 +866,14 @@ is-noncommutative-mul-Q8 : is-noncommutative-mul-Q8 f = Eq-eq-Q8 (f i-Q8 j-Q8) map-equiv-count-Q8 : Fin 8 → Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inl (inr star)))))))) = e-Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inr star))))))) = -e-Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inl (inr star)))))) = i-Q8 -map-equiv-count-Q8 (inl (inl (inl (inl (inr star))))) = -i-Q8 -map-equiv-count-Q8 (inl (inl (inl (inr star)))) = j-Q8 -map-equiv-count-Q8 (inl (inl (inr star))) = -j-Q8 -map-equiv-count-Q8 (inl (inr star)) = k-Q8 -map-equiv-count-Q8 (inr star) = -k-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inl (inr _)))))))) = e-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inl (inl (inr _))))))) = -e-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inl (inr _)))))) = i-Q8 +map-equiv-count-Q8 (inl (inl (inl (inl (inr _))))) = -i-Q8 +map-equiv-count-Q8 (inl (inl (inl (inr _)))) = j-Q8 +map-equiv-count-Q8 (inl (inl (inr _))) = -j-Q8 +map-equiv-count-Q8 (inl (inr _)) = k-Q8 +map-equiv-count-Q8 (inr _) = -k-Q8 map-inv-equiv-count-Q8 : Q8 → Fin 8 map-inv-equiv-count-Q8 e-Q8 = inl (inl (inl (inl (inl (inl (inl (inr star))))))) @@ -899,16 +899,16 @@ is-section-map-inv-equiv-count-Q8 -k-Q8 = refl is-retraction-map-inv-equiv-count-Q8 : ( map-inv-equiv-count-Q8 ∘ map-equiv-count-Q8) ~ id is-retraction-map-inv-equiv-count-Q8 - (inl (inl (inl (inl (inl (inl (inl (inr star)))))))) = refl + (inl (inl (inl (inl (inl (inl (inl (inr _)))))))) = refl is-retraction-map-inv-equiv-count-Q8 - (inl (inl (inl (inl (inl (inl (inr star))))))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inl (inr star)))))) = + (inl (inl (inl (inl (inl (inl (inr _))))))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inl (inr _)))))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inr star))))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inr star)))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inl (inr star))) = refl -is-retraction-map-inv-equiv-count-Q8 (inl (inr star)) = refl -is-retraction-map-inv-equiv-count-Q8 (inr star) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inl (inr _))))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inl (inr _)))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inl (inr _))) = refl +is-retraction-map-inv-equiv-count-Q8 (inl (inr _)) = refl +is-retraction-map-inv-equiv-count-Q8 (inr _) = refl is-equiv-map-equiv-count-Q8 : is-equiv map-equiv-count-Q8 is-equiv-map-equiv-count-Q8 = diff --git a/src/foundation/descent-coproduct-types.lagda.md b/src/foundation/descent-coproduct-types.lagda.md index 830753d53c..03c1a582ba 100644 --- a/src/foundation/descent-coproduct-types.lagda.md +++ b/src/foundation/descent-coproduct-types.lagda.md @@ -1,6 +1,8 @@ # Descent for coproduct types ```agda +{-# OPTIONS --lossy-unification #-} + module foundation.descent-coproduct-types where ``` diff --git a/src/foundation/equivalence-relations.lagda.md b/src/foundation/equivalence-relations.lagda.md index 127b324232..821a14f484 100644 --- a/src/foundation/equivalence-relations.lagda.md +++ b/src/foundation/equivalence-relations.lagda.md @@ -126,24 +126,26 @@ module _ is-block-partition-equivalence-relation Q = type-Prop (is-block-prop-partition-equivalence-relation Q) - is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation : - is-partition (is-equivalence-class-inhabited-subtype-equivalence-relation R) - is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation x = - is-contr-equiv - ( Σ ( Σ ( equivalence-class R) - ( λ C → is-in-equivalence-class R C x)) - ( λ t → is-inhabited-subtype (subtype-equivalence-class R (pr1 t)))) - ( ( equiv-right-swap-Σ) ∘e - ( equiv-Σ - ( λ Q → is-in-subtype (subtype-equivalence-class R (pr1 Q)) x) - ( equiv-right-swap-Σ) - ( λ Q → id-equiv))) - ( is-contr-Σ - ( is-torsorial-is-in-equivalence-class R x) - ( center-total-is-in-equivalence-class R x) - ( is-proof-irrelevant-is-prop - ( is-prop-type-trunc-Prop) - ( is-inhabited-subtype-equivalence-class R (class R x)))) + abstract + is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation : + is-partition + ( is-equivalence-class-inhabited-subtype-equivalence-relation R) + is-partition-is-equivalence-class-inhabited-subtype-equivalence-relation x = + is-contr-equiv + ( Σ ( Σ ( equivalence-class R) + ( λ C → is-in-equivalence-class R C x)) + ( λ t → is-inhabited-subtype (subtype-equivalence-class R (pr1 t)))) + ( ( equiv-right-swap-Σ) ∘e + ( equiv-Σ + ( λ Q → is-in-subtype (subtype-equivalence-class R (pr1 Q)) x) + ( equiv-right-swap-Σ) + ( λ Q → id-equiv))) + ( is-contr-Σ + ( is-torsorial-is-in-equivalence-class R x) + ( center-total-is-in-equivalence-class R x) + ( is-proof-irrelevant-is-prop + ( is-prop-type-trunc-Prop) + ( is-inhabited-subtype-equivalence-class R (class R x)))) partition-equivalence-relation : partition l2 (l1 ⊔ l2) A pr1 partition-equivalence-relation = @@ -333,79 +335,64 @@ module _ {l1 l2 : Level} {A : UU l1} (P : partition l1 l2 A) where - is-block-is-equivalence-class-equivalence-relation-partition : - (Q : inhabited-subtype l1 A) → - is-equivalence-class - ( equivalence-relation-partition P) - ( subtype-inhabited-subtype Q) → - is-block-partition P Q - is-block-is-equivalence-class-equivalence-relation-partition Q H = - apply-universal-property-trunc-Prop H - ( subtype-partition P Q) - ( λ (a , K) → - tr - ( is-block-partition P) - ( inv - ( eq-has-same-elements-inhabited-subtype Q - ( inhabited-subtype-block-partition P (class-partition P a)) - ( λ x → - logical-equivalence-reasoning - is-in-inhabited-subtype Q x - ↔ Σ ( block-partition P) - ( λ B → - is-in-block-partition P B a × - is-in-block-partition P B x) - by K x - ↔ is-in-block-partition P (class-partition P a) x - by - iff-equiv - ( ( left-unit-law-Σ-is-contr - ( is-contr-block-containing-element-partition P a) - ( center-block-containing-element-partition P a)) ∘e - ( inv-associative-Σ - ( block-partition P) - ( λ B → is-in-block-partition P B a) - ( λ B → is-in-block-partition P (pr1 B) x)))))) - ( is-block-class-partition P a)) - - is-equivalence-class-is-block-partition : - (Q : inhabited-subtype l1 A) → - is-block-partition P Q → - is-equivalence-class - ( equivalence-relation-partition P) - ( subtype-inhabited-subtype Q) - is-equivalence-class-is-block-partition Q H = - apply-universal-property-trunc-Prop - ( is-inhabited-subtype-inhabited-subtype Q) - ( is-equivalence-class-Prop + abstract + is-block-is-equivalence-class-equivalence-relation-partition : + (Q : inhabited-subtype l1 A) → + is-equivalence-class ( equivalence-relation-partition P) - ( subtype-inhabited-subtype Q)) - ( λ (a , q) → - unit-trunc-Prop - ( pair - ( a) - ( λ x → - iff-equiv - ( equivalence-reasoning - is-in-inhabited-subtype Q x - ≃ is-in-block-partition P (make-block-partition P Q H) x - by - compute-is-in-block-partition P Q H x - ≃ Σ ( block-partition P) - ( λ B → - is-in-block-partition P B a × - is-in-block-partition P B x) - by - inv-equiv - ( ( left-unit-law-Σ-is-contr - ( is-contr-block-containing-element-partition P a) - ( pair - ( make-block-partition P Q H) - ( make-is-in-block-partition P Q H a q))) ∘e - ( inv-associative-Σ - ( block-partition P) - ( λ B → is-in-block-partition P B a) - ( λ B → is-in-block-partition P (pr1 B) x))))))) + ( subtype-inhabited-subtype Q) → + is-block-partition P Q + is-block-is-equivalence-class-equivalence-relation-partition Q H = + apply-universal-property-trunc-Prop H + ( subtype-partition P Q) + ( λ (a , K) → + tr + ( is-block-partition P) + ( inv + ( eq-has-same-elements-inhabited-subtype Q + ( inhabited-subtype-block-partition P (class-partition P a)) + ( λ x → + ( iff-equiv + ( ( left-unit-law-Σ-is-contr + ( is-contr-block-containing-element-partition P a) + ( center-block-containing-element-partition P a)) ∘e + ( inv-associative-Σ + ( block-partition P) + ( λ B → is-in-block-partition P B a) + ( λ B → is-in-block-partition P (pr1 B) x)))) ∘iff + ( K x)))) + ( is-block-class-partition P a)) + + abstract + is-equivalence-class-is-block-partition : + (Q : inhabited-subtype l1 A) → + is-block-partition P Q → + is-equivalence-class + ( equivalence-relation-partition P) + ( subtype-inhabited-subtype Q) + is-equivalence-class-is-block-partition Q H = + apply-universal-property-trunc-Prop + ( is-inhabited-subtype-inhabited-subtype Q) + ( is-equivalence-class-Prop + ( equivalence-relation-partition P) + ( subtype-inhabited-subtype Q)) + ( λ (a , q) → + unit-trunc-Prop + ( pair + ( a) + ( λ x → + iff-equiv + ( ( inv-equiv + ( ( left-unit-law-Σ-is-contr + ( is-contr-block-containing-element-partition P a) + ( pair + ( make-block-partition P Q H) + ( make-is-in-block-partition P Q H a q))) ∘e + ( inv-associative-Σ + ( block-partition P) + ( λ B → is-in-block-partition P B a) + ( λ B → is-in-block-partition P (pr1 B) x)))) ∘e + ( compute-is-in-block-partition P Q H x))))) has-same-elements-partition-equivalence-relation-partition : has-same-elements-subtype @@ -430,14 +417,15 @@ is-retraction-equivalence-relation-partition-equivalence-relation P = #### The map `equivalence-relation-partition` is an equivalence ```agda -is-equiv-equivalence-relation-partition : - {l : Level} {A : UU l} → - is-equiv (equivalence-relation-partition {l} {l} {l} {A}) -is-equiv-equivalence-relation-partition = - is-equiv-is-invertible - partition-equivalence-relation - is-section-equivalence-relation-partition-equivalence-relation - is-retraction-equivalence-relation-partition-equivalence-relation +abstract + is-equiv-equivalence-relation-partition : + {l : Level} {A : UU l} → + is-equiv (equivalence-relation-partition {l} {l} {l} {A}) + is-equiv-equivalence-relation-partition = + is-equiv-is-invertible + partition-equivalence-relation + is-section-equivalence-relation-partition-equivalence-relation + is-retraction-equivalence-relation-partition-equivalence-relation equiv-equivalence-relation-partition : {l : Level} {A : UU l} → partition l l A ≃ equivalence-relation l A diff --git a/src/foundation/partitions.lagda.md b/src/foundation/partitions.lagda.md index 9f37022516..414d0edeca 100644 --- a/src/foundation/partitions.lagda.md +++ b/src/foundation/partitions.lagda.md @@ -286,40 +286,43 @@ will have no more use for the large type of blocks of a partition. is-prop-is-in-block-partition-Large-Type ( map-inv-compute-block-partition B) - compute-is-in-block-partition : - (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → - is-in-inhabited-subtype B x ≃ - is-in-block-partition (make-block-partition B H) x - compute-is-in-block-partition B H x = - equiv-tr - ( λ C → is-in-block-partition-Large-Type C x) - ( inv (is-retraction-map-inv-compute-block-partition (B , H))) - - make-is-in-block-partition : - (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → - is-in-inhabited-subtype B x → - is-in-block-partition (make-block-partition B H) x - make-is-in-block-partition B H x K = - map-equiv (compute-is-in-block-partition B H x) K + abstract + compute-is-in-block-partition : + (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → + is-in-inhabited-subtype B x ≃ + is-in-block-partition (make-block-partition B H) x + compute-is-in-block-partition B H x = + equiv-tr + ( λ C → is-in-block-partition-Large-Type C x) + ( inv (is-retraction-map-inv-compute-block-partition (B , H))) + + abstract + make-is-in-block-partition : + (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) → + is-in-inhabited-subtype B x → + is-in-block-partition (make-block-partition B H) x + make-is-in-block-partition B H x K = + map-equiv (compute-is-in-block-partition B H x) K block-containing-element-partition : A → UU (l1 ⊔ l2) block-containing-element-partition a = Σ block-partition (λ B → is-in-block-partition B a) - is-contr-block-containing-element-partition : - (a : A) → is-contr (block-containing-element-partition a) - is-contr-block-containing-element-partition a = - is-contr-equiv' - ( Σ block-partition-Large-Type - ( λ B → is-in-block-partition-Large-Type B a)) - ( equiv-Σ - ( λ B → is-in-block-partition B a) - ( compute-block-partition) - ( λ B → - equiv-tr - ( λ C → is-in-block-partition-Large-Type C a) - ( inv (is-retraction-map-inv-compute-block-partition B)))) - ( is-partition-subtype-partition a) + abstract + is-contr-block-containing-element-partition : + (a : A) → is-contr (block-containing-element-partition a) + is-contr-block-containing-element-partition a = + is-contr-equiv' + ( Σ block-partition-Large-Type + ( λ B → is-in-block-partition-Large-Type B a)) + ( equiv-Σ + ( λ B → is-in-block-partition B a) + ( compute-block-partition) + ( λ B → + equiv-tr + ( λ C → is-in-block-partition-Large-Type C a) + ( inv (is-retraction-map-inv-compute-block-partition B)))) + ( is-partition-subtype-partition a) center-block-containing-element-partition : (a : A) → block-containing-element-partition a @@ -415,22 +418,23 @@ module _ refl-has-same-elements-inhabited-subtype ( inhabited-subtype-block-partition P B) - is-torsorial-has-same-elements-block-partition : - is-torsorial has-same-elements-block-partition - is-torsorial-has-same-elements-block-partition = - is-contr-equiv' - ( Σ ( block-partition P) + abstract + is-torsorial-has-same-elements-block-partition : + is-torsorial has-same-elements-block-partition + is-torsorial-has-same-elements-block-partition = + is-contr-equiv' + ( Σ ( block-partition P) + ( λ C → + inhabited-subtype-block-partition P B ＝ + inhabited-subtype-block-partition P C)) + ( equiv-tot ( λ C → - inhabited-subtype-block-partition P B ＝ - inhabited-subtype-block-partition P C)) - ( equiv-tot - ( λ C → - extensionality-inhabited-subtype - ( inhabited-subtype-block-partition P B) - ( inhabited-subtype-block-partition P C))) - ( fundamental-theorem-id' - ( λ C → ap (inhabited-subtype-block-partition P)) - ( is-emb-inhabited-subtype-block-partition P B)) + extensionality-inhabited-subtype + ( inhabited-subtype-block-partition P B) + ( inhabited-subtype-block-partition P C))) + ( fundamental-theorem-id' + ( λ C → ap (inhabited-subtype-block-partition P)) + ( is-emb-inhabited-subtype-block-partition P B)) has-same-elements-eq-block-partition : (C : block-partition P) → (B ＝ C) → @@ -615,50 +619,51 @@ module _ pr2 (subtype-partition-Set-Indexed-Σ-Decomposition Q) = is-prop-is-block-partition-Set-Indexed-Σ-Decomposition Q - is-partition-subtype-partition-Set-Indexed-Σ-Decomposition : - is-partition (subtype-partition-Set-Indexed-Σ-Decomposition {l2}) - is-partition-subtype-partition-Set-Indexed-Σ-Decomposition a = - is-contr-equiv - ( Σ ( inhabited-subtype l2 A) - ( has-same-elements-inhabited-subtype - ( pair - ( λ x → - Id-Prop - ( indexing-set-Set-Indexed-Σ-Decomposition D) - ( index-Set-Indexed-Σ-Decomposition D x) - ( index-Set-Indexed-Σ-Decomposition D a)) - ( unit-trunc-Prop (pair a refl))))) - ( ( equiv-tot - ( λ Q → - ( ( ( equiv-Π-equiv-family + abstract + is-partition-subtype-partition-Set-Indexed-Σ-Decomposition : + is-partition (subtype-partition-Set-Indexed-Σ-Decomposition {l2}) + is-partition-subtype-partition-Set-Indexed-Σ-Decomposition a = + is-contr-equiv + ( Σ ( inhabited-subtype l2 A) + ( has-same-elements-inhabited-subtype + ( pair ( λ x → - inv-equiv - ( equiv-equiv-iff - ( Id-Prop - ( indexing-set-Set-Indexed-Σ-Decomposition D) - ( index-Set-Indexed-Σ-Decomposition D x) - ( index-Set-Indexed-Σ-Decomposition D a)) - ( subtype-inhabited-subtype Q x)) ∘e - ( equiv-inv-equiv))) ∘e - ( left-unit-law-Σ-is-contr - ( is-torsorial-Id (index-Set-Indexed-Σ-Decomposition D a)) - ( pair - ( index-Set-Indexed-Σ-Decomposition D a) - ( refl)))) ∘e - ( equiv-right-swap-Σ)) ∘e - ( equiv-tot (λ ie → pr2 ie a)))) ∘e - ( associative-Σ - ( inhabited-subtype l2 A) - ( is-block-partition-Set-Indexed-Σ-Decomposition) - ( λ B → is-in-inhabited-subtype (pr1 B) a))) - ( is-torsorial-has-same-elements-inhabited-subtype - ( pair - ( λ x → - Id-Prop - ( indexing-set-Set-Indexed-Σ-Decomposition D) - ( index-Set-Indexed-Σ-Decomposition D x) - ( index-Set-Indexed-Σ-Decomposition D a)) - ( unit-trunc-Prop (pair a refl)))) + Id-Prop + ( indexing-set-Set-Indexed-Σ-Decomposition D) + ( index-Set-Indexed-Σ-Decomposition D x) + ( index-Set-Indexed-Σ-Decomposition D a)) + ( unit-trunc-Prop (pair a refl))))) + ( ( equiv-tot + ( λ Q → + ( ( ( equiv-Π-equiv-family + ( λ x → + inv-equiv + ( equiv-equiv-iff + ( Id-Prop + ( indexing-set-Set-Indexed-Σ-Decomposition D) + ( index-Set-Indexed-Σ-Decomposition D x) + ( index-Set-Indexed-Σ-Decomposition D a)) + ( subtype-inhabited-subtype Q x)) ∘e + ( equiv-inv-equiv))) ∘e + ( left-unit-law-Σ-is-contr + ( is-torsorial-Id (index-Set-Indexed-Σ-Decomposition D a)) + ( pair + ( index-Set-Indexed-Σ-Decomposition D a) + ( refl)))) ∘e + ( equiv-right-swap-Σ)) ∘e + ( equiv-tot (λ ie → pr2 ie a)))) ∘e + ( associative-Σ + ( inhabited-subtype l2 A) + ( is-block-partition-Set-Indexed-Σ-Decomposition) + ( λ B → is-in-inhabited-subtype (pr1 B) a))) + ( is-torsorial-has-same-elements-inhabited-subtype + ( pair + ( λ x → + Id-Prop + ( indexing-set-Set-Indexed-Σ-Decomposition D) + ( index-Set-Indexed-Σ-Decomposition D x) + ( index-Set-Indexed-Σ-Decomposition D a)) + ( unit-trunc-Prop (pair a refl)))) partition-Set-Indexed-Σ-Decomposition : {l1 l2 l3 : Level} {A : UU l1} → diff --git a/src/foundation/type-arithmetic-unit-type.lagda.md b/src/foundation/type-arithmetic-unit-type.lagda.md index 508c3f20b6..7f3e6fc73e 100644 --- a/src/foundation/type-arithmetic-unit-type.lagda.md +++ b/src/foundation/type-arithmetic-unit-type.lagda.md @@ -17,6 +17,8 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.retractions +open import foundation-core.sections ``` @@ -35,7 +37,7 @@ module _ where map-left-unit-law-Σ : Σ unit A → A star - map-left-unit-law-Σ (pair star a) = a + map-left-unit-law-Σ (_ , a) = a map-inv-left-unit-law-Σ : A star → Σ unit A pr1 (map-inv-left-unit-law-Σ a) = star @@ -43,11 +45,11 @@ module _ is-section-map-inv-left-unit-law-Σ : ( map-left-unit-law-Σ ∘ map-inv-left-unit-law-Σ) ~ id - is-section-map-inv-left-unit-law-Σ a = refl + is-section-map-inv-left-unit-law-Σ = refl-htpy is-retraction-map-inv-left-unit-law-Σ : ( map-inv-left-unit-law-Σ ∘ map-left-unit-law-Σ) ~ id - is-retraction-map-inv-left-unit-law-Σ (pair star a) = refl + is-retraction-map-inv-left-unit-law-Σ = refl-htpy is-equiv-map-left-unit-law-Σ : is-equiv map-left-unit-law-Σ is-equiv-map-left-unit-law-Σ = @@ -83,16 +85,16 @@ module _ map-left-unit-law-product = pr2 map-inv-left-unit-law-product : A → unit × A - map-inv-left-unit-law-product = map-inv-left-unit-law-Σ (λ x → A) + map-inv-left-unit-law-product = map-inv-left-unit-law-Σ (λ _ → A) is-section-map-inv-left-unit-law-product : - ( map-left-unit-law-product ∘ map-inv-left-unit-law-product) ~ id + is-section map-left-unit-law-product map-inv-left-unit-law-product is-section-map-inv-left-unit-law-product = - is-section-map-inv-left-unit-law-Σ (λ x → A) + is-section-map-inv-left-unit-law-Σ (λ _ → A) is-retraction-map-inv-left-unit-law-product : - ( map-inv-left-unit-law-product ∘ map-left-unit-law-product) ~ id - is-retraction-map-inv-left-unit-law-product (pair star a) = refl + is-retraction map-left-unit-law-product map-inv-left-unit-law-product + is-retraction-map-inv-left-unit-law-product = refl-htpy is-equiv-map-left-unit-law-product : is-equiv map-left-unit-law-product is-equiv-map-left-unit-law-product = @@ -129,12 +131,12 @@ module _ pr2 (map-inv-right-unit-law-product a) = star is-section-map-inv-right-unit-law-product : - (map-right-unit-law-product ∘ map-inv-right-unit-law-product) ~ id - is-section-map-inv-right-unit-law-product a = refl + is-section map-right-unit-law-product map-inv-right-unit-law-product + is-section-map-inv-right-unit-law-product = refl-htpy is-retraction-map-inv-right-unit-law-product : - (map-inv-right-unit-law-product ∘ map-right-unit-law-product) ~ id - is-retraction-map-inv-right-unit-law-product (pair a star) = refl + is-retraction map-right-unit-law-product map-inv-right-unit-law-product + is-retraction-map-inv-right-unit-law-product = refl-htpy is-equiv-map-right-unit-law-product : is-equiv map-right-unit-law-product is-equiv-map-right-unit-law-product = @@ -159,15 +161,15 @@ module _ map-left-unit-law-Π f = f star map-inv-left-unit-law-Π : A star → ((t : unit) → A t) - map-inv-left-unit-law-Π a star = a + map-inv-left-unit-law-Π a _ = a is-section-map-inv-left-unit-law-Π : - ( map-left-unit-law-Π ∘ map-inv-left-unit-law-Π) ~ id - is-section-map-inv-left-unit-law-Π a = refl + is-section map-left-unit-law-Π map-inv-left-unit-law-Π + is-section-map-inv-left-unit-law-Π = refl-htpy is-retraction-map-inv-left-unit-law-Π : - ( map-inv-left-unit-law-Π ∘ map-left-unit-law-Π) ~ id - is-retraction-map-inv-left-unit-law-Π f = eq-htpy (λ star → refl) + is-retraction map-left-unit-law-Π map-inv-left-unit-law-Π + is-retraction-map-inv-left-unit-law-Π = refl-htpy is-equiv-map-left-unit-law-Π : is-equiv map-left-unit-law-Π is-equiv-map-left-unit-law-Π = @@ -208,12 +210,12 @@ module _ is-equiv-map-left-unit-law-function-type : is-equiv map-left-unit-law-function-type is-equiv-map-left-unit-law-function-type = - is-equiv-map-left-unit-law-Π λ _ → A + is-equiv-map-left-unit-law-Π (λ _ → A) is-equiv-map-inv-left-unit-law-function-type : is-equiv map-inv-left-unit-law-function-type is-equiv-map-inv-left-unit-law-function-type = - is-equiv-map-inv-left-unit-law-Π λ _ → A + is-equiv-map-inv-left-unit-law-Π (λ _ → A) left-unit-law-function-type : (unit → A) ≃ A left-unit-law-function-type = left-unit-law-Π (λ _ → A) diff --git a/src/orthogonal-factorization-systems/higher-modalities.lagda.md b/src/orthogonal-factorization-systems/higher-modalities.lagda.md index b44ca06b76..268ae3b349 100644 --- a/src/orthogonal-factorization-systems/higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/higher-modalities.lagda.md @@ -55,7 +55,7 @@ modalities in their most general form only make sense for ### Closure under identity type formers -We say that the [locally small type](foundation-core.identity-types.md) of a +We say that the [identity types](foundation-core.identity-types.md) of a [locally small type](foundation.locally-small-types.md) are **modal** if their [small equivalent](foundation-core.small-types.md) is modal. We say that a modality is closed under [identity type](foundation-core.identity-types.md) diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md index 8991458d44..a5b4c0921e 100644 --- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md @@ -1,6 +1,8 @@ # The universal cover of the circle ```agda +{-# OPTIONS --lossy-unification #-} + module synthetic-homotopy-theory.universal-cover-circle where ``` diff --git a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md index 5497bc58c2..54fb5a7daa 100644 --- a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md +++ b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md @@ -1345,20 +1345,20 @@ module _ λ s → np ( ( tr - ( λ y → - Id - ( i) - ( map-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))) - ( y))) - ( inv r1) - ( inv - ( right-computation-standard-transposition - ( has-decidable-equality-count eX) - ( np))) ∙ + ( λ y → + Id + ( i) + ( map-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( y))) + ( inv r1) + ( inv + ( right-computation-standard-transposition + ( has-decidable-equality-count eX) + ( np))) ∙ ( s ∙ r1)))) ( inl ( tr @@ -2334,13 +2334,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ - ( map-inv-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))))) - ( y))) + ( ( pr1 Y' + ( map-inv-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( y))))) ( P) ( inr ( inv @@ -2353,13 +2353,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( j))) + ( np))) + ( j)))) ( P) ( inl ( q ∙ @@ -2463,13 +2463,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( y))) + ( np))) + ( y)))) ( P) ( inr ( inv @@ -2482,13 +2482,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( ( pr1 Y') ∘ - ( map-inv-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))))) - ( i))) + ( pr1 Y' + ( map-inv-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( i)))) ( P) ( inl ( r ∙ @@ -2529,13 +2529,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( ( pr1 Y') ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( x))) + ( np))) + ( x)))) ( P) ( inl ( inv @@ -2548,13 +2548,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( ( pr1 Y') ∘ - ( map-inv-equiv - ( transposition - ( standard-2-Element-Decidable-Subtype - ( has-decidable-equality-count eX) - ( np))))) - ( j))) + ( pr1 Y' + ( map-inv-equiv + ( transposition + ( standard-2-Element-Decidable-Subtype + ( has-decidable-equality-count eX) + ( np))) + ( j)))) ( P) ( inr ( s ∙ @@ -2597,13 +2597,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( x))) + ( np))) + ( x)))) ( P) ( inl ( inv @@ -2616,13 +2616,13 @@ module _ ( tr ( λ Y' → type-Decidable-Prop - ( ( pr1 Y' ∘ + ( pr1 Y' ( map-inv-equiv ( transposition ( standard-2-Element-Decidable-Subtype ( has-decidable-equality-count eX) - ( np))))) - ( i))) + ( np))) + ( i)))) ( P) ( inr ( t ∙