{-# OPTIONS --type-in-type #-}

open import Data.Product

data  : Set where

-- f doesn't type check unless we put the equality type in Set
data _≡_ {} {A : Set } (a : A) : A  Set where
  refl : a  a

subst :  { ℓ′} {A : Set } {a b : A}  (P : A  Set ℓ′)  (p : a  b)  P a  P b
subst _ refl pa = pa

¬_ :  {}  Set   Set 
¬ A = A  

 :  {}  Set   Set _
 {} S = S  Set

{-# NO_POSITIVITY_CHECK #-}
record Bad : Set₁ where
  constructor mkBad
  field bad :  ( Bad)

f :  Bad  Bad
f p = mkBad (_≡ p)

fInj :  {p q}  f p  f q  p  q
fInj {p} fp≡fq = subst  p≡  p≡ p) (badInj fp≡fq) refl
  where
  badInj :  {a b}  mkBad a  mkBad b  a  b
  badInj refl = refl

-- type-in-type is for here onwards
P₀ :  Bad
P₀ x = Σ[ P   Bad ] x  f P × ¬ (P x)

x₀ : Bad
x₀ = f P₀

P₀x₀→¬P₀x₀ : P₀ x₀  ¬ P₀ x₀
P₀x₀→¬P₀x₀ (P , x₀≡fP , ¬Px₀) P₀x₀ = ¬Px₀ (subst  P  P x₀) (fInj x₀≡fP) P₀x₀)

¬P₀x₀→P₀x₀ : ¬ P₀ x₀  P₀ x₀
¬P₀x₀→P₀x₀ ¬P₀x₀ = P₀ , refl , ¬P₀x₀

¬P₀x₀ : ¬ P₀ x₀
¬P₀x₀ P₀x₀ = P₀x₀→¬P₀x₀ P₀x₀ P₀x₀

false : 
false = ¬P₀x₀ (¬P₀x₀→P₀x₀ ¬P₀x₀)