[Agda] Positivity of members of Set

[Owen]

Hello everyone,

It occurs to me that Chung-Kil Hur's proof can be viewed as an
infinite recursion arising from a negative occurrence of Set in a
constructor for Set. This is because the proof uses the excluded
middle only to "pattern match" on an element of Set -- that is, to
find out the type constructor for a type (where injectivity grabs the
type argument). In fact, the proof translates almost verbatim to an
ordinary datatype Set' where I : (Set' → Set') → Set'  is a
constructor, if the positivity check is disabled; then, the excluded
middle is not needed (and, again, injectivity grabs the constructor
argument).

Is there a compelling reason to allow Set to appear negatively within
Set? If a type constructor containing Set in a negative position were
required to be in Set₁, the issue would go away, and type constructors
could still be treated as injective.

Best,
Owen

> Hi everyone,
>
> I proved the absurdity in Agda assuming the excluded middle.
> Is it a well-known fact ?
> It seems that Agda's set theory is weird.
>
> This comes from the injectivity of inductive type constructors.
>
> The proof sketch is as follows.
>
> Define a family of inductive type
>
> data I : (Set -> Set) -> Set where
>
> with no constructors.
>
> By injectivity of type constructors, I can show that I : (Set -> Set) -> Set is injective.
>
> As you may see, there is a size problem with this injectivity.
>
> So, I just used the cantor's diagonalization to derive absurdity in a classical way.
>
> Does anyone know whether cantor's diagonalization essentially needs the classical axiom, or can be done intuitionistically ?
> If the latter is true, then the Agda system is inconsistent.
>
> Please have a look at the Agda code below, and let me know if there's any mistakes.
>
> All comments are wellcome.
>
> Thanks,
> Chung-Kil Hur
>
>
> ============== Agda code ===============
>
> module cantor where
>
>   data Empty : Set where
>
>   data One : Set where
>     one : One
>
>   data coprod (A : Set1) (B : Set1) : Set1 where
>     inl : ∀ (a : A) -> coprod A B
>     inr : ∀ (b : B) -> coprod A B
>
>   postulate exmid : ∀ (A : Set1) -> coprod A (A -> Empty)
>
>   data Eq1 {A : Set1} (x : A) : A -> Set1 where
>     refleq1 : Eq1 x x
>
>   cast : ∀ { A B } -> Eq1 A B -> A -> B
>   cast refleq1 a = a
>
>   Eq1cong : ∀ {f g : Set -> Set} a -> Eq1 f g -> Eq1 (f a) (g a)
>   Eq1cong a refleq1 = refleq1
>
>   Eq1sym : ∀ {A : Set1} { x y : A } -> Eq1 x y -> Eq1 y x
>   Eq1sym refleq1 = refleq1
>
>   Eq1trans : ∀ {A : Set1} { x y z : A } -> Eq1 x y -> Eq1 y z -> Eq1 x z
>   Eq1trans refleq1 refleq1 = refleq1
>
>   data I : (Set -> Set) -> Set where
>
>   Iinj : ∀ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y
>   Iinj refleq1 = refleq1
>
>   data invimageI (a : Set) : Set1 where
>     invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a
>
>   J : Set -> (Set -> Set)
>   J a with exmid (invimageI a)
>   J a | inl (invelmtI x y) = x
>   J a | inr b = λ x → Empty
>
>   data invimageJ (x : Set -> Set) : Set1 where
>     invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x
>
>   IJIeqI : ∀ x -> Eq1 (I (J (I x))) (I x)
>   IJIeqI x with exmid (invimageI (I x))
>   IJIeqI x | inl (invelmtI x' y) = y
>   IJIeqI x | inr b with b (invelmtI x refleq1)
>   IJIeqI x | inr b | ()
>
>   J_srj : ∀ (x : Set -> Set) -> invimageJ x
>   J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))
>
>   cantor : Set -> Set
>   cantor a with exmid (Eq1 (J a a) Empty)
>   cantor a | inl a' = One
>   cantor a | inr b = Empty
>
>   OneNeqEmpty : Eq1 One Empty -> Empty
>   OneNeqEmpty p = cast p one
>
>   cantorone : ∀ a -> Eq1 (J a a) Empty -> Eq1 (cantor a) One
>   cantorone a p with exmid (Eq1 (J a a) Empty)
>   cantorone a p | inl a' = refleq1
>   cantorone a p | inr b with b p
>   cantorone a p | inr b | ()
>
>   cantorempty : ∀ a -> (Eq1 (J a a) Empty -> Empty) -> Eq1 (cantor a) Empty
>   cantorempty a p with exmid (Eq1 (J a a) Empty)
>   cantorempty a p | inl a' with p a'
>   cantorempty a p | inl a' | ()
>   cantorempty a p | inr b = refleq1
>
>   cantorcase : ∀ a -> Eq1 cantor (J a) -> Empty
>   cantorcase a pf with exmid (Eq1 (J a a) Empty)
>   cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a')
>   cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b))
>
>   absurd : Empty
>   absurd with (J_srj cantor)
>   absurd | invelmtJ a y = cantorcase a (Eq1sym y)