Formalization of the fact that a dependent type theory with excluded middle cannot have a universe Set such that Set → Set injects into Set.

UniverseInjection.agda

-- Counterexample by Chung Kil Hur, improved by Andrej Bauer

-- We show that it is inconsistent to have an injection I : (Set → Set) → Set and excluded middle.
-- Indeed, excluded middle and I together give a surjection J : Set → (Set → Set),
-- which by Lawvere's fixed point theorem begets a fixed point operator on Set.
-- However, negation does not have a fixed point.

module cantor where

-- generalities

data Empty : Set where

data coprod (A : Set1) (B : Set1) : Set1 where
  inl : ∀ (a : A) → coprod A B
  inr : ∀ (b : B) → coprod A B

-- Identity type on the universe

data Id {A : Set1} (x : A) : A → Set1 where
  refl : Id x x

cast : ∀ { A B } → Id A B → A → B
cast refl a = a

Idcong : ∀ {A B} {x y : A} (f : A → B) → Id x y → Id (f x) (f y)
Idcong f refl = refl

Idsym : ∀ {A : Set1} { x y : A } → Id x y → Id y x
Idsym refl = refl

data I : (Set → Set) → Set where

-- we postulate injectivity of I (in old Agda it was possible to prove it)
postulate Iinj : ∀ { x y : Set → Set } → Id (I x) (I y) → Id x y
-- Iinj refl = refl -- the old Agda proof, does not work anymore

data invimageI (a : Set) : Set1 where
  invelmtI : forall x → (Id (I x) a) → invimageI a

-- using excluded middle, we construct a left inverse J of I

-- excluded middle (only used in J and JIid)
postulate lem : ∀ (A : Set1) → coprod A (A → Empty)

J : Set → (Set → Set)
J a with lem (invimageI a)
J a | inl (invelmtI x y) = x
J a | inr _ = λ _ → Empty

JIid : ∀ x → Id (J (I x)) x
JIid x = Iinj (IJIeqI x)
  where IJIeqI : ∀ x → Id (I (J (I x))) (I x)
        IJIeqI x with lem (invimageI (I x))
        IJIeqI x | inl (invelmtI _ y) = y
        IJIeqI x | inr b with b (invelmtI x refl)
        IJIeqI x | inr b | ()

-- Because J has a right inverse, it is surjective and Lawvere's fixed point
-- theorem applies to give a fixed-point operator on Set

fix : ∀ (f : Set → Set) → Set
fix f = J (I q) (I q) where q = λ x → f (J x x)

fixes : ∀ (f : Set → Set) → Id (fix f) (f (fix f))
fixes f = Idcong (λ h → h (I q)) (JIid q) where q = λ x → f (J x x)

-- To get into trouble, we just need an endomap on Set without a fixed point

-- negation will do
not : Set → Set
not a = a → Empty

notnofix : ∀ (a : Set) → Id a (not a) → Empty
notnofix a p = (λ x → cast p x x) (cast (Idsym p) (λ x → cast p x x))

absurd : Empty
absurd = notnofix (fix not) (fixes not)