display forms for dcpos

the1lab · Sep 18, 2024 · fd4b816 · fd4b816
1 parent 316ec0c
commit fd4b816
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/Order/DCPO.lagda.md b/src/Order/DCPO.lagda.md
@@ -237,7 +237,7 @@ module DCPOs {o ℓ : Level} = Cat.Reasoning (DCPOs o ℓ)
 DCPO : (o ℓ : Level) → Type _
 DCPO o ℓ = DCPOs.Ob {o} {ℓ}
 
-DCPOs↪Posets : ∀ {o ℓ} → Functor (DCPOs o ℓ) (Posets o ℓ) 
+DCPOs↪Posets : ∀ {o ℓ} → Functor (DCPOs o ℓ) (Posets o ℓ)
 DCPOs↪Posets = Forget-subcat
 
 DCPOs↪Sets : ∀ {o ℓ} → Functor (DCPOs o ℓ) (Sets o)
@@ -261,15 +261,15 @@ module DCPO {o ℓ} (D : DCPO o ℓ) where
  poset : Poset o ℓ
  poset = D .fst
 
- open Order.Reasoning poset public
+ open Order.Reasoning (D .fst) public
 
  set : Set o
  set = el ⌞ D ⌟ Ob-is-set
 
  has-dcpo : is-dcpo poset
  has-dcpo = D .snd
 
- open is-dcpo has-dcpo public
+ open is-dcpo (D .snd) public
 
  ⋃-pointwise
  : ∀ {Ix} {s s' : Ix → Ob}