fix: better argument passing for extensionality

RedPRL · Dec 10, 2023 · b02e839 · b02e839
1 parent c0085df
commit b02e839
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 7 deletions.
diff --git a/src/Mugen/Order/Instances/BasedSupport.agda b/src/Mugen/Order/Instances/BasedSupport.agda
@@ -362,11 +362,19 @@ module _
 --------------------------------------------------------------------------------
 -- Extensionality
 
-module _ {A : Type o} ⦃ _ : H-Level A 2 ⦄ {ℓr} ⦃ s : Extensional (Nat → ⌞ A ⌟) ℓr ⦄ where
+module _ {A : Type o} {ℓr} ⦃ s : Extensional (Nat → A) ℓr ⦄ where
 
-  Extensional-BasedSupportList : Extensional (BasedSupportList ⌞ A ⌟) ℓr
-  Extensional-BasedSupportList = injection→extensional! index-injective s
+  Extensional-BasedSupportList
+    : {@(tactic hlevel-tactic-worker) A-is-set : is-set A}
+    → Extensional (BasedSupportList A) ℓr
+  Extensional-BasedSupportList {A-is-set} =
+    injection→extensional! {sb = Π-is-hlevel 2 λ _ → A-is-set} index-injective s
 
   instance
     extensionality-based-support-list : Extensionality (BasedSupportList ⌞ A ⌟)
     extensionality-based-support-list = record { lemma = quote Extensional-BasedSupportList }
+
+private
+  open import Data.Nat
+  _ : (f : BasedSupportList Nat) → f ≡ f
+  _ = λ f → ext λ _ → refl
diff --git a/src/Mugen/Order/Instances/Support.agda b/src/Mugen/Order/Instances/Support.agda
@@ -110,10 +110,15 @@ module _
 --------------------------------------------------------------------------------
 -- Extensionality
 
-module _ {A : Type o} ⦃ _ : H-Level A 2 ⦄ {ε : ⌞ A ⌟} {ℓr} ⦃ s : Extensional (BasedSupportList ⌞ A ⌟) ℓr ⦄ where
-
-  Extensional-FiniteSupportList : Extensional (SupportList ε) ℓr
-  Extensional-FiniteSupportList = injection→extensional! (supp-to-based-is-injective hlevel!) s
+module _ {A : Type o} {ε : ⌞ A ⌟} {ℓr} ⦃ s : Extensional (BasedSupportList ⌞ A ⌟) ℓr ⦄ where
+
+  Extensional-FiniteSupportList
+    : {@(tactic hlevel-tactic-worker) A-is-set : is-set A}
+    → Extensional (SupportList ε) ℓr
+  Extensional-FiniteSupportList {A-is-set} =
+    injection→extensional!
+      {sb = BasedSupportList-is-hlevel 0 A-is-set}
+      (supp-to-based-is-injective A-is-set) s
 
   instance
     extensionality-finite-support-list : Extensionality (SupportList ε)