Does #Agda's function arrow have a type? basically this right
_->_ : forall {l l' : Level} -> Set l -> Set l' -> Set (l ⊔ l')
Conversation
Trouble is that you need to account for substituting the parameter unto the return type. This signature only describes non-dependent functions.
1
4
Is there a way to account for that in a type?
1
1
Replying to
Yeah, not sure sadly. The best I've ever been able to do is:
Prod : (A : Type) (B : A -> Type) -> Type;
Prod A B = (a : A) -> B a;
😕