[Agda] Positivity of members of Set

[Andreas Abel]

Owen,

at least semantically, there is no reason why "I" as in

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

should be injective.  I F and I G are both the empty type, for arbitrary 
F and G.

Also, we want to be able to abstract arbitrary objects in types, even (F 
: Set -> Set).  For instance,

   module M (F : K) where

     data I : Set where

should succeed, regardless the type K of F.

Cheers,
Andreas

On 25.08.2014 19:35, Owen wrote:
> 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)
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/