 an explicit version in LaTTe, as follows:</p>
<pre><code class="language-clojure">(lambda [A :type]
  (lambda [B :type]
      (lambda [x A]
           (lambda [y B]
        (lambda [C :type]
           (lambda [z (==&gt; A B
                           C)]
                    ((z x) y)))))))
</code></pre>
<p>(wow! that’s verbose…)</p>
<p>The type of this function is more interesting:</p>
<pre><code class="language-clojure">(forall [A :type]
  (forall [B :type]
    (==&gt; A B
        (forall [C :type]
 