make uniqueness defintions abstract

UniMath · Sep 12, 2023 · 63c807b · 63c807b
1 parent 4689d54
commit 63c807b
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 26 deletions.
diff --git a/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md b/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md
@@ -53,15 +53,16 @@ module _
   {B : UU l3} (f : type-subuniverse P → B)
   where
 
-  unique-action-equiv-function-subuniverse :
-    (X : type-subuniverse P) →
-    is-contr
-      ( Σ ( (Y : type-subuniverse P) → equiv-subuniverse P X Y → f X ＝ f Y)
-          ( λ h → h X id-equiv ＝ refl))
-  unique-action-equiv-function-subuniverse X =
-    is-contr-map-ev-id-equiv-subuniverse P X
-      ( λ Y e → f X ＝ f Y)
-      ( refl)
+  abstract
+    unique-action-equiv-function-subuniverse :
+      (X : type-subuniverse P) →
+      is-contr
+        ( Σ ( (Y : type-subuniverse P) → equiv-subuniverse P X Y → f X ＝ f Y)
+            ( λ h → h X id-equiv ＝ refl))
+    unique-action-equiv-function-subuniverse X =
+      is-contr-map-ev-id-equiv-subuniverse P X
+        ( λ Y e → f X ＝ f Y)
+        ( refl)
 
   action-equiv-function-subuniverse :
     (X Y : type-subuniverse P) → equiv-subuniverse P X Y → f X ＝ f Y

diff --git a/src/foundation/action-on-equivalences-functions.lagda.md b/src/foundation/action-on-equivalences-functions.lagda.md
@@ -42,13 +42,15 @@ module _
   {l1 l2 : Level} {B : UU l2} (f : UU l1 → B)
   where
 
-  unique-action-equiv-function :
-    (X : UU l1) →
-    is-contr (Σ ((Y : UU l1) → X ≃ Y → f X ＝ f Y) (λ h → h X id-equiv ＝ refl))
-  unique-action-equiv-function X =
-    is-contr-map-ev-id-equiv
-      ( λ Y e → f X ＝ f Y)
-      ( refl)
+  abstract
+    unique-action-equiv-function :
+      (X : UU l1) →
+      is-contr
+        ( Σ ((Y : UU l1) → X ≃ Y → f X ＝ f Y) (λ h → h X id-equiv ＝ refl))
+    unique-action-equiv-function X =
+      is-contr-map-ev-id-equiv
+        ( λ Y e → f X ＝ f Y)
+        ( refl)
 
   action-equiv-function :
     {X Y : UU l1} → X ≃ Y → f X ＝ f Y

diff --git a/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md b/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md
@@ -41,11 +41,13 @@ module _
   ( P : subuniverse l1 l2) (B : type-subuniverse P → UU l3)
   where
 
-  unique-action-equiv-family-over-subuniverse :
-    (X : type-subuniverse P) →
-    is-contr (fiber (ev-id-equiv-subuniverse P X {λ Y e → B X ≃ B Y}) id-equiv)
-  unique-action-equiv-family-over-subuniverse X =
-    is-contr-map-ev-id-equiv-subuniverse P X (λ Y e → B X ≃ B Y) id-equiv
+  abstract
+    unique-action-equiv-family-over-subuniverse :
+      (X : type-subuniverse P) →
+      is-contr
+        ( fiber (ev-id-equiv-subuniverse P X {λ Y e → B X ≃ B Y}) id-equiv)
+    unique-action-equiv-family-over-subuniverse X =
+      is-contr-map-ev-id-equiv-subuniverse P X (λ Y e → B X ≃ B Y) id-equiv
 
   action-equiv-family-over-subuniverse :
     (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y

diff --git a/src/foundation/action-on-equivalences-type-families.lagda.md b/src/foundation/action-on-equivalences-type-families.lagda.md
@@ -64,11 +64,12 @@ module _
   {l1 l2 : Level} (B : UU l1 → UU l2)
   where
 
-  unique-action-equiv-family :
-    {X : UU l1} →
-    is-contr (fiber (ev-id-equiv (λ Y e → B X ≃ B Y)) id-equiv)
-  unique-action-equiv-family =
-    is-contr-map-ev-id-equiv (λ Y e → B _ ≃ B Y) id-equiv
+  abstract
+    unique-action-equiv-family :
+      {X : UU l1} →
+      is-contr (fiber (ev-id-equiv (λ Y e → B X ≃ B Y)) id-equiv)
+    unique-action-equiv-family =
+      is-contr-map-ev-id-equiv (λ Y e → B _ ≃ B Y) id-equiv
 
   action-equiv-family :
     {X Y : UU l1} → (X ≃ Y) → B X ≃ B Y