[Agda] How to write a type alias for _->_?

[James Wood]

Hi David,

The `A` introduced on the left hand side of the `=` is an inhabitant of 
the `A` introduced implicitly (which the type checker now calls `A₁`, 
because it was shadowed by the former `A`). The story for the `B`s is 
similar. Remember that `X → Y` is a shorthand for `(_ : X) → Y`, i.e, we 
get to talk about inhabitants of `X`. This contrasts with `∀ X → Y`, 
which is a shorthand for `(X : _) → Y`.

Ignoring potential for universe polymorphism, _⇒_ should have the much 
simpler type `Set → Set → Set`. That is, it takes two types, say, `A` 
and `B`, and produces a new type `A → B`.

Regards,
James

On 20/01/2021 23:19, David Banas wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> Hi all,
> 
> I’m trying to define a type alias for function arrow: _->_, and can’t 
> make it work.
> Here’s my code:
> 
>     _⇒_ : ∀ {A B : Set} → A → B → Set₁
>     _⇒_ A B = {!A → B!}
> 
> 
> And, when I type `C-c C-<SPACE>` in the hole, the “A” gets highlighted 
> in red and I’m told:
> 
>     A₁ should be a sort, but it isn't
>     when checking that the expression A has type _3
> 
> 
> which I don’t really understand.
> 
> Can anyone shed some light?
> 
> Thanks,
> -db
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>