Merge pull request #1326 from agda/agda5000

Changes related to SizeUniv [agda/agda#5000]

Author: andreasabel

.travis.yml

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

src/Codata/Thunk.agda

@@ -8,8 +8,7 @@
 
 module Codata.Thunk where
 
-open import Size
-open import Relation.Unary
+open import Size; open SizedType
 
 ------------------------------------------------------------------------
 -- Basic types.

src/Size.agda

@@ -9,9 +9,33 @@
 module Size where
 
 open import Agda.Builtin.Size public
-  renaming ( SizeU to SizeUniv ) --  sort SizeUniv
-  using    ( Size                --  Size   : SizeUniv
-           ; Size<_              --  Size<_ : Size → SizeUniv
-           ; ↑_                  --  ↑_     : Size → Size
-           ; _⊔ˢ_                --  _⊔ˢ_   : Size → Size → Size
-           ; ∞ )                 --  ∞      : Size
+  using ( SizeUniv            --  sort SizeUniv
+        ; Size                --  Size   : SizeUniv
+        ; Size<_              --  Size<_ : Size → SizeUniv
+        ; ↑_                  --  ↑_     : Size → Size
+        ; _⊔ˢ_                --  _⊔ˢ_   : 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