[Made the code universe-polymorphic.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101119151346
 Ignore-this: 6d8e331aedb90136aa4799a21b4f946d
] hunk ./ReverseComposition.agda 5
+{-# OPTIONS --universe-polymorphism #-}
+
hunk ./ReverseComposition.agda 9
+open import Category.Monad
hunk ./ReverseComposition.agda 12
+open import Data.Maybe as Maybe
hunk ./ReverseComposition.agda 14
-open import Data.Product
+open import Data.Product using (∃; ,_; proj₁; proj₂)
hunk ./ReverseComposition.agda 17
+open import Level
hunk ./ReverseComposition.agda 26
-data _⇨_ : List Set → Set → Set₁ where
+data _⇨_ {ℓ} : List (Set ℓ) → Set ℓ → Set (suc ℓ) where
hunk ./ReverseComposition.agda 34
-_·_ : ∀ {A As B} → (A ∷ As) ⇨ B → A → As ⇨ B
+_·_ : ∀ {ℓ} {A B : Set ℓ} {As} → (A ∷ As) ⇨ B → A → As ⇨ B
hunk ./ReverseComposition.agda 39
-! : ∀ {B} → [] ⇨ B → B
+! : ∀ {ℓ} {B : Set ℓ} → [] ⇨ B → B
hunk ./ReverseComposition.agda 47
-_↑_ : Set → ℕ → Set₁
+_↑_ : ∀ {ℓ} → Set ℓ → ℕ → Set (suc ℓ)
hunk ./ReverseComposition.agda 52
-app : ∀ {A n} → A ↑ n → Vec A n → A
+app : ∀ {ℓ} {A : Set ℓ} {n} → A ↑ n → Vec A n → A
hunk ./ReverseComposition.agda 61
-data _≈_ : ∀ {As₁ As₂ B₁ B₂} → As₁ ⇨ B₁ → As₂ ⇨ B₂ → Set₁ where
+data _≈_ {ℓ} : ∀ {As₁ As₂} {B₁ B₂ : Set ℓ} →
+               As₁ ⇨ B₁ → As₂ ⇨ B₂ → Set (suc ℓ) where
hunk ./ReverseComposition.agda 68
-refl : ∀ {As B} (f : As ⇨ B) → f ≈ f
+refl : ∀  {ℓ As} {B : Set ℓ} (f : As ⇨ B) → f ≈ f
hunk ./ReverseComposition.agda 72
-sym : ∀ {As₁ As₂ B₁ B₂} {f : As₁ ⇨ B₁} {g : As₂ ⇨ B₂} →
+sym : ∀ {ℓ As₁ As₂} {B₁ B₂ : Set ℓ} {f : As₁ ⇨ B₁} {g : As₂ ⇨ B₂} →
hunk ./ReverseComposition.agda 77
-trans : ∀ {As₁ As₂ As₃ B₁ B₂ B₃}
+trans : ∀ {ℓ As₁ As₂ As₃} {B₁ B₂ B₃ : Set ℓ}
hunk ./ReverseComposition.agda 90
-  _≈⟨_⟩_ : ∀ {As₁ B₁ As₂ B₂ As₃ B₃}
-             (f : As₁ ⇨ B₁) {g : As₂ ⇨ B₂} {h : As₃ ⇨ B₃} →
+  _≈⟨_⟩_ : ∀ {ℓ As₁ As₂ As₃} {B₁ B₂ B₃ : Set ℓ}
+           (f : As₁ ⇨ B₁) {g : As₂ ⇨ B₂} {h : As₃ ⇨ B₃} →
hunk ./ReverseComposition.agda 95
-  _≡⟨_⟩_ : ∀ {As₁ B₁ As₂ B₂} f {g : As₁ ⇨ B₁} {h : As₂ ⇨ B₂} →
+  _≡⟨_⟩_ : ∀ {ℓ As₁ As₂} {B₁ B₂ : Set ℓ}
+           f {g : As₁ ⇨ B₁} {h : As₂ ⇨ B₂} →
hunk ./ReverseComposition.agda 100
-  _∎ : ∀ {As B} (f : As ⇨ B) → f ≈ f
+  _∎ : ∀ {ℓ As} {B : Set ℓ} (f : As ⇨ B) → f ≈ f
hunk ./ReverseComposition.agda 112
-  EqualTo : ∀ {As B} → As ⇨ B → Set₁
-  EqualTo {As} {B} f = ∃ λ (g : As ⇨ B) → f ≈ g
+  EqualTo : ∀ {ℓ As} {B : Set ℓ} → As ⇨ B → Set (suc ℓ)
+  EqualTo {As = As} {B} f = ∃ λ (g : As ⇨ B) → f ≈ g
hunk ./ReverseComposition.agda 115
-  ▷_ : ∀ {As B} {f g : As ⇨ B} → f ≈ g → EqualTo f
+  ▷_ : ∀ {ℓ As} {B : Set ℓ} {f g : As ⇨ B} → f ≈ g → EqualTo f
hunk ./ReverseComposition.agda 118
-  witness : ∀ {As B} {f : As ⇨ B} → EqualTo f → As ⇨ B
+  witness : ∀ {ℓ As} {B : Set ℓ} {f : As ⇨ B} → EqualTo f → As ⇨ B
hunk ./ReverseComposition.agda 121
-  proof : ∀ {As B} {f : As ⇨ B} (f≈ : EqualTo f) → f ≈ witness f≈
+  proof : ∀ {ℓ As} {B : Set ℓ} {f : As ⇨ B}
+          (f≈ : EqualTo f) → f ≈ witness f≈
hunk ./ReverseComposition.agda 127
-η : ∀ {A As B} {f : (A ∷ As) ⇨ B} → Λ (λ x → f · x) ≡ f
+η : ∀ {ℓ As} {A B : Set ℓ} {f : (A ∷ As) ⇨ B} → Λ (λ x → f · x) ≡ f
hunk ./ReverseComposition.agda 132
-_·-cong_ : ∀ {A₁ As₁ B₁ x₁} {f₁ : A₁ ∷ As₁ ⇨ B₁}
-             {A₂ As₂ B₂ x₂} {f₂ : A₂ ∷ As₂ ⇨ B₂} →
+_·-cong_ : ∀ {ℓ As₁ As₂} {A₁ B₁ A₂ B₂ : Set ℓ}
+             {x₁ x₂} {f₁ : A₁ ∷ As₁ ⇨ B₁} {f₂ : A₂ ∷ As₂ ⇨ B₂} →
hunk ./ReverseComposition.agda 137
-!-cong : ∀ {B₁} {x₁ : [] ⇨ B₁}
-           {B₂} {x₂ : [] ⇨ B₂} →
+!-cong : ∀ {ℓ} {B₁ B₂ : Set ℓ} {x₁ : [] ⇨ B₁} {x₂ : [] ⇨ B₂} →
hunk ./ReverseComposition.agda 146
-_>>=_ : ∀ {As B Bs C} → As ⇨ B → (B → Bs ⇨ C) → As ++ Bs ⇨ C
+_>>=_ : ∀ {ℓ As Bs} {B C : Set ℓ} →
+        As ⇨ B → (B → Bs ⇨ C) → As ++ Bs ⇨ C
hunk ./ReverseComposition.agda 153
-module MonadLaws where
+module MonadLaws {ℓ} where
hunk ./ReverseComposition.agda 155
-  left-identity : ∀ {A As B} (f : A → As ⇨ B) x →
+  left-identity : ∀ {As} {A B : Set ℓ} (f : A → As ⇨ B) x →
hunk ./ReverseComposition.agda 159
-  right-identity : ∀ {As B} (f : As ⇨ B) → f >>= return ≈ f
+  right-identity : ∀ {As} {B : Set ℓ}
+                   (f : As ⇨ B) → f >>= return ≈ f
hunk ./ReverseComposition.agda 164
-  assoc : ∀ {As B Bs C Cs D}
+  assoc : ∀ {As Bs Cs} {B C D : Set ℓ}
hunk ./ReverseComposition.agda 172
-  _>>=-cong_ : ∀ {As₁ B₁ Bs₁ C₁} {f₁ : As₁ ⇨ B₁} {g₁ : B₁ → Bs₁ ⇨ C₁}
-                 {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ → Bs₂ ⇨ C₂} →
+  _>>=-cong_ : ∀ {As₁ Bs₁ As₂ Bs₂} {B₁ C₁ B₂ C₂ : Set ℓ}
+                 {f₁ : As₁ ⇨ B₁} {g₁ : B₁ → Bs₁ ⇨ C₁}
+                 {f₂ : As₂ ⇨ B₂} {g₂ : B₂ → Bs₂ ⇨ C₂} →
hunk ./ReverseComposition.agda 184
-_⊙_ : ∀ {As B Bs C} → As ⇨ B → (B ∷ Bs) ⇨ C → As ++ Bs ⇨ C
+_⊙_ : ∀ {ℓ As Bs} {B C : Set ℓ} →
+      As ⇨ B → (B ∷ Bs) ⇨ C → As ++ Bs ⇨ C
hunk ./ReverseComposition.agda 188
-identity : ∀ {A} → A ∷ [] ⇨ A
+identity : ∀ {ℓ} {A : Set ℓ} → A ∷ [] ⇨ A
hunk ./ReverseComposition.agda 191
-module MonoidLaws where
+module MonoidLaws {ℓ} where
hunk ./ReverseComposition.agda 196
-  right-identity : ∀ {As B} (f : As ⇨ B) → f ⊙ identity ≈ f
+  right-identity : ∀ {As} {B : Set ℓ}
+                   (f : As ⇨ B) → f ⊙ identity ≈ f
hunk ./ReverseComposition.agda 205
-  left-identity : ∀ {A As B} (f : A ∷ As ⇨ B) → identity ⊙ f ≈ f
+  left-identity : ∀ {As} {A B : Set ℓ}
+                  (f : A ∷ As ⇨ B) → identity ⊙ f ≈ f
hunk ./ReverseComposition.agda 216
-  assoc : ∀ {As B Bs C Cs D}
+  assoc : ∀ {As Bs Cs} {B C D : Set ℓ}
hunk ./ReverseComposition.agda 229
-  _⊙-cong_ : ∀ {As₁ B₁ Bs₁ C₁} {f₁ : As₁ ⇨ B₁} {g₁ : B₁ ∷ Bs₁ ⇨ C₁}
-               {As₂ B₂ Bs₂ C₂} {f₂ : As₂ ⇨ B₂} {g₂ : B₂ ∷ Bs₂ ⇨ C₂} →
+  _⊙-cong_ : ∀ {As₁ Bs₁ As₂ Bs₂} {B₁ C₁ B₂ C₂ : Set ℓ}
+               {f₁ : As₁ ⇨ B₁} {g₁ : B₁ ∷ Bs₁ ⇨ C₁}
+               {f₂ : As₂ ⇨ B₂} {g₂ : B₂ ∷ Bs₂ ⇨ C₂} →
hunk ./ReverseComposition.agda 235
-  identity-cong : ∀ {A} → identity {A} ≈ identity {A}
+  identity-cong : {A : Set ℓ} → identity {A = A} ≈ identity {A = A}