A proof of false in Agda 2.9.0

PositivelyFalse.agda

{-# OPTIONS -vtc.pos:30 #-}
-- Credit to Naïm Favier for the idea that
-- 'if b then Set else (Set → Set)' might trick
-- the positivity checker.
module PositivelyFalse where

--------------------------------------------------------------------------------
-- Prelude

data ⊥ : Set where

-- Unit sans eta
data ⊤ : Set where
  tt : ⊤

⊤-rec : ∀ {ℓ} {A : Set ℓ} → ⊤ → A → A
⊤-rec tt x = x

--------------------------------------------------------------------------------
-- False

Negate : (tt : ⊤) → ⊤-rec tt (Set → Set)
Negate tt X = (X → ⊥)

mutual
  -- This tricks the positivity checker, which doesn't add
  -- an edge from the second argument of P to Negate.
  P : (tt : ⊤) → ⊤-rec tt (Set → Set)
  P = Negate

  -- This in turn breaks positivity checking for FixP
  data FixP : Set where
    wrap : P tt FixP → FixP

no-fixp : FixP → ⊥
no-fixp (wrap x) = x (wrap x)

yet-fixp : FixP
yet-fixp = wrap no-fixp

bang : ⊥
bang = no-fixp yet-fixp