[Agda] Negative coinductive sized types

[Nils Anders Danielsson]

On 2020-11-03 21:27, Florian Engel wrote:
> I don't understand why i can't give cons the type
> 
>    cons : {i : Size} {j : Size< i} {A : Set} → A -> Stream j A → Stream i A

The following type works:

   {i : Size} {A : Set} → A → Stream i A → Stream (↑ i) A

-- 
/NAD