Use generalized variables in Category subdirectory (#1095)

Author: jespercockx

src/Category/Applicative.agda

@@ -11,27 +11,31 @@
 
 module Category.Applicative where
 
-open import Level using (suc; _⊔_)
+open import Level using (Level; suc; _⊔_)
 open import Data.Unit
 open import Category.Applicative.Indexed
 
-RawApplicative : ∀ {f} → (Set f → Set f) → Set (suc f)
+private
+  variable
+    f : Level
+
+RawApplicative : (Set f → Set f) → Set (suc f)
 RawApplicative F = RawIApplicative {I = ⊤} λ _ _ → F
 
-module RawApplicative {f} {F : Set f → Set f}
+module RawApplicative {F : Set f → Set f}
                       (app : RawApplicative F) where
   open RawIApplicative app public
 
-RawApplicativeZero : ∀ {f} → (Set f → Set f) → Set _
+RawApplicativeZero : (Set f → Set f) → Set _
 RawApplicativeZero F = RawIApplicativeZero {I = ⊤} (λ _ _ → F)
 
-module RawApplicativeZero {f} {F : Set f → Set f}
+module RawApplicativeZero {F : Set f → Set f}
                           (app : RawApplicativeZero F) where
   open RawIApplicativeZero app public
 
-RawAlternative : ∀ {f} → (Set f → Set f) → Set _
+RawAlternative : (Set f → Set f) → Set _
 RawAlternative F = RawIAlternative {I = ⊤} (λ _ _ → F)
 
-module RawAlternative {f} {F : Set f → Set f}
-                          (app : RawAlternative F) where
+module RawAlternative {F : Set f → Set f}
+                      (app : RawAlternative F) where
   open RawIAlternative app public

src/Category/Applicative/Indexed.agda

@@ -17,20 +17,27 @@ open import Function
 open import Level
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
-IFun : ∀ {i} → Set i → (ℓ : Level) → Set (i ⊔ suc ℓ)
+private
+  variable
+    a b c i f : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+IFun : Set i → (ℓ : Level) → Set (i ⊔ suc ℓ)
 IFun I ℓ = I → I → Set ℓ → Set ℓ
 
 ------------------------------------------------------------------------
 -- Type, and usual combinators
 
-record RawIApplicative {i f} {I : Set i} (F : IFun I f) :
+record RawIApplicative {I : Set i} (F : IFun I f) :
                        Set (i ⊔ suc f) where
   infixl 4 _⊛_ _<⊛_ _⊛>_
   infix  4 _⊗_
 
   field
-    pure : ∀ {i A} → A → F i i A
-    _⊛_  : ∀ {i j k A B} → F i j (A → B) → F j k A → F i k B
+    pure : ∀ {i} → A → F i i A
+    _⊛_  : ∀ {i j k} → F i j (A → B) → F j k A → F i k B
 
   rawFunctor : ∀ {i j} → RawFunctor (F i j)
   rawFunctor = record
@@ -42,43 +49,43 @@ record RawIApplicative {i f} {I : Set i} (F : IFun I f) :
            RawFunctor (rawFunctor {i = i} {j = j})
            public
 
-  _<⊛_ : ∀ {i j k A B} → F i j A → F j k B → F i k A
+  _<⊛_ : ∀ {i j k} → F i j A → F j k B → F i k A
   x <⊛ y = const <$> x ⊛ y
 
-  _⊛>_ : ∀ {i j k A B} → F i j A → F j k B → F i k B
+  _⊛>_ : ∀ {i j k} → F i j A → F j k B → F i k B
   x ⊛> y = flip const <$> x ⊛ y
 
-  _⊗_ : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
+  _⊗_ : ∀ {i j k} → F i j A → F j k B → F i k (A × B)
   x ⊗ y = (_,_) <$> x ⊛ y
 
-  zipWith : ∀ {i j k A B C} → (A → B → C) → F i j A → F j k B → F i k C
+  zipWith : ∀ {i j k} → (A → B → C) → F i j A → F j k B → F i k C
   zipWith f x y = f <$> x ⊛ y
 
-  zip : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
+  zip : ∀ {i j k} → F i j A → F j k B → F i k (A × B)
   zip = zipWith _,_
 
 ------------------------------------------------------------------------
 -- Applicative with a zero
 
 record RawIApplicativeZero
-       {i f} {I : Set i} (F : IFun I f) :
+       {I : Set i} (F : IFun I f) :
        Set (i ⊔ suc f) where
   field
     applicative : RawIApplicative F
-    ∅           : ∀ {i j A} → F i j A
+    ∅           : ∀ {i j} → F i j A
 
   open RawIApplicative applicative public
 
 ------------------------------------------------------------------------
 -- Alternative functors: `F i j A` is a monoid
 
 record RawIAlternative
-       {i f} {I : Set i} (F : IFun I f) :
+       {I : Set i} (F : IFun I f) :
        Set (i ⊔ suc f) where
   infixr 3 _∣_
   field
     applicativeZero : RawIApplicativeZero F
-    _∣_             : ∀ {i j A} → F i j A → F i j A → F i j A
+    _∣_             : ∀ {i j} → F i j A → F i j A → F i j A
 
   open RawIApplicativeZero applicativeZero public
 
@@ -87,18 +94,18 @@ record RawIAlternative
 -- Applicative functor morphisms, specialised to propositional
 -- equality.
 
-record Morphism {i f} {I : Set i} {F₁ F₂ : IFun I f}
+record Morphism {I : Set i} {F₁ F₂ : IFun I f}
                 (A₁ : RawIApplicative F₁)
                 (A₂ : RawIApplicative F₂) : Set (i ⊔ suc f) where
   module A₁ = RawIApplicative A₁
   module A₂ = RawIApplicative A₂
   field
-    op      : ∀ {i j X} → F₁ i j X → F₂ i j X
-    op-pure : ∀ {i X} (x : X) → op (A₁.pure {i = i} x) ≡ A₂.pure x
-    op-⊛    : ∀ {i j k X Y} (f : F₁ i j (X → Y)) (x : F₁ j k X) →
+    op      : ∀ {i j} → F₁ i j A → F₂ i j A
+    op-pure : ∀ {i} (x : A) → op (A₁.pure {i = i} x) ≡ A₂.pure x
+    op-⊛    : ∀ {i j k} (f : F₁ i j (A → B)) (x : F₁ j k A) →
               op (f A₁.⊛ x) ≡ (op f A₂.⊛ op x)
 
-  op-<$> : ∀ {i j X Y} (f : X → Y) (x : F₁ i j X) →
+  op-<$> : ∀ {i j} (f : A → B) (x : F₁ i j A) →
            op (f A₁.<$> x) ≡ (f A₂.<$> op x)
   op-<$> f x = begin
     op (A₁._⊛_ (A₁.pure f) x)       ≡⟨ op-⊛ _ _ ⟩

src/Category/Applicative/Predicate.agda

@@ -18,9 +18,13 @@ open import Level
 open import Relation.Unary
 open import Relation.Unary.PredicateTransformer using (Pt)
 
+private
+  variable
+    i ℓ : Level
+
 ------------------------------------------------------------------------
 
-record RawPApplicative {i ℓ} {I : Set i} (F : Pt I ℓ) :
+record RawPApplicative {I : Set i} (F : Pt I ℓ) :
                        Set (i ⊔ suc ℓ) where
   infixl 4 _⊛_ _<⊛_ _⊛>_
   infix  4 _⊗_

src/Category/Comonad.agda

@@ -13,29 +13,36 @@ module Category.Comonad where
 open import Level
 open import Function
 
-record RawComonad {f} (W : Set f → Set f) : Set (suc f) where
+private
+  variable
+    a b c f : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+record RawComonad (W : Set f → Set f) : Set (suc f) where
 
   infixl 1 _=>>_ _=>=_
   infixr 1 _<<=_ _=<=_
 
   field
-    extract : ∀ {A} → W A → A
-    extend  : ∀ {A B} → (W A → B) → (W A → W B)
+    extract : W A → A
+    extend  : (W A → B) → (W A → W B)
 
-  duplicate : ∀ {A} → W A → W (W A)
+  duplicate : W A → W (W A)
   duplicate = extend id
 
-  liftW : ∀ {A B} → (A → B) → W A → W B
+  liftW : (A → B) → W A → W B
   liftW f = extend (f ∘′ extract)
 
-  _=>>_ : ∀ {A B} → W A → (W A → B) → W B
+  _=>>_ : W A → (W A → B) → W B
   _=>>_ = flip extend
 
-  _=>=_ : ∀ {c A B} {C : Set c} → (W A → B) → (W B → C) → W A → C
+  _=>=_ : (W A → B) → (W B → C) → W A → C
   f =>= g = g ∘′ extend f
 
-  _<<=_ : ∀ {A B} → (W A → B) → W A → W B
+  _<<=_ : (W A → B) → W A → W B
   _<<=_ = extend
 
-  _=<=_ : ∀ {A B c} {C : Set c} → (W B → C) → (W A → B) → W A → C
+  _=<=_ : (W B → C) → (W A → B) → W A → C
   _=<=_ = flip _=>=_

src/Category/Functor.agda

@@ -15,27 +15,32 @@ open import Level
 
 open import Relation.Binary.PropositionalEquality
 
-record RawFunctor {ℓ ℓ′} (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
+private
+  variable
+    ℓ ℓ′ ℓ″ : Level
+    A B X Y : Set ℓ
+
+record RawFunctor (F : Set ℓ → Set ℓ′) : Set (suc ℓ ⊔ ℓ′) where
   infixl 4 _<$>_ _<$_
   infixl 1 _<&>_
 
   field
-    _<$>_ : ∀ {A B} → (A → B) → F A → F B
+    _<$>_ : (A → B) → F A → F B
 
-  _<$_ : ∀ {A B} → A → F B → F A
+  _<$_ : A → F B → F A
   x <$ y = const x <$> y
 
-  _<&>_ : ∀ {A B} → F A → (A → B) → F B
+  _<&>_ : F A → (A → B) → F B
   _<&>_ = flip _<$>_
 
 -- A functor morphism from F₁ to F₂ is an operation op such that
 -- op (F₁ f x) ≡ F₂ f (op x)
 
-record Morphism {ℓ ℓ′ ℓ″} {F₁ : Set ℓ → Set ℓ′} {F₂ : Set ℓ → Set ℓ″}
+record Morphism {F₁ : Set ℓ → Set ℓ′} {F₂ : Set ℓ → Set ℓ″}
                 (fun₁ : RawFunctor F₁)
                 (fun₂ : RawFunctor F₂) : Set (suc ℓ ⊔ ℓ′ ⊔ ℓ″) where
   open RawFunctor
   field
-    op     : ∀{X} → F₁ X → F₂ X
-    op-<$> : ∀{X Y} (f : X → Y) (x : F₁ X) →
+    op     : F₁ X → F₂ X
+    op-<$> : (f : X → Y) (x : F₁ X) →
              op (fun₁ ._<$>_ f x) ≡ fun₂ ._<$>_ f (op x)

src/Category/Functor/Predicate.agda

@@ -15,7 +15,11 @@ open import Level
 open import Relation.Unary
 open import Relation.Unary.PredicateTransformer using (PT)
 
-record RawPFunctor {i j ℓ₁ ℓ₂} {I : Set i} {J : Set j}
+private
+  variable
+    i j ℓ₁ ℓ₂ : Level
+
+record RawPFunctor {I : Set i} {J : Set j}
                    (F : PT I J ℓ₁ ℓ₂) : Set (i ⊔ j ⊔ suc ℓ₁ ⊔ suc ℓ₂)
                    where
   infixl 4 _<$>_ _<$_

src/Category/Monad.agda

@@ -13,27 +13,29 @@ module Category.Monad where
 open import Function
 open import Category.Monad.Indexed
 open import Data.Unit
+open import Level
 
-RawMonad : ∀ {f} → (Set f → Set f) → Set _
+private
+  variable
+    f : Level
+
+RawMonad : (Set f → Set f) → Set _
 RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M)
 
-RawMonadT : ∀ {f} (T : (Set f → Set f) → (Set f → Set f)) → Set _
+RawMonadT : (T : (Set f → Set f) → (Set f → Set f)) → Set _
 RawMonadT T = RawIMonadT {I = ⊤} (λ M _ _ → T (M _ _))
 
-RawMonadZero : ∀ {f} → (Set f → Set f) → Set _
+RawMonadZero : (Set f → Set f) → Set _
 RawMonadZero M = RawIMonadZero {I = ⊤} (λ _ _ → M)
 
-RawMonadPlus : ∀ {f} → (Set f → Set f) → Set _
+RawMonadPlus : (Set f → Set f) → Set _
 RawMonadPlus M = RawIMonadPlus {I = ⊤} (λ _ _ → M)
 
-module RawMonad {f} {M : Set f → Set f}
-                (Mon : RawMonad M) where
+module RawMonad {M : Set f → Set f} (Mon : RawMonad M) where
   open RawIMonad Mon public
 
-module RawMonadZero {f} {M : Set f → Set f}
-                    (Mon : RawMonadZero M) where
+module RawMonadZero {M : Set f → Set f}(Mon : RawMonadZero M) where
   open RawIMonadZero Mon public
 
-module RawMonadPlus {f} {M : Set f → Set f}
-                    (Mon : RawMonadPlus M) where
+module RawMonadPlus {M : Set f → Set f} (Mon : RawMonadPlus M) where
   open RawIMonadPlus Mon public

src/Category/Monad/Continuation.agda

@@ -16,30 +16,34 @@ open import Category.Monad.Indexed
 open import Function
 open import Level
 
+private
+  variable
+    i f : Level
+    I : Set i
+
 ------------------------------------------------------------------------
 -- Delimited continuation monads
 
-DContT : ∀ {i f} {I : Set i} → (I → Set f) → (Set f → Set f) → IFun I f
+DContT : (I → Set f) → (Set f → Set f) → IFun I f
 DContT K M r₂ r₁ a = (a → M (K r₁)) → M (K r₂)
 
-DCont : ∀ {i f} {I : Set i} → (I → Set f) → IFun I f
+DCont : (I → Set f) → IFun I f
 DCont K = DContT K Identity
 
-DContTIMonad : ∀ {i f} {I : Set i} (K : I → Set f) {M} →
-               RawMonad M → RawIMonad (DContT K M)
+DContTIMonad : ∀ (K : I → Set f) {M} → RawMonad M → RawIMonad (DContT K M)
 DContTIMonad K Mon = record
   { return = λ a k → k a
   ; _>>=_  = λ c f k → c (flip f k)
   }
   where open RawMonad Mon
 
-DContIMonad : ∀ {i f} {I : Set i} (K : I → Set f) → RawIMonad (DCont K)
+DContIMonad : (K : I → Set f) → RawIMonad (DCont K)
 DContIMonad K = DContTIMonad K Id.monad
 
 ------------------------------------------------------------------------
 -- Delimited continuation operations
 
-record RawIMonadDCont {i f} {I : Set i} (K : I → Set f)
+record RawIMonadDCont {I : Set i} (K : I → Set f)
                       (M : IFun I f) : Set (i ⊔ suc f) where
   field
     monad : RawIMonad M
@@ -49,7 +53,7 @@ record RawIMonadDCont {i f} {I : Set i} (K : I → Set f)
 
   open RawIMonad monad public
 
-DContTIMonadDCont : ∀ {i f} {I : Set i} (K : I → Set f) {M} →
+DContTIMonadDCont : ∀ (K : I → Set f) {M} →
                     RawMonad M → RawIMonadDCont K (DContT K M)
 DContTIMonadDCont K Mon = record
   { monad = DContTIMonad K Mon
@@ -59,6 +63,5 @@ DContTIMonadDCont K Mon = record
   where
   open RawIMonad Mon
 
-DContIMonadDCont : ∀ {i f} {I : Set i}
-                   (K : I → Set f) → RawIMonadDCont K (DCont K)
+DContIMonadDCont : (K : I → Set f) → RawIMonadDCont K (DCont K)
 DContIMonadDCont K = DContTIMonadDCont K Id.monad