CODEWITHSUNDEEP
agda
seldon
seldon

Reputation: 1027

Why is Agda refusing Set₁ → Set₁?

Here's the code:

Continuation : Set → Set₁ → Set₁
Continuation R X = (X → R) → R

Selection : Set → Set₁ → Set₁
Selection R X = (X → R) → X

dagger : {R : Set} → Selection R → Continuation R
dagger S X k = k (S k)

I need continuation and selection to use a higher universe for other reasons. But then the definition of dagger raises an error:

(Set₁ → Set₁) should be a sort, but it isn't when checking that the inferred type of an application Set₁ → Set₁ matches the expected type _16

Upvotes: 1

Views: 230

Answers (1)

gallais
gallais

Reputation: 12113

In Agda _→_ is the function space not of any category but that of types and functions. My guess is that you want the following:

dagger : {R : Set} → ∀ X → Selection R X → Continuation R X
dagger X S k = k (S k)

i.e. the function space of indexed types and index-preserving functions.

Alternatively you could make this clear by using the stdlib's Relation.Unary notion of morphism and write:

open import Relation.Unary

dagger : {R : Set} → Selection R ⊆ Continuation R
dagger S k = k (S k)

Upvotes: 4

Related Questions