[Agda] Re: Question on the Agda tutorial

Timon Gehr timon.gehr at gmx.ch
Wed Jul 10 23:35:37 CEST 2013

On 07/10/2013 11:03 PM, david rush wrote:
> Hi y'all -
> I've started working through the Agda tutorial  in order to try and eliminate
> gaps in what I think I understand while hacking up a framework for numerical
> computation, and I ran across this question:
>      Give an isomorphic definition of Maybe A with the help of _⊎_ and ⊤

http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Parametric.html ?

> And for the life of me I can't figure it out. Either the question is wrong or
> I've seriously missed something, because it seems to me that it would be easy
> to formulate a type isomorphic to Maybe A with the help of _⊎_ and ⊥.
> Can someone tell me what I am missing, if anything?
> - d

The following two are valid answers:

A ⊎ ⊤
⊤ ⊎ A

More information about the Agda mailing list