Idris2 is anticlassical

[gallais]

I expect this is known but just for the sake of it, I thought I'd port Chung Kil Hur's classic proof.

module InjectiveTypeConstructors

0 ExcludedMiddle : Type
ExcludedMiddle = (0 a : Type) -> Either a (Not a)

data InverseImage : (a -> b) -> b -> Type where
  MkII : (x : a) -> f x === y -> InverseImage f y

parameters (exmid : ExcludedMiddle)

  data I : (Type -> Type) -> Type where

  injectiveI : forall a, b. I a === I b -> a === b
  injectiveI Refl = Refl

  J : Type -> (Type -> Type)
  J a with (exmid (InverseImage I a))
    J a | Left (MkII x y) = x
    J a | Right b = const Void

  IJIeqI : (x : Type -> Type) -> I (J (I x)) === I x
  IJIeqI x with (exmid (InverseImage I (I x)))
    _ | Left (MkII y eq) = eq
    _ | Right notp = void $ notp (MkII x Refl)

  surjectiveJ : (x : Type -> Type) -> InverseImage J x
  surjectiveJ x = MkII (I x) (injectiveI $ IJIeqI x)

  Cantor : Type -> Type
  Cantor a with (exmid (J a a === Void))
    Cantor a | Left a' = ()
    Cantor a | Right b = Void


  cantorUnit : J a a === Void -> Cantor a === ()
  cantorUnit eq with (exmid (J a a === Void))
    _ | Left p = Refl
    _ | Right p = void (p eq)

  cantorVoid : Not (J a a === Void) -> Cantor a === Void
  cantorVoid neq with (exmid (J a a === Void))
    _ | Left p = void (neq p)
    _ | Right p = Refl

  cantorNotJ : Not (Cantor === J a)
  cantorNotJ pf with (exmid (J a a === Void))
    _ | Left p =
      let eq : Void === ()
          := trans (sym p) (trans (cong ($ a) (sym pf)) (cantorUnit p)) in
      rewrite eq in ()
    _ | Right p = p $ trans (cong ($ a) (sym pf)) (cantorVoid p)


anticlassical : Not ExcludedMiddle
anticlassical exmid with (surjectiveJ exmid (Cantor exmid))
  _ | MkII a eq = cantorNotJ exmid (sym eq)

[ohad]

It's only anticlassical if you put LEM in the proof-relevant fragment. It might not be anticlassical if you put it in a propositional fragment, no?