Move PosetDownset to where principalDownsets are

agda · Sep 8, 2024 · cab1808 · cab1808
1 parent 4d669c1
commit cab1808
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 17 deletions.
diff --git a/Cubical/Algebra/DistLattice/Downset.agda b/Cubical/Algebra/DistLattice/Downset.agda
@@ -16,6 +16,7 @@ open import Cubical.Algebra.Lattice
 open import Cubical.Algebra.DistLattice.Base
 
 open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Poset.Mappings
 
 open Iso
 
@@ -44,7 +45,7 @@ module DistLatticeDownset (L' : DistLattice ℓ) where
       _ = LPoset .snd
 
   ↓ᴰᴸ : L → DistLattice ℓ
-  fst (↓ᴰᴸ u) = ↓ u
+  fst (↓ᴰᴸ u) = principalDownset IndPoset u .fst
   DistLatticeStr.0l (snd (↓ᴰᴸ u)) = 0l , ∨lLid u
   DistLatticeStr.1l (snd (↓ᴰᴸ u)) = u , is-refl u
   DistLatticeStr._∨l_ (snd (↓ᴰᴸ u)) (v , v≤u) (w , w≤u) =

diff --git a/Cubical/Relation/Binary/Order/Poset/Mappings.agda b/Cubical/Relation/Binary/Order/Poset/Mappings.agda
@@ -339,6 +339,32 @@ module _
         isPrincipalUpset→isUpset : isPrincipalUpset → (isUpset S)
         isPrincipalUpset→isUpset (x , p) = transport⁻ (cong isUpset p) (isUpsetPrincipalUpset x)
 
+module PosetDownset (P' : Poset ℓ ℓ') where
+  private P = ⟨ P' ⟩
+  open PosetStr (snd P')
+
+  ↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
+  fst (↓ᴾ u) = principalDownset P' u .fst
+  PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst
+  PosetStr.isPoset (snd (↓ᴾ u)) =
+    isPosetInduced
+      (PosetStr.isPoset (snd P'))
+       _
+      (principalDownset P' u .snd)
+
+module PosetUpset (P' : Poset ℓ ℓ') where
+  private P = ⟨ P' ⟩
+  open PosetStr (snd P')
+
+  ↑ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
+  fst (↑ᴾ u) = principalUpset P' u .fst
+  PosetStr._≤_ (snd (↑ᴾ u)) v w = v .fst ≤ w .fst
+  PosetStr.isPoset (snd (↑ᴾ u)) =
+    isPosetInduced
+      (PosetStr.isPoset (snd P'))
+       _
+      (principalUpset P' u .snd)
+
 -- Isotone maps are characterized by their actions on down-sets and up-sets
 module _
   {P : Poset ℓ₀ ℓ₀'}

diff --git a/Cubical/Relation/Binary/Order/Poset/Properties.agda b/Cubical/Relation/Binary/Order/Poset/Properties.agda
@@ -97,22 +97,6 @@ Poset→Proset (_ , pos)
   = proset _ (PosetStr._≤_ pos)
              (isPoset→isProset (PosetStr.isPoset pos))
 
-module PosetDownset (P' : Poset ℓ ℓ') where
-  private P = fst P'
-  open PosetStr (snd P')
-
-  ↓ : P → Type (ℓ-max ℓ ℓ')
-  ↓ u = Σ[ v ∈ P ] v ≤ u
-
-  ↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
-  fst (↓ᴾ u) = ↓ u
-  PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst
-  PosetStr.isPoset (snd (↓ᴾ u)) =
-    isPosetInduced
-      (PosetStr.isPoset (snd P'))
-      _
-      (EmbeddingΣProp (λ a → is-prop-valued _ _))
-
 Poset→Quoset : Poset ℓ ℓ' → Quoset ℓ (ℓ-max ℓ ℓ')
 Poset→Quoset (_ , pos)
   = quoset _ (BinaryRelation.IrreflKernel (PosetStr._≤_ pos))