[Agda] Why does Agda think this is not strictly positive?

[Roman]

Hi, Fredrik.

> This implies that Coerce β A is equivalent to (A -> Coerce β A)

I don't think this is the case: `Coerce β A` is isomorphic to `A`.

> open import Data.Empty

> oops : D -> ⊥
> oops (C (coerce x)) = oops x

That's just because `D` is uninhabited. Here is the same:

    data D′ : Set where
      C′ : D′ -> D′

    oops′ : D′ -> ⊥
    oops′ (C′ d) = oops′ d