[Agda] Re: Question on the Agda tutorial

[Timon Gehr]

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?
>
> TIA
> - d
>

The following two are valid answers:

A ⊎ ⊤
⊤ ⊎ A