CODEWITHSUNDEEP
lambdatypesagda
Eben Cowley
Eben Cowley

Reputation: 175

Why is this not a valid definition of dependent function types in agda?

I was watching a lecture where the lecturer said that it was impossible, or at least very difficult to define Pi types in Agda. But I'm convinced there has to be a way. Given a type in a universe and a family from the type to the universe, any function from the type to some type in the family will be of the Pi type. So I thought it would make sense to use a lambda:

data Pi (A : Set) (B : A -> Set) : Set where
  \ (a : A) -> (b : B a) : Pi A B

When I try to load this it gives me a parse error. I'm not sure why, perhaps it doesn't want \ to be a type constructor, but it kind of makes sense to consider a lambda to be a type constructor of a function type. Note that I am using the latex feature for Agda in Emacs but I don't think I can write latex in stack overflow. That being said, I tried replacing the lowercase lambda with an uppercase one to see if it wanted a unique type constructor, but to no avail.

Upvotes: 1

Views: 345

Answers (1)

asr
asr

Reputation: 1186

You can use the uppercase lambda after fixing the typo in : Pi A B, that is

data Pi (A : Set) (B : A -> Set) : Set where
  Λ : ((a : A) -> B a) -> Pi A B

Upvotes: 3

Related Questions