Global: porting classes from formal-prelude

Class/Allable.agda

@@ -1,4 +1,5 @@
+{-# OPTIONS --cubical-compatible #-}
 module Class.Allable where
 
 open import Class.Allable.Core public
-open import Class.Allable.Instance public
+open import Class.Allable.Instances public

Class/Allable/Core.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible #-}
 module Class.Allable.Core where
 
 open import Class.Prelude

Class/Allable/Instance.agda → Class/Allable/Instances.agda

@@ -1,4 +1,5 @@
-module Class.Allable.Instance where
+{-# OPTIONS --cubical-compatible #-}
+module Class.Allable.Instances where
 
 open import Class.Prelude
 open import Class.Allable.Core
@@ -18,20 +19,4 @@ instance
   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
-
-  _ : ∀[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0
-  _ = auto
-
-  _ : ∀[ x ∈ just 42 ] x > 0
-  _ = auto
-
-  _ : ∀[ x ∈ nothing ] x > 0
-  _ = auto
-
-  _ : ¬∀[ x ∈ just 0 ] x > 0
-  _ = auto
+  Allable-List⁺ .All P = All P ∘ L⁺.toList

Class/Anyable.agda

@@ -1,4 +1,5 @@
+{-# OPTIONS --cubical-compatible #-}
 module Class.Anyable where
 
 open import Class.Anyable.Core public
-open import Class.Anyable.Instance public
+open import Class.Anyable.Instances public

Class/Anyable/Core.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible #-}
 module Class.Anyable.Core where
 
 open import Class.Prelude

Class/Anyable/Instance.agda → Class/Anyable/Instances.agda

@@ -1,4 +1,5 @@
-module Class.Anyable.Instance where
+{-# OPTIONS --cubical-compatible #-}
+module Class.Anyable.Instances where
 
 open import Class.Prelude
 open import Class.Anyable.Core
@@ -18,17 +19,4 @@ instance
   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
-
-  _ : ∃[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0
-  _ = auto
-
-  _ : ∃[ x ∈ just 42 ] x > 0
-  _ = auto
-
-  _ : ∄[ x ∈ nothing ] x > 0
-  _ = auto
+  Anyable-List⁺ .Any P = Any P ∘ L⁺.toList

Class/Applicative/Instances.agda

@@ -49,7 +49,8 @@ instance
   -- Applicative-∃Vec : Applicative (∃ ∘ Vec)
   -- Applicative-∃Vec = λ where
   --   .pure x → 1 , pure x
-  --   ._<*>_ (n , xs) (m , ys) → {! (n ⊔ m) , zipWith _$_ xs ys  -- (+ zipWith-⊔ lemma) !}
+  --   ._<*>_ (n , xs) (m , ys) →
+  --     {! (n ⊔ m) , zipWith _$_ xs ys (+ zipWith-⊔ lemma) !}
 
   private module M where
     open import Reflection.TCM.Syntax public

Class/Coercions.agda

@@ -0,0 +1,19 @@
+{-# OPTIONS --cubical-compatible #-}
+module Class.Coercions where
+
+open import Class.Prelude
+
+infix -1 _↝_
+record _↝_ (A : Type ℓ) (B : Type ℓ′) : Typeω where
+  field to : A → B
+  syntax to {B = B} = to[ B ]
+open _↝_ ⦃...⦄ public
+
+tos : ⦃ A ↝ B ⦄ → List A ↝ List B
+tos .to = map to
+
+infix -1 _⁇_↝_
+record _⁇_↝_ (A : Type ℓ) (P : Pred A ℓ′) (B : Type ℓ′) : Typeω where
+  field toBecause : (x : A) .{_ : P x} → B
+  syntax toBecause x {p} = ⌞ x ⊣ p ⌟
+open _⁇_↝_ ⦃...⦄ public

Class/DecEq/Core.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.DecEq.Core where
 
 open import Class.Prelude
@@ -20,3 +20,6 @@ open DecEq ⦃...⦄ public
 DecEq¹ = DecEq ¹
 DecEq² = DecEq ²
 DecEq³ = DecEq ³
+
+Irrelevant⇒DecEq : Irrelevant A → DecEq A
+Irrelevant⇒DecEq ∀≡ ._≟_ = yes ∘₂ ∀≡

Class/Decidable.agda

@@ -3,3 +3,4 @@ module Class.Decidable where
 
 open import Class.Decidable.Core public
 open import Class.Decidable.Instances public
+open import Class.Decidable.WithoutK public

Class/Decidable/Core.agda

@@ -1,11 +1,11 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Decidable.Core where
 
+open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse)
+
 open import Class.Prelude
 open import Class.Core
 
-open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse)
-
 record _⁇ (P : Type ℓ) : Type ℓ where
   constructor ⁇_
   field dec : Dec P
@@ -24,13 +24,6 @@ open _⁇ ⦃...⦄ public
 ¿_¿ᵇ : (P : Type ℓ) → ⦃ P ⁇ ⦄ → Bool
 ¿ P ¿ᵇ = ⌊ ¿ P ¿ ⌋
 
-infix 0 ifᵈ_then_else_
-ifᵈ_then_else_ : ∀ {X : Type ℓ} (P : Type ℓ′)
-  → ⦃ P ⁇ ⦄ → ({_ : P} → X) → ({_ : ¬ P} → X) → X
-ifᵈ P then t else f with ¿ P ¿
-... | yes p = t {p}
-... | no ¬p = f {¬p}
-
 _⁇¹ = _⁇ ¹
 _⁇² = _⁇ ²
 _⁇³ = _⁇ ³

Class/Decidable/Instances.agda

@@ -1,19 +1,14 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Decidable.Instances where
 
 open import Class.Prelude
 open import Class.Decidable.Core
 open import Class.DecEq.Core
 
-private variable
-  n : ℕ
-  x : A
-  P Q : Pred A ℓ
-  R : Rel A ℓ
-
 instance
 
   -- ** deriving from DecEq
+
   DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇²
   DecEq⇒Dec = ⁇² _≟_
 
@@ -40,19 +35,6 @@ instance
   Dec-⊎ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A ⊎ B) ⁇
   Dec-⊎ .dec = dec D.⊎-dec dec
 
-  import Data.Sum.Relation.Unary.All as ⊎; open ⊎ using (inj₁; inj₂)
-  open import Relation.Nullary.Decidable using () renaming (map′ to mapDec)
-
-  Dec-⊎All : ⦃ P ⁇¹ ⦄ → ⦃ Q ⁇¹ ⦄ → ⊎.All P Q ⁇¹
-  Dec-⊎All {P = P} {Q = Q} {x = inj₁ x} .dec = mapDec inj₁ inj₁˘ ¿ P x ¿
-    where inj₁˘ : ⊎.All P Q (inj₁ x) → P x
-          inj₁˘ (inj₁ x) = x
-  Dec-⊎All {P = P} {Q = Q} {x = inj₂ y} .dec = mapDec inj₂ inj₂˘ ¿ Q y ¿
-    where inj₂˘ : ⊎.All P Q (inj₂ x) → Q x
-          inj₂˘ (inj₂ x) = x
-
-  import Data.Bool as 𝔹
-
   Dec-T : T ⁇¹
   Dec-T = ⁇¹ 𝔹.T?
 
@@ -70,7 +52,6 @@ instance
   Dec-AllPairs : ⦃ R ⁇² ⦄ → AP.AllPairs R ⁇¹
   Dec-AllPairs = ⁇¹ AP.allPairs? dec²
 
-  open import Data.Vec as V
   open import Data.Vec.Relation.Unary.All as V
   open import Data.Vec.Relation.Unary.Any as V
 
@@ -80,22 +61,19 @@ instance
   Dec-VAny : ⦃ P ⁇¹ ⦄ → V.Any P {n} ⁇¹
   Dec-VAny = ⁇¹ V.any? dec¹
 
-  import Data.Maybe as M
-  import Data.Maybe.Relation.Unary.All as M renaming (dec to all?)
-  import Data.Maybe.Relation.Unary.Any as M renaming (dec to any?)
+  import Data.Maybe.Relation.Unary.All as Mb renaming (dec to all?)
+  import Data.Maybe.Relation.Unary.Any as Mb renaming (dec to any?)
 
-  Dec-MAll : ⦃ P ⁇¹ ⦄ → M.All P ⁇¹
-  Dec-MAll = ⁇¹ M.all? dec¹
+  Dec-MAll : ⦃ P ⁇¹ ⦄ → Mb.All P ⁇¹
+  Dec-MAll = ⁇¹ Mb.all? dec¹
 
-  Dec-MAny : ⦃ P ⁇¹ ⦄ → M.Any P ⁇¹
-  Dec-MAny = ⁇¹ M.any? dec¹
+  Dec-MAny : ⦃ P ⁇¹ ⦄ → Mb.Any P ⁇¹
+  Dec-MAny = ⁇¹ Mb.any? dec¹
 
   -- ** inequalities
 
-  import Data.Nat.Properties as ℕ
-
-  ℕ-Dec-≤ = ⁇² ℕ._≤?_
-  ℕ-Dec-< = ⁇² ℕ._<?_
+  ℕ-Dec-≤ = ⁇² Nat._≤?_
+  ℕ-Dec-< = ⁇² Nat._<?_
 
   import Data.Integer.Properties as ℤ
 

Class/Decidable/WithoutK.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --without-K #-}
+module Class.Decidable.WithoutK where
+
+open import Class.Prelude
+open import Class.Decidable.Core
+
+infix 0 ifᵈ_then_else_
+ifᵈ_then_else_ : ∀ {X : Type ℓ} (P : Type ℓ′)
+  → ⦃ P ⁇ ⦄ → ({_ : P} → X) → ({_ : ¬ P} → X) → X
+ifᵈ P then t else f with ¿ P ¿
+... | yes p = t {p}
+... | no ¬p = f {¬p}
+
+instance
+  import Data.Sum.Relation.Unary.All as ⊎; open ⊎ using (inj₁; inj₂)
+
+  Dec-⊎All : ⦃ P ⁇¹ ⦄ → ⦃ Q ⁇¹ ⦄ → ⊎.All P Q ⁇¹
+  Dec-⊎All {P = P} {Q = Q} {x = inj₁ x} .dec = mapDec inj₁ inj₁˘ ¿ P x ¿
+    where inj₁˘ : ∀ {x} → ⊎.All P Q (inj₁ x) → P x
+          inj₁˘ (inj₁ x) = x
+  Dec-⊎All {P = P} {Q = Q} {x = inj₂ y} .dec = mapDec inj₂ inj₂˘ ¿ Q y ¿
+    where inj₂˘ : ∀ {x} → ⊎.All P Q (inj₂ x) → Q x
+          inj₂˘ (inj₂ x) = x

Class/Default.agda

@@ -5,49 +5,5 @@
 {-# OPTIONS --cubical-compatible #-}
 module Class.Default where
 
-open import Class.Prelude
-import Data.Vec as V
-
-record Default (A : Type ℓ) : Type ℓ where
-  constructor ⌞_⌟
-  field def : A
-open Default ⦃...⦄ public
-
-private variable n : ℕ
-
-instance
-  Default-⊤ : Default ⊤
-  Default-⊤ = ⌞ tt ⌟
-
-  Default-× : ⦃ Default A ⦄ → ⦃ Default B ⦄ → Default (A × B)
-  Default-× = ⌞ def , def ⌟
-
-  Default-⊎ : ⦃ Default A ⦄ → ⦃ Default B ⦄ → Default (A ⊎ B)
-  Default-⊎ = ⌞ inj₁ def ⌟
-
-  Default-Maybe : Default (Maybe A)
-  Default-Maybe = ⌞ nothing ⌟
-
-  Default-Bool : Default Bool
-  Default-Bool = ⌞ true ⌟
-
-  Default-ℕ : Default ℕ
-  Default-ℕ = ⌞ zero ⌟
-
-  Default-ℤ : Default ℤ
-  Default-ℤ = ⌞ ℤ.pos def ⌟
-
-  Default-Fin : Default (Fin (suc n))
-  Default-Fin = ⌞ zero ⌟
-
-  Default-List : Default (List A)
-  Default-List = ⌞ [] ⌟
-
-  Default-Vec-zero : Default (Vec A 0)
-  Default-Vec-zero = ⌞ V.[] ⌟
-
-  Default-Vec-suc : ⦃ Default A ⦄ → Default (Vec A (suc n))
-  Default-Vec-suc = ⌞ V.replicate _ def ⌟
-
-  Default-→ : ⦃ Default B ⦄ → Default (A → B)
-  Default-→ = ⌞ const def ⌟
+open import Class.Default.Core public
+open import Class.Default.Instances public

Class/Default/Core.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical-compatible #-}
+module Class.Default.Core where
+
+open import Class.Prelude
+
+record Default (A : Type ℓ) : Type ℓ where
+  field def : A
+open Default ⦃...⦄ public

Class/Default/Instances.agda

@@ -0,0 +1,27 @@
+{-# OPTIONS --cubical-compatible #-}
+module Class.Default.Instances where
+
+open import Class.Prelude
+open import Class.Default.Core
+
+instance
+  Default-⊤ = Default ⊤    ∋ λ where .def → tt
+  Default-𝔹 = Default Bool ∋ λ where .def → true
+  Default-ℕ = Default ℕ    ∋ λ where .def → zero
+  Default-ℤ = Default ℤ    ∋ λ where .def → ℤ.pos def
+
+  Default-Maybe : Default (Maybe A)
+  Default-Maybe .def = nothing
+
+  Default-List : Default (List A)
+  Default-List .def = []
+
+  Default-Fin : Default (Fin (suc n))
+  Default-Fin .def = Fin.zero
+
+  Default-→ : ⦃ Default B ⦄ → Default (A → B)
+  Default-→ .def = const def
+
+  module _ ⦃ _ : Default A ⦄ ⦃ _ : Default B ⦄ where
+    Default-× = Default (A × B) ∋ λ where .def → def , def
+    Default-⊎ = Default (A ⊎ B) ∋ λ where .def → inj₁ def

Class/Foldable/Core.agda

@@ -9,4 +9,20 @@ open import Class.Monoid
 
 record Foldable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
   field fold : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A
+
+  foldMap : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B
+  foldMap f = fold ∘ fmap f
+
 open Foldable ⦃...⦄ public
+
+record Foldable′ (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
+  field foldMap′ : ⦃ _ : Semigroup B ⦄ → ⦃ Monoid B ⦄ → (A → B) → F A → B
+
+  fold′ : ⦃ _ : Semigroup A ⦄ → ⦃ Monoid A ⦄ → F A → A
+  fold′ = foldMap′ id
+
+open Foldable′ ⦃...⦄ public
+
+Foldable′⇒Foldable : ⦃ _ : Functor F ⦄ → Foldable′ F → Foldable F
+Foldable′⇒Foldable f = let instance _ = f in
+  λ where .fold → fold′

Class/Foldable/Instances.agda

@@ -9,7 +9,10 @@ open import Class.Foldable.Core
 
 instance
   Foldable-List : Foldable List
-  Foldable-List .fold = go where go = λ where
-    [] → ε
-    (x ∷ []) → x
-    (x ∷ xs@(_ ∷ _)) → x ◇ go xs
+  Foldable-List .fold = foldr _◇_ ε
+
+  Foldable-Maybe : Foldable Maybe
+  Foldable-Maybe .fold = fromMaybe ε
+
+  Foldable-List⁺ : Foldable List⁺
+  Foldable-List⁺ .fold (x ∷ xs) = x ◇ fold xs