[Agda] AIM 10 notes

[Benja Fallenstein]

Hi Conor,

(new to this, please be kind if I say something particularly stupid :-))

> As it is, you may find traditional miseries
> arising, when (^ Nat) -> (^ Nat) turns out to be different from
> ^(Nat -> Nat). But perhaps you've got that covered..?

I've noticed that IIUC, the two are isomorphic:

ltr : ∀ {A} → ↑ (A → A) → ↑ A → ↑ A
ltr f x = ⇑ (f (⇓ x))

rtl : ∀ {A} → (↑ A → ↑ A) → ↑ (A → A)
rtl f = ⇑ (λ x → ⇓ f (⇑ x))

so what would be the traditional miseries? Definitional equality?
Annoyance if the inference algorithm is too naive to insert all the
arrows you want?

[on Coq]
> I believe it allows one to write
>
>  cons (List Nat) nil : List Set

It does; I happened to try that one yesterday after reading some old
post of yours about universe polymorphism :-)

Isn't typical ambiguity sufficient for that, though? It seems like you
only need to infer an index one level higher for the List Set
constructors than for List Nat?

Thanks,
- Benja