[Agda] Question on the Agda tutorial

[Andrés Sicard-Ramírez]

On 10 July 2013 16:03, david rush <kumoyuki at gmail.com> 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:

Which tutorial are you reading?

>
>     Give an isomorphic definition of Maybe A with the help of _⊎_ and ⊤
>
> 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?

-- A version without universe levels.

Maybe' : (A : Set) → Set
Maybe' A = A ⊎ ⊤

-- 
Andrés