Tidy up: s/Set/Type + flags + levels

Class/Applicative.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Applicative where
 
 open import Class.Applicative.Core public

Class/Applicative/Core.agda

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

Class/Applicative/Instances.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Applicative.Instances where
 
 open import Class.Prelude

Class/Bifunctor.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Bifunctor where
 
 open import Class.Prelude hiding (A; B; C)

Class/CommutativeMonoid.agda

@@ -1,5 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
-
+{-# OPTIONS --cubical-compatible #-}
 module Class.CommutativeMonoid where
 
 open import Class.CommutativeMonoid.Core public

Class/CommutativeMonoid/Core.agda

@@ -1,12 +1,12 @@
-{-# OPTIONS --safe --without-K #-}
-
+{-# OPTIONS --cubical-compatible #-}
 module Class.CommutativeMonoid.Core where
 
-import Algebra as Alg
 open import Class.Prelude
 open import Class.Semigroup
 open import Class.Monoid
 
+import Algebra as Alg
+
 record CommutativeMonoid c ℓ Carrier : Type (lsuc (c ⊔ ℓ)) where
   infix  4 _≈_
   field
@@ -19,7 +19,8 @@ module Conversion {c ℓ} where
   toBundle : ∀ {Carrier} → CommutativeMonoid c ℓ Carrier → Alg.CommutativeMonoid c ℓ
   toBundle c = record { CommutativeMonoid c }
 
-  fromBundle : (m : Alg.CommutativeMonoid c ℓ) → CommutativeMonoid c ℓ (Alg.CommutativeMonoid.Carrier m)
+  fromBundle : (m : Alg.CommutativeMonoid c ℓ)
+             → CommutativeMonoid c ℓ (Alg.CommutativeMonoid.Carrier m)
   fromBundle c = record
     { Alg.CommutativeMonoid c using (_≈_; isCommutativeMonoid)
     ; semigroup = λ where ._◇_ → Alg.CommutativeMonoid._∙_ c

Class/CommutativeMonoid/Instances.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 
 module Class.CommutativeMonoid.Instances where
 

Class/Core.agda

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

Class/Default.agda

@@ -2,7 +2,7 @@
 -- Types with a default value.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Default where
 
 open import Class.Prelude

Class/Foldable.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Foldable where
 
 open import Class.Foldable.Core public

Class/Foldable/Core.agda

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

Class/Foldable/Instances.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Foldable.Instances where
 
 open import Class.Prelude

Class/Functor.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Functor where
 
 open import Class.Functor.Core public

Class/Functor/Core.agda

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

Class/Functor/Instances.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Functor.Instances where
 
 open import Class.Prelude

Class/HasAdd.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --cubical-compatible #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.HasAdd where
 
 open import Class.HasAdd.Core public

Class/HasAdd/Core.agda

@@ -1,8 +1,10 @@
-{-# OPTIONS --safe --cubical-compatible #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.HasAdd.Core where
 
-record HasAdd (A : Set) : Set where
+open import Class.Prelude
+
+record HasAdd (A : Type ℓ) : Type ℓ where
   infixl 6 _+_
   field _+_ : A → A → A
 
-open HasAdd ⦃ ... ⦄ public
+open HasAdd ⦃...⦄ public

Class/HasAdd/Instance.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --cubical-compatible #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.HasAdd.Instance where
 
 open import Class.HasAdd.Core

Class/HasOrder.agda

@@ -1,5 +1,3 @@
-{-# OPTIONS --safe #-}
-
 module Class.HasOrder where
 
 open import Class.HasOrder.Core public

Class/HasOrder/Core.agda

@@ -1,30 +1,28 @@
-{-# OPTIONS --safe #-}
-
+{-# OPTIONS --without-K #-}
 module Class.HasOrder.Core where
 
+open import Class.Prelude
 open import Class.Decidable
-open import Data.Empty
-open import Data.Product
-open import Data.Sum
-open import Function
-open import Level
-open import Relation.Binary
-open import Relation.Binary using () renaming (Decidable to Decidable²)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
+open import Function.Bundles using (module Equivalence; mk⇔; _⇔_)
+open import Relation.Binary using
+  ( IsPreorder; IsPartialOrder; IsEquivalence; Total; IsTotalOrder
+  ; IsStrictTotalOrder; IsStrictPartialOrder
+  ; Irreflexive; Antisymmetric; Asymmetric; Transitive
+  )
 
 open Equivalence
 
-module _ {a} {A : Set a} where
-  module _ {_≈_ : Rel A a} where
+module _ {A : Type ℓ} where
+  module _ {_≈_ : Rel A ℓ′} {ℓ″ ℓ‴} (let 𝐿 = lsuc ℓ ⊔ ℓ′ ⊔ lsuc ℓ″ ⊔ lsuc ℓ‴) where
 
-    record HasPreorder : Set (suc a) where
+    record HasPreorder : Type 𝐿 where
       infix 4 _≤_ _<_ _≥_ _>_
       field
-        _≤_ _<_       : Rel A a
+        _≤_           : Rel A ℓ″
+        _<_           : Rel A ℓ‴
         ≤-isPreorder  : IsPreorder _≈_ _≤_
         <-irrefl      : Irreflexive _≈_ _<_
-        ≤⇔<∨≈         : ∀ {x y} → x ≤ y ⇔ (x < y ⊎ x ≈ y)
+        ≤⇔<∨≈         : ∀ {x y : A} → x ≤ y ⇔ (x < y ⊎ x ≈ y)
 
       _≥_ = flip _≤_
       _>_ = flip _<_
@@ -33,10 +31,10 @@ module _ {a} {A : Set a} where
         using ()
         renaming (isEquivalence to ≈-isEquivalence; refl to ≤-refl; trans to ≤-trans)
 
-      _≤?_ : ⦃ _≤_ ⁇² ⦄ → Decidable _≤_
+      _≤?_ : ⦃ _≤_ ⁇² ⦄ → Decidable² _≤_
       _≤?_ = dec²
 
-      _<?_ : ⦃ _<_ ⁇² ⦄ → Decidable _<_
+      _<?_ : ⦃ _<_ ⁇² ⦄ → Decidable² _<_
       _<?_ = dec²
 
       infix 4 _<?_ _≤?_
@@ -55,12 +53,12 @@ module _ {a} {A : Set a} where
 
     open HasPreorder ⦃...⦄
 
-    record HasDecPreorder : Set (suc a) where
+    record HasDecPreorder : Type 𝐿 where
       field ⦃ hasPreorder ⦄ : HasPreorder
             ⦃ dec-≤ ⦄ : _≤_ ⁇²
             ⦃ dec-< ⦄ : _<_ ⁇²
 
-    record HasPartialOrder : Set (suc a) where
+    record HasPartialOrder : Type 𝐿 where
       field
         ⦃ hasPreorder ⦄ : HasPreorder
         ≤-antisym : Antisymmetric _≈_ _≤_
@@ -90,13 +88,13 @@ module _ {a} {A : Set a} where
 
     open HasPartialOrder ⦃...⦄
 
-    record HasDecPartialOrder : Set (suc a) where
+    record HasDecPartialOrder : Type 𝐿 where
       field
         ⦃ hasPartialOrder ⦄ : HasPartialOrder
         ⦃ dec-≤ ⦄ : _≤_ ⁇²
         ⦃ dec-< ⦄ : _<_ ⁇²
 
-    record HasTotalOrder : Set (suc a) where
+    record HasTotalOrder : Type 𝐿 where
       field
         ⦃ hasPartialOrder ⦄ : HasPartialOrder
         ≤-total : Total _≤_
@@ -106,15 +104,15 @@ module _ {a} {A : Set a} where
 
       open IsEquivalence ≈-isEquivalence renaming (sym to ≈-sym)
 
-      ≮⇒≥ : Decidable _≈_ → ∀ {x y} → ¬ (x < y) → y ≤ x
+      ≮⇒≥ : Decidable² _≈_ → ∀ {x y} → ¬ (x < y) → y ≤ x
       ≮⇒≥ _≈?_ {x} {y} x≮y with x ≈? y | ≤-total y x
       ... | yes x≈y  | _        = IsPreorder.reflexive ≤-isPreorder (≈-sym x≈y)
       ... | _        | inj₁ y≤x = y≤x
       ... | no  x≉y  | inj₂ x≤y = contradiction (≤∧≉⇒< (x≤y , x≉y)) x≮y
 
     open HasTotalOrder ⦃...⦄
 
-    record HasDecTotalOrder : Set (suc a) where
+    record HasDecTotalOrder : Type 𝐿 where
       field
         ⦃ hasTotalOrder ⦄ : HasTotalOrder
         ⦃ dec-≤ ⦄ : _≤_ ⁇²
@@ -133,9 +131,9 @@ open HasDecPartialOrder ⦃...⦄ public hiding (hasPartialOrder)
 open HasTotalOrder ⦃...⦄ public hiding (hasPartialOrder)
 open HasDecTotalOrder ⦃...⦄ public hiding (hasTotalOrder)
 
-module _ {a} {A : Set a} {_≈_ : Rel A a} where
+module _ {A : Type ℓ} {_≈_ : Rel A ℓ′} where
 
-  module _ {_≤_ : Rel A a} where
+  module _ {_≤_ : Rel A ℓ″} where
     import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as SNS
 
     module _ (≤-isPreorder : IsPreorder _≈_ _≤_)
@@ -158,7 +156,7 @@ module _ {a} {A : Set a} {_≈_ : Rel A a} where
         ; ≤-antisym = antsym
         }
 
-  module _ {_<_ : Rel A a} where
+  module _ {_<_ : Rel A ℓ″} where
 
     import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as SNS
 
@@ -181,7 +179,6 @@ module _ {a} {A : Set a} {_≈_ : Rel A a} where
           ; ≤-antisym = SNS.isPartialOrder <-isStrictPartialOrder .IsPartialOrder.antisym
           }
 
-
     module _ (<-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_) where
 
       private spo = IsStrictTotalOrder.isStrictPartialOrder <-isStrictTotalOrder

Class/HasOrder/Instance.agda

@@ -1,5 +1,4 @@
-{-# OPTIONS --safe #-}
-
+{-# OPTIONS --without-K #-}
 module Class.HasOrder.Instance where
 
 open import Class.DecEq

Class/Monad.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Monad where
 
 open import Class.Monad.Core public

Class/Monad/Core.agda

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

Class/Monad/Instances.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Monad.Instances where
 
 open import Class.Prelude

Class/Monoid.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Monoid where
 
 open import Class.Monoid.Core public

Class/Monoid/Core.agda

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

Class/Monoid/Instances.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Monoid.Instances where
 
 open import Class.Prelude

Class/Prelude.agda

@@ -1,12 +1,12 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Prelude where
 
 open import Agda.Primitive public
   using () renaming (Set to Type; Setω to Typeω)
 open import Level public
   using (Level; _⊔_) renaming (suc to lsuc)
-open import Function public
-  using (id; _∘_; _∋_; _$_; const; constᵣ; flip; it)
+open import Function.Base public
+  using (id; _∘_; _∋_; _$_; const; constᵣ; flip; it; case_of_)
 
 open import Data.Empty public
   using (⊥; ⊥-elim)
@@ -44,7 +44,7 @@ open import Data.These public
   using (These; this; that; these)
 
 open import Relation.Nullary public
-  using (¬_; Dec; yes; no)
+  using (¬_; Dec; yes; no; contradiction)
 open import Relation.Nullary.Decidable public
   using (⌊_⌋; dec-yes; isYes)
 open import Relation.Unary public
@@ -54,7 +54,7 @@ open import Relation.Binary public
   using (REL; Rel; DecidableEquality)
   renaming (Decidable to Decidable²)
 module _ {a b c} where
-  3REL : (A : Set a) (B : Set b) (C : Set c) (ℓ : Level) → Type _
+  3REL : (A : Type a) (B : Type b) (C : Type c) (ℓ : Level) → Type _
   3REL A B C ℓ = A → B → C → Type ℓ
 
   Decidable³ : ∀ {A B C ℓ} → 3REL A B C ℓ → Type _
@@ -66,7 +66,7 @@ open import Reflection public
   using (TC; Arg; Abs)
 
 variable
-  ℓ ℓ′ ℓ″ : Level
+  ℓ ℓ′ ℓ″ ℓ‴ : Level
   A B C : Type ℓ
 
 module Alg (_~_ : Rel A ℓ) where

Class/Semigroup.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Semigroup where
 
 open import Class.Semigroup.Core public

Class/Semigroup/Core.agda

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

Class/Semigroup/Instances.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --cubical-compatible #-}
 module Class.Semigroup.Instances where
 
 open import Class.Prelude