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
 ```
 
 </details>
@@ -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 ∙