[Agda] type of map..<=

Sanjoy Das sanjoy at playingwithpointers.com
Fri Oct 5 11:00:07 CEST 2012

> 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

More information about the Agda mailing list