[Agda] Parameterized type families

[Álvaro García Pérez]

Hello,

I'm trying to define a Set parameterized on a function that takes a Set. ¿Do
anybody know the differences between declaring one argument before the colon
or after the colon in a data definition?

{- This one defines a Set1 instead of a Set-}
data Func : {A : Set} -> (f : A -> A) -> Set where
  c : {A : Set} -> (g : A -> A) -> Func g

{- This one works -}
data Func {A : Set} : (f : A -> A) -> Set where
  c : (g : A -> A) -> Func g

{- This one raises "g x != f x of type A when checking the constructor" -}
data Func {A : Set} (f : A -> A) : Set where
  c : (g : A -> A) -> Func g

How does agda manipulate internally those parameters? Why the third version
does not work? Would be any differences if declaring the parameter A
explicitly? Is there any other way to index a data type on a function?

Many thanks,

Alvaro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081022/8cf00bab/attachment.html