refactor: use the singleton poset from the upstream

RedPRL · Jun 14, 2024 · 8e3e0c8 · 8e3e0c8
1 parent f0c9ed2
commit 8e3e0c8
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 16 deletions.
diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda
@@ -23,7 +23,6 @@ open import Mugen.Cat.HierarchyTheory.McBride
 open import Mugen.Order.StrictOrder
 open import Mugen.Order.Instances.Endomorphism renaming (Endomorphism to Endomorphism-poset)
 open import Mugen.Order.Instances.LeftInvariantRightCentered
-open import Mugen.Order.Instances.Singleton
 
 import Mugen.Order.Reasoning as Reasoning
 
@@ -55,7 +54,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
 
   -- made public for the naturality proof in a different file
   Δ⁺ : Poset o r
-  Δ⁺ = ◆ {o = o} {r = r} ⊎ᵖ (Δ ⊎ᵖ Δ)
+  Δ⁺ = 𝟙ᵖ {o = o} {ℓ = r} ⊎ᵖ (Δ ⊎ᵖ Δ)
 
   private
     H⟨Δ⁺⟩ : Poset o r
@@ -109,7 +108,7 @@ module Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
 
   pattern ι₀ α = inl α
 
-  ι₀-hom : Hom ◆ Δ⁺
+  ι₀-hom : Hom 𝟙ᵖ Δ⁺
   ι₀-hom .hom = ι₀
   ι₀-hom .pres-≤[]-equal α≤β = lift α≤β , λ _ → refl
 

diff --git a/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda b/src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbeddingNaturality.agda
@@ -25,7 +25,6 @@ open import Mugen.Order.StrictOrder
 open import Mugen.Order.Instances.Endomorphism renaming (Endomorphism to Endomorphism-poset)
 open import Mugen.Order.Instances.LeftInvariantRightCentered
 open import Mugen.Order.Instances.Lift
-open import Mugen.Order.Instances.Singleton
 
 import Mugen.Order.Reasoning as Reasoning
 

diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda
@@ -49,7 +49,6 @@ import Mugen.Order.Instances.Opposite
 import Mugen.Order.Instances.Pointwise
 import Mugen.Order.Instances.Prefix
 import Mugen.Order.Instances.Product
-import Mugen.Order.Instances.Singleton
 import Mugen.Order.Instances.Support
 import Mugen.Order.Lattice
 import Mugen.Order.Reasoning

diff --git a/src/Mugen/Order/Instances/Singleton.agda b/src/Mugen/Order/Instances/Singleton.agda