[Agda] Forget Hurken's Paradox, Agda has a quicker route to success

[Dan Doel]

On Thu, Sep 6, 2012 at 12:47 PM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2012-09-06 17:21, Andreas Abel wrote:
>>
>> The problem is that Agda considers
>>
>>    F D = \Sigma E : Set. (D ≡ E) * (E → ⊥)
>>
>> as strictly positive in D.
>
>
> I'm trying to understand if this is actually a problem. Are there any
> dire consequences if we stick to predicative types?

The above F is demonstrably both contravariant and not covariant:

    F : Set → Set₁
    F X = Σ[ E ∶ Set ] (X ≡ E × (E → ⊥))

    thd : ∀{X} → F X → X → ⊥
    thd (E , X≡E , ¬E) = subst (λ Z → Z → ⊥) (sym X≡E) ¬E

    contra : ∀{X Y} → (X → Y) → F Y → F X
    contra {X} {Y} f FY = X , refl , thd FY ∘ f

    ¬co : Σ[ X ∶ Set ] Σ[ Y ∶ Set ] ¬ ((X → Y) → (F X → F Y))
    ¬co = ⊥ , ⊤ , (λ map → thd (map ⊥-elim (⊥ , refl , ⊥-elim)) _)

So Agda's checker should not be considering it covariant, let alone
strictly positive, even if nothing predicative can take advantage of
this example.

-- Dan