Global: porting classes from formal-prelude

Author: omelkonian

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 renamed to 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 renamed to 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