Fix Allable/Anyable + instances for List⁺

Author: omelkonian

Class/Allable/Core.agda

@@ -2,12 +2,12 @@ module Class.Allable.Core where
 
 open import Class.Prelude
 
-record Allable (F : Set ℓ → Set ℓ) : Set (lsuc ℓ) where
-  field All : ∀ {A} → (A → Set) → F A → Set ℓ
+record Allable (F : Type ℓ → Type ℓ) : Typeω where
+  field All : ∀ {A} → (A → Type ℓ′) → F A → Type (ℓ ⊔ ℓ′)
 
   ∀∈-syntax   = All
   ∀∈-syntax′  = All
-  ¬∀∈-syntax  = λ {A} P → ¬_ ∘ All {A} P
+  ¬∀∈-syntax  = λ {A} {ℓ′} (P : A → Type ℓ′) → ¬_ ∘ All P
   ¬∀∈-syntax′ = ¬∀∈-syntax
   infix 2 ∀∈-syntax ∀∈-syntax′ ¬∀∈-syntax ¬∀∈-syntax′
   syntax ∀∈-syntax   P         xs = ∀[∈     xs ] P

Class/Allable/Instance.agda

@@ -17,6 +17,9 @@ instance
   Allable-Maybe : Allable {ℓ} Maybe
   Allable-Maybe .All = M.All
 
+  Allable-List⁺ : Allable {ℓ} List⁺
+  Allable-List⁺ .All P = All P ∘ toList
+
 private
   open import Class.Decidable
   open import Class.HasOrder

Class/Anyable/Core.agda

@@ -2,12 +2,12 @@ module Class.Anyable.Core where
 
 open import Class.Prelude
 
-record Anyable (F : Set ℓ → Set ℓ) : Set (lsuc ℓ) where
-  field Any : ∀ {A} → (A → Set) → F A → Set ℓ
+record Anyable (F : Type ℓ → Type ℓ) : Typeω where
+  field Any : ∀ {A} → (A → Type ℓ′) → F A → Type (ℓ ⊔ ℓ′)
 
   ∃∈-syntax  = Any
   ∃∈-syntax′ = Any
-  ∄∈-syntax  = λ {A} P → ¬_ ∘ Any {A} P
+  ∄∈-syntax  = λ {A} {ℓ′} (P : A → Type ℓ′) → ¬_ ∘ Any P
   ∄∈-syntax′ = ∄∈-syntax
   infix 2 ∃∈-syntax ∃∈-syntax′ ∄∈-syntax ∄∈-syntax′
   syntax ∃∈-syntax  P         xs = ∃[∈    xs ] P

Class/Anyable/Instance.agda

@@ -17,6 +17,9 @@ instance
   Anyable-Maybe : Anyable {ℓ} Maybe
   Anyable-Maybe .Any = M.Any
 
+  Anyable-List⁺ : Anyable {ℓ} List⁺
+  Anyable-List⁺ .Any P = Any P ∘ toList
+
 private
   open import Class.Decidable
   open import Class.HasOrder

Class/Prelude.agda

@@ -37,7 +37,7 @@ open import Data.Maybe public
 open import Data.List public
   using (List; []; _∷_; [_]; map; _++_; foldr; concat; concatMap)
 open import Data.List.NonEmpty public
-  using (List⁺; _∷_; _⁺++⁺_; foldr₁)
+  using (List⁺; _∷_; _⁺++⁺_; foldr₁; toList)
 open import Data.Vec public
   using (Vec; []; _∷_)
 open import Data.These public