On 2012-10-12 20:51, Dmytro Starosud wrote: > Could you tell me please whether there is anything to support unique types in Agda? Do you mean uniqueness types? -- /NAD