[ agda/agda#5000 ] Move SizedType etc into module Size

Author: andreasabel

.travis.yml

@@ -56,7 +56,7 @@ matrix:
              cd ../ &&
              git clone https://github.com/agda/agda &&
              cd agda &&
-             git checkout 0f4538c8dcd175b92acd577ca0bdca232f5cd17f &&
+             git checkout a8077a59977d55d85743790924adf24dc0c9de2d &&
              cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
           fi
 

src/Codata/Thunk.agda

@@ -9,26 +9,11 @@
 module Codata.Thunk where
 
 open import Level
-open import Size
-
-private
-  variable
-    ℓ ℓ₁ ℓ₂ : Level
+open import Size; open SizedType
 
 ------------------------------------------------------------------------
 -- Basic types.
 
-SizedType : (ℓ : Level) → Set (suc ℓ)
-SizedType ℓ = Size → Set ℓ
-
-∀ˢ[_] : SizedType ℓ → Set ℓ
-∀ˢ[ F ] = ∀{i} → F i
-
-infixr 8 _⇒ˢ_
-
-_⇒ˢ_ : SizedType ℓ₁ → SizedType ℓ₂ → SizedType (ℓ₁ ⊔ ℓ₂)
-F ⇒ˢ G = λ i → F i → G i
-
 record Thunk {ℓ} (F : Size → Set ℓ) (i : Size) : Set ℓ where
   coinductive
   field force : {j : Size< i} → F j
@@ -57,26 +42,26 @@ syntax Thunk-syntax (λ j → e) i = Thunk[ j < i ] e
 -- Thunk is a functor
 module _ {p q} {P : Size → Set p} {Q : Size → Set q} where
 
-  map : ∀ˢ[ P ⇒ˢ Q ] → ∀ˢ[ Thunk P ⇒ˢ Thunk Q ]
+  map : ∀[ P ⇒ Q ] → ∀[ Thunk P ⇒ Thunk Q ]
   map f p .force = f (p .force)
 
 -- Thunk is a comonad
 module _ {p} {P : Size → Set p} where
 
-  extract : ∀ˢ[ Thunk P ] → P ∞
+  extract : ∀[ Thunk P ] → P ∞
   extract p = p .force
 
-  duplicate : ∀ˢ[ Thunk P ⇒ˢ Thunk (Thunk P) ]
+  duplicate : ∀[ Thunk P ⇒ Thunk (Thunk P) ]
   duplicate p .force .force = p .force
 
 module _ {p q} {P : Size → Set p} {Q : Size → Set q} where
 
   infixl 1 _<*>_
-  _<*>_ : ∀ˢ[ Thunk (P ⇒ˢ Q) ⇒ˢ Thunk P ⇒ˢ Thunk Q ]
+  _<*>_ : ∀[ Thunk (P ⇒ Q) ⇒ Thunk P ⇒ Thunk Q ]
   (f <*> p) .force = f .force (p .force)
 
 -- We can take cofixpoints of functions only making Thunk'd recursive calls
 module _ {p} (P : Size → Set p) where
 
-  cofix : ∀ˢ[ Thunk P ⇒ˢ P ] → ∀ˢ[ P ]
+  cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ]
   cofix f = f λ where .force → cofix f

src/Size.agda

@@ -16,3 +16,26 @@ open import Agda.Builtin.Size public
         ; _⊔ˢ_                --  _⊔ˢ_   : Size → Size → Size
         ; ∞                   --  ∞      : Size
         )
+
+open import Level
+
+private
+  variable
+    ℓ ℓ₁ ℓ₂ : Level
+
+-- Concept of sized type
+
+SizedType : (ℓ : Level) → Set (suc ℓ)
+SizedType ℓ = Size → Set ℓ
+
+-- Type constructors involving SizedType
+
+module SizedType where
+
+  infixr 8 _⇒_
+
+  _⇒_ : SizedType ℓ₁ → SizedType ℓ₂ → SizedType (ℓ₁ ⊔ ℓ₂)
+  F ⇒ G = λ i → F i → G i
+
+  ∀[_] : SizedType ℓ → Set ℓ
+  ∀[ F ] = ∀{i} → F i