title: Why is this not a valid definition of dependent function types in agda?
body: <p>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:</p>
  
  <pre><code>data Pi (A : Set) (B : A -&gt; Set) : Set where
    \ (a : A) -&gt; (b : B a) : Pi A B
  </code></pre>
  
  <p>When I try to load this it gives me a parse error. I'm not sure why, perhaps it doesn't want <code>\</code> 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.</p>