From b02e8391802c4f1ab3d6c8e9289c06403bac04b4 Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 10 Dec 2023 08:27:40 -0600 Subject: [PATCH] fix: better argument passing for extensionality --- src/Mugen/Order/Instances/BasedSupport.agda | 14 +++++++++++--- src/Mugen/Order/Instances/Support.agda | 13 +++++++++---- 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/src/Mugen/Order/Instances/BasedSupport.agda b/src/Mugen/Order/Instances/BasedSupport.agda index d5c009b..bd0cbeb 100644 --- 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 index ffa1ae2..143ae84 100644 --- 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 ε)