Merge Class and Interface modules

Author: WhatisRT

Class/Applicative.agda

@@ -1,7 +1,5 @@
--- {-# OPTIONS --safe #-}
+{-# OPTIONS --safe --without-K #-}
 module Class.DecEq where
 
 open import Class.DecEq.Core public
 open import Class.DecEq.Instances public
-open import Class.DecEq.WithK public
-open import Class.DecEq.Derive public

Class/Applicative/Core.agda

@@ -6,11 +6,11 @@ open import Data.Bool using (Bool; not)
 open import Data.Product using (_,_)
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable using (⌊_⌋; dec-yes)
-open import Relation.Binary using () renaming (Decidable to Decidable²)
+open import Relation.Binary using (DecidableEquality) renaming (Decidable to Decidable²)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 record DecEq {ℓ} (A : Type ℓ) : Type ℓ where
-  field _≟_ : Decidable² {A = A} _≡_
+  field _≟_ : DecidableEquality A
 
   _==_ : A → A → Bool
   x == y = ⌊ x ≟ y ⌋

Class/Applicative/Derive.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Level
+
+module Interface.Default where
+
+record Default {a : Level} (A : Set a) : Set a where
+  field
+    default : A