Moved _⇒_ and ∀[_] from Size to Relation.Unary.Sized

Author: andreasabel

CHANGELOG.md

@@ -70,8 +70,15 @@ New modules
 * Added `Reflection.Annotated.Free` implementing free variable annotations for
   reflected terms.
 
+* Added `Relation.Unary.Sized` for unary relations over sized types now that `Size` lives in it's own universe since Agda 2.6.2.
+
 Other major changes
 -------------------
 
 Other minor additions
 ---------------------
+
+* Added new type in `Size`:
+  ```agda
+  SizedSet ℓ = Size → Set ℓ
+  ```

src/Codata/Thunk.agda

@@ -8,29 +8,30 @@
 
 module Codata.Thunk where
 
-open import Size; open SizedType
+open import Size
+open import Relation.Unary.Sized
 
 ------------------------------------------------------------------------
 -- Basic types.
 
-record Thunk {ℓ} (F : Size → Set ℓ) (i : Size) : Set ℓ where
+record Thunk {ℓ} (F : SizedSet ℓ) (i : Size) : Set ℓ where
   coinductive
   field force : {j : Size< i} → F j
 open Thunk public
 
-Thunk^P : ∀ {f p} {F : Size → Set f} (P : Size → F ∞ → Set p)
+Thunk^P : ∀ {f p} {F : SizedSet f} (P : Size → F ∞ → Set p)
           (i : Size) (tf : Thunk F ∞) → Set p
 Thunk^P P i tf = Thunk (λ i → P i (tf .force)) i
 
-Thunk^R : ∀ {f g r} {F : Size → Set f} {G : Size → Set g}
+Thunk^R : ∀ {f g r} {F : SizedSet f} {G : SizedSet g}
           (R : Size → F ∞ → G ∞ → Set r)
           (i : Size) (tf : Thunk F ∞) (tg : Thunk G ∞) → Set r
 Thunk^R R i tf tg = Thunk (λ i → R i (tf .force) (tg .force)) i
 
 ------------------------------------------------------------------------
 -- Syntax
 
-Thunk-syntax : ∀ {ℓ} → (Size → Set ℓ) → Size → Set ℓ
+Thunk-syntax : ∀ {ℓ} → SizedSet ℓ → Size → Set ℓ
 Thunk-syntax = Thunk
 
 syntax Thunk-syntax (λ j → e) i = Thunk[ j < i ] e
@@ -39,28 +40,28 @@ syntax Thunk-syntax (λ j → e) i = Thunk[ j < i ] e
 -- Basic functions.
 
 -- Thunk is a functor
-module _ {p q} {P : Size → Set p} {Q : Size → Set q} where
+module _ {p q} {P : SizedSet p} {Q : SizedSet q} where
 
   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
+module _ {p} {P : SizedSet p} where
 
   extract : ∀[ Thunk P ] → P ∞
   extract p = p .force
 
   duplicate : ∀[ Thunk P ⇒ Thunk (Thunk P) ]
   duplicate p .force .force = p .force
 
-module _ {p q} {P : Size → Set p} {Q : Size → Set q} where
+module _ {p q} {P : SizedSet p} {Q : SizedSet q} where
 
   infixl 1 _<*>_
   _<*>_ : ∀[ 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
+module _ {p} (P : SizedSet p) where
 
   cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ]
   cofix f = f λ where .force → cofix f

src/Relation/Unary/Sized.agda

@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed unary relations over sized types
+------------------------------------------------------------------------
+
+-- Sized types live in the special sort `SizeUniv` and therefore are no
+-- longer compatible with the ordinary combinators defined in
+-- `Relation.Unary`.
+
+{-# OPTIONS --without-K --safe --sized-types #-}
+
+module Relation.Unary.Sized  where
+
+open import Level
+open import Size
+
+private
+  variable
+    ℓ ℓ₁ ℓ₂ : Level
+
+infixr 8 _⇒_
+_⇒_ : SizedSet ℓ₁ → SizedSet ℓ₂ → SizedSet (ℓ₁ ⊔ ℓ₂)
+F ⇒ G = λ i → F i → G i
+
+∀[_] : SizedSet ℓ → Set ℓ
+∀[ F ] = ∀{i} → F i

src/Size.agda

@@ -8,34 +8,22 @@
 
 module Size where
 
-open import Agda.Builtin.Size public
-  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
+------------------------------------------------------------------------
+-- Re-export builtins
 
-  infixr 8 _⇒_
+open import Agda.Builtin.Size public using
+  ( SizeUniv  --  sort SizeUniv
+  ; Size      --  : SizeUniv
+  ; Size<_    --  : Size → SizeUniv
+  ; ↑_        --  : Size → Size
+  ; _⊔ˢ_      --  : Size → Size → Size
+  ; ∞         --  : Size
+  )
 
-  _⇒_ : SizedType ℓ₁ → SizedType ℓ₂ → SizedType (ℓ₁ ⊔ ℓ₂)
-  F ⇒ G = λ i → F i → G i
+------------------------------------------------------------------------
+-- Concept of sized type
 
-  ∀[_] : SizedType ℓ → Set ℓ
-  ∀[ F ] = ∀{i} → F i
+SizedSet : (ℓ : Level) → Set (suc ℓ)
+SizedSet ℓ = Size → Set ℓ