<div dir="ltr"><div dir="ltr"><div>Have a look at cubical. <br></div><div><table class="gmail-highlight gmail-tab-size gmail-js-file-line-container"><tbody><tr><td id="gmail-LC78" class="gmail-blob-code gmail-blob-code-inner gmail-js-file-line">
<br></td>
      </tr>
      <tr>
        </tr></tbody></table><table class="gmail-highlight gmail-tab-size gmail-js-file-line-container"><tbody><tr><td id="gmail-LC79" class="gmail-blob-code gmail-blob-code-inner gmail-js-file-line gmail-highlighted">  <span class="gmail-pl-en">funExt</span> <span class="gmail-pl-k">:</span> {f g : (x : A) <span class="gmail-pl-k">→</span> B x} <span class="gmail-pl-k">→</span> ((x : A) <span class="gmail-pl-k">→</span> f x ≡ g x) <span class="gmail-pl-k">→</span> f ≡ g</td>
      </tr>
      <tr>
        </tr></tbody></table>  funExt p <span class="gmail-pl-k">=</span> <span class="gmail-pl-k">λ</span> i x <span class="gmail-pl-k">→</span> p x i</div><div><table class="gmail-highlight gmail-tab-size gmail-js-file-line-container" width="6" height="1"><tbody><tr><td id="gmail-LC78" class="gmail-blob-code gmail-blob-code-inner gmail-js-file-line"><br></td>
      </tr>
      <tr>
        </tr></tbody></table><br></div><div><a href="https://github.com/agda/cubical/blob/43bba3614117b6b107787c137f5776af2e128710/Cubical/Core/Prelude.agda#L79">https://github.com/agda/cubical/blob/43bba3614117b6b107787c137f5776af2e128710/Cubical/Core/Prelude.agda#L79</a><br></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Nov 14, 2018 at 9:14 PM Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com">nicolai.kraus@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div>On Wed, Nov 14, 2018 at 6:50 PM 千里冰封 <<a href="mailto:ice1000kotlin@foxmail.com" target="_blank">ice1000kotlin@foxmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><span style="color:rgb(51,51,51);font-family:幼圆">test : {A B : Type i} (a : A) (P Q : (A -> B)) -> P a == Q a -> P == Q</span></div></blockquote><div><br></div><div>P and Q are functions A -> B, but you only know that they are equal for one single input a:A. The functions could differ for other inputs, so you should not expect that they are equal.</div><div>Maybe you want to look up "function extensionality" (which looks similar but says something very different).</div></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>