[Agda] Agda with the excluded middle is inconsistent ?

[Andrew Pitts]

I have been following this thread with interest. What is needed most
is a simple yet expressive (and fixed!) core type theory with an
easily understandable (by users) semantics: we should not have to
"discover" the _logical_ consequences of  an implementation---it's a
bit like saying the meaning of my programming language is given by my
compiler.

The rest of this message is speculation without reference to such a
semantics. :-)

Personally, my bet is that the version of Agda2 that allows one to
prove that type constructors are injective up to intensional equality
is inconsistent, without  the need for any form of excluded middle
postulate.

I say this not because I think that the injectivity up to intensional
equality of type constructors is in itself contradictory---indeed I
believe it is quite a natural property to ask for....so long as the
universe in which the type constructor is valued is sufficiently
large. For example, in the presence of injectivity, allowing Set to
contain a (Set -> Set)-indexed family of mutually distinct names for
the empty set

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

seems dangerous because Set is "too small"; whereas allowing it in Set1

  data I1 : (Set -> Set) -> Set1 where

seems uncontentious. So I would advocate applying the same
predicativity/size considerations to (injective) type constructors as
Agda currently applies to data constructors. Another example: Agda2
allows

  data J (f : Set -> Set) : Set where
    unit : J f

almost by accident, since it doesn't allow

  data K : (f : Set -> Set) -> Set where
    unit :  (f : Set -> Set) -> K f

because of predicativity restrictions on data constructors. I would
prefer to rule out both declarations while still allowing injective
type constructors like

  data J1 (f : Set -> Set) : Set1 where
    unit : J1 f

or

  data K1 : (f : Set -> Set) -> Set1 where
    unit :  (f : Set -> Set) -> K1 f

Best wishes,

Andy