[Agda] Forget Hurken's Paradox,
Agda has a quicker route to success
Dan Doel
dan.doel at gmail.com
Sun Sep 16 22:09:57 CEST 2012
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
More information about the Agda
mailing list