title: What is the combinatory logic equivalent of intuitionistic type theory?
body: <p>I recently completed a university course which featured Haskell and Agda (a dependent typed functional programming language), and was wondering if it was possible to replace lambda calculus in these with combinatory logic. With Haskell this seems possible using the S and K combinators, thus making it point-free. I was wondering what the equivalent was for Agda. I.e., can one make a dependently typed functional programming language equivalent to Agda without using any variables?</p>
  
  <p>Also, is it possible to somehow replace quantification with combinators? I don't know if this is a coincidence but universal quantification for example makes a type signature look like a lambda expression. Is there a way to remove universal quantification from a type signature without changing its meaning? E.g. in:</p>
  
  <pre><code>forall a : Int -&gt; a &lt; 0 -&gt; a + a &lt; a
  </code></pre>
  
  <p>Can the same thing be expressed without using a forall?</p>