diff --git a/Cubical/Relation/Binary/Order/Poset/Subset.agda b/Cubical/Relation/Binary/Order/Poset/Subset.agda index 8a5387a6d..9153602a4 100644 --- a/Cubical/Relation/Binary/Order/Poset/Subset.agda +++ b/Cubical/Relation/Binary/Order/Poset/Subset.agda @@ -22,7 +22,7 @@ open import Cubical.Relation.Binary.Order.Poset.Properties private variable ℓ ℓ' ℓ'' ℓ''' ℓ₀ ℓ₁ : Level - + module _ (P : Poset ℓ ℓ') where