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

@@ -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": {

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/

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 =

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
 ```
 

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