<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    Dear Philippe,<br>
    <br>
    These Agda exercise sessions - mostly by Jesper Cockx - may be of
    interest to you:<br>
    <a class="moz-txt-link-freetext" href="https://github.com/anuyts/agda-sessions">https://github.com/anuyts/agda-sessions</a><br>
    <br>
    To answer your question:<br>
    <span style="font-variant-ligatures: no-common-ligatures" class="">tauto₁</span><span
      style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span
      style="font-variant-ligatures: no-common-ligatures; color:
      #535353" class="">=</span><span style="font-variant-ligatures:
      no-common-ligatures;" class=""> </span>\ A B C g f a -> g a (f
    a)<br>
    <br>
    Best regards,<br>
    Andreas<br>
    <br>
    <div class="moz-cite-prefix">On 18/04/2020 17:32, Philippe de
      Rochambeau wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:5D08F574-4173-482C-B79D-95A4BDA7A89D@free.fr">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      s/« which the user can then apply » /«  letting the use apply
      them »/<br class="">
      <div><br class="">
        <blockquote type="cite" class="">
          <div class="">Le 18 avr. 2020 à 17:30, Philippe de Rochambeau
            <<a href="mailto:phiroc@free.fr" class=""
              moz-do-not-send="true">phiroc@free.fr</a>> a écrit :</div>
          <br class="Apple-interchange-newline">
          <div class="">
            <div style="word-wrap: break-word; -webkit-nbsp-mode: space;
              line-break: after-white-space;" class="">
              <div class=""><br class="">
              </div>
              <div class="">Hello,</div>
              <div class=""><br class="">
              </div>
              <div class="">I am attempting to translate a Coq proof
                into Agda, for learning purposes (cf. <a
                  href="https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf"
                  class="" moz-do-not-send="true">https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf</a>,
                p. 9):</div>
              <div class=""><br class="">
              </div>
              <div class="">
                <div style="margin: 0px; font-stretch: normal;
                  line-height: normal; font-family: Menlo;" class=""><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #4500ff" class="">tauto₁</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">:</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">∀</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">(</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class="">A B C </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">:</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #4500ff" class="">Set</span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">)</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">(</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class="">A </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> B </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> C</span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">)</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">(</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class="">A </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> B</span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">)</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> A </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">→</span><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class=""> C</span></div>
                <div style="margin: 0px; font-stretch: normal;
                  line-height: normal; font-family: Menlo; color:
                  rgb(69, 0, 255);" class=""><span
                    style="font-variant-ligatures: no-common-ligatures"
                    class="">tauto₁</span><span
                    style="font-variant-ligatures: no-common-ligatures;"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #535353" class="">=</span><span
                    style="font-variant-ligatures: no-common-ligatures;"
                    class=""> </span><span
                    style="font-variant-ligatures: no-common-ligatures;
                    color: #343434; background-color: #a2ff9f" class="">{
                    }</span><span style="font-variant-ligatures:
                    no-common-ligatures; background-color: rgb(162, 255,
                    159);" class="">0</span></div>
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal; font-family: Menlo; color: rgb(69,
                0, 255);" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">Here’s how Coq introduces
                hypotheses, letting the use apply them.</div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal; font-family: Menlo; color: rgb(69,
                0, 255);" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  236.23px; top: 794.986px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.849653);"
                  class="">Coq < apply H’.</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  236.23px; top: 814.911px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">1 </span><span style="left: 236.23px; top:
                  814.911px; font-size: 16.6043px; font-family:
                  monospace; transform: scaleX(0.999592);" class="">subgoal</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 854.761px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">A : Prop</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 874.687px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">B : Prop</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 894.612px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">C : Prop</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 914.537px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">H : A -> B -> C</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 934.462px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">H’ : A -> B</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 954.387px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">HA : A</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  256.157px; top: 974.312px; font-size: 16.6043px;
                  font-family: monospace; transform: scaleX(0.999592);"
                  class="">============================</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><span style="left:
                  266.118px; top: 994.239px; font-size: 16.6043px;
                  font-family: monospace;" class="">A</span></div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">How do you do the same
                thing in Agda?</div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">Cheers,</div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class=""><br class="">
              </div>
              <div style="margin: 0px; font-stretch: normal;
                line-height: normal;" class="">Philippe</div>
            </div>
            _______________________________________________<br class="">
            Agda mailing list<br class="">
            <a href="mailto:Agda@lists.chalmers.se" class=""
              moz-do-not-send="true">Agda@lists.chalmers.se</a><br
              class="">
            <a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
          </div>
        </blockquote>
      </div>
      <br class="">
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>