[Agda] Quotient types in Agda, if you Trust Me

[Andrew Pitts]

On 14 May 2015 at 11:56, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>>...is there a small example to illustrate the limitation of quotients
>>types?
>
> The simplest example is to consider infinitely branching trees
> ....

Thanks -- that's a very instructive example.

Andy