[Agda] type of map..<=

[Sanjoy Das]

> Generally, when setting a type signature, may it happen that more than
> one type is possible? If there are multiple possibilities, does there

Such a thing is syntactically possible:

data X : Set where
  t : X

data Y : Set where
  t : Y

m : -- can be either X or Y
m = t

but I don't think this answers your question.

Whether a value may have more than one type at a more fundamental
level I do not know.

-- 
Sanjoy Das
http://playingwithpointers.com