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

[Andreas Abel]

On 17.09.12 11:06 AM, Altenkirch Thorsten 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 am concerned what happens on the next level, I.e. can we construct a
> fixpoint of
>
> F : Set₁ → Set₁
> F X = Σ[ E ː Set ] (X ≡ lift E × (E → ⊥))

Yes, we can...  (If we are missing the latest patches...)

data D : Set1 where
   abs : ∀ {E : Set} → D ≡ Lift E → (E → D) → D

down : ∀ {a} {D : Set (lsuc a)} {E : Set a}
        → D ≡ Lift {ℓ = lsuc a} E
        → D → E
down {a} eq d = lower {ℓ = lsuc a} (subst (λ X → X) eq d)

app : D → D → D
app (abs eq f) d = f (down eq d)

But I do not see how to get

   lam : (D → D) → D

> Or alternatively we could use a universe (U : Set, El U -> Set):
>
> F : Set → Set
> F X = Σ[ E ː U ] (X ≡ El E × (E → ⊥))
>
>
> That looks dangerous…

Agreed.

Andreas

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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