Formalization of paradox from Coquand and Paulin '88 in Agda

CoquandPaulin.agda

{-# OPTIONS --without-K #-}

module CoquandPaulin where

-- contradiction from non-strictly-positive type and impredicative sigma
-- possibly also "strong elimination", whatever that is
-- and impredicative identity
-- adapted from https://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/
-- originally from Inductively Defined Types by Thierry Coquand and Christine Paulin

open import Agda.Builtin.Sigma

data ⊥ : Set where

{-# NO_UNIVERSE_CHECK #-}
data _≡_ {X : Set₁} (x : X) : X → Set where
  refl : x ≡ x
ap : {A B : Set₁} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
ap f refl = refl
subst : {A : Set₁} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl Px = Px
sym : {A : Set₁} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

{-# NO_UNIVERSE_CHECK #-}
record ImpredΣ (A : Set₁) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

{-# NO_POSITIVITY_CHECK #-}
data A : Set₁ where
  introA : ((A → Set) → Set) → A

introA-injective : (x y : (A → Set) → Set) → introA x ≡ introA y → x ≡ y
introA-injective x .x refl = refl

i : {X : Set₁} → X → X → Set
i x y = x ≡ y

i-injective : {X : Set₁} (x y : X) → i x ≡ i y → x ≡ y
i-injective {X} x y ix≡iy = sym (subst (λ iz → iz x) ix≡iy refl)

f : (A → Set) → A
f p = introA (i p)

f-injective : (x y : A → Set) → f x ≡ f y → x ≡ y
f-injective x y fx≡fy = i-injective x y (introA-injective (i x) (i y) fx≡fy)

P0 : A → Set
P0 x = ImpredΣ (A → Set) λ P → Σ (f P ≡ x) λ _ → P x → ⊥

x0 : A
x0 = f P0

bad1 : P0 x0 → P0 x0 → ⊥
bad1 (P , (fP≡x0 , Px0)) = subst (λ P → P x0 → ⊥) (f-injective P P0 fP≡x0) Px0

bad2 : (P0 x0 → ⊥) → P0 x0
bad2 ¬P0x0 = P0 , refl , ¬P0x0

worse : ⊥
worse = cannot does
  where
    cannot : P0 x0 → ⊥
    cannot x = bad1 x x

    does : P0 x0
    does = bad2 cannot