feat(FiniteSupport): add extensionality

RedPRL · Nov 24, 2023 · 42389a3 · 42389a3
1 parent f784da3
commit 42389a3
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 10 deletions.
diff --git a/src/Mugen/Algebra/Displacement/FiniteSupport.agda b/src/Mugen/Algebra/Displacement/FiniteSupport.agda
@@ -150,3 +150,27 @@ module _
   fin-support-ordered-monoid : has-ordered-monoid (FiniteSupport 𝒟 cmp)
   fin-support-ordered-monoid = right-invariant→has-ordered-monoid (FiniteSupport 𝒟 cmp) λ {xs} {ys} {zs} xs≤ys →
     ⊎-mapl fin-support-list-path (≤-right-invariant 𝒟-ordered-monoid cmp (⊎-mapl (ap FinSupportList.support) xs≤ys))
+
+--------------------------------------------------------------------------------
+-- Extensionality based on 'finite-support-list' and eventually 'index-inj'
+-- from NearlyConst.
+
+module _ {o r}
+  {𝒟 : Displacement-algebra o r}
+  (let module 𝒟 = Displacement-algebra 𝒟)
+  {cmp : ∀ x y → Tri 𝒟._<_ x y}
+  where
+  module 𝒩 = NearlyConst 𝒟 cmp
+  open FinSupport 𝒟 cmp
+  open FinSupportList
+
+  Extensional-FinSupportList : ∀ {ℓr} ⦃ s : Extensional 𝒩.SupportList ℓr ⦄ → Extensional FinSupportList ℓr
+  Extensional-FinSupportList ⦃ s ⦄ .Pathᵉ xs ys = s .Pathᵉ (xs .support) (ys .support)
+  Extensional-FinSupportList ⦃ s ⦄ .reflᵉ xs = s .reflᵉ (xs .support)
+  Extensional-FinSupportList ⦃ s ⦄ .idsᵉ .to-path p = fin-support-list-path $ s .idsᵉ .to-path p
+  Extensional-FinSupportList ⦃ s ⦄ .idsᵉ .to-path-over p =
+    is-prop→pathp (λ _ → identity-system-hlevel 1 (s .idsᵉ) 𝒩.SupportList-is-set) _ p
+
+  instance
+    extensionality-fin-support-list : ∀ {ℓr} ⦃ s : Extensional ⌞ 𝒟 ⌟ ℓr ⦄ → Extensionality FinSupportList
+    extensionality-fin-support-list = record { lemma = quote Extensional-FinSupportList }
diff --git a/src/Mugen/Algebra/Displacement/NearlyConstant.agda b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
@@ -509,16 +509,6 @@ module _
 --------------------------------------------------------------------------------
 -- Extensionality based on 'index-inj'
 
--- this lemma should probably be put into 1lab
-private
-  identity-system-hlevel
-    : ∀ {ℓ ℓ'} {A : Type ℓ} n {R : A → A → Type ℓ'} {r : ∀ x → R x x}
-    → is-identity-system R r
-    → is-hlevel A (suc n)
-    → ∀ {x y : A} → is-hlevel (R x y) n
-  identity-system-hlevel n ids hl {x} {y} =
-    is-hlevel≃ n (identity-system-gives-path ids) (Path-is-hlevel' n hl x y)
-
 -- 1lab's or Agda's instance search somehow does not seem to deal with
 -- explicit arguments, so we re-parametrize things with implicit '𝒟' and 'cmp'.
 module _ {o r}

diff --git a/src/Mugen/Prelude.agda b/src/Mugen/Prelude.agda
@@ -61,3 +61,13 @@ x |> f = f x
 
 over : ∀ {ℓ} {A : Type ℓ} {x y : A} {f : A → A} → (∀ x → f x ≡ x) → f x ≡ f y → x ≡ y
 over {x = x} {y = y} p q =  sym (p x) ·· q ·· p y
+
+--------------------------------------------------------------------------------
+-- This lemma should probably be put into 1lab
+identity-system-hlevel
+  : ∀ {ℓ ℓ'} {A : Type ℓ} n {R : A → A → Type ℓ'} {r : ∀ x → R x x}
+  → is-identity-system R r
+  → is-hlevel A (suc n)
+  → ∀ {x y : A} → is-hlevel (R x y) n
+identity-system-hlevel n ids hl {x} {y} =
+  is-hlevel≃ n (identity-system-gives-path ids) (Path-is-hlevel' n hl x y)