<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>Hi Philippe, <br>
      <br>
      Indeed you cannot compare two values of arbitrary types for
      equality.<br>
      <br>
      James' idea was to write a function that given two comparison
      functions for the first and second projection <br>
      of a pair, produces a comparison function for the pair as a whole.
      <br>
      <br>
      The signature you wrote for _eq_ is correct<br>
      and you should be able to implement, although its implementation
      should take 4 parameters: `eq eqa eqb ab ab' = ?`<br>
      Try putting a and a' in the hole on the RHS and pressing C-c C-C
      to expand the cases. Now you can use eqa and eqb to compare<br>
      the components of the pairs.<br>
      <br>
      On the use site, you know the type A at which you're comparing and
      you can give a non-generic implementation of the two input
      comparison functions,<br>
      for example for Nat.<br>
      <br>
      Once you have an idea of how the implementation works in a
      functional language, you can look at typeclasses in Agda to get a
      definition that is a little<br>
      easier to work with and does not require you to manually give the
      comparison functions as parameters.<br>
      <br>
      Hope this helps,<br>
      <br>
      <br>
      Arjen<br>
    </p>
    <div class="moz-cite-prefix">On 5/4/20 8:00 AM, Philippe de
      Rochambeau wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:EF4ACBD8-74C8-4029-B13E-0C5E26C74F5E@free.fr">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      Good morning James,
      <div class=""><br class="">
      </div>
      <div class="">I spent a few hours yesterday attempting to write
        the <i class="">fst</i> description procedure, as suggested,
        but to no avail.</div>
      <div class="">For me, <i class="">fst_desc_proc</i> should
        compare two values of type <i class="">A</i> and, if they are
        equal, return <i class="">true</i>, otherwise, <i class="">false</i>.</div>
      <div class="">But how how do you generically compare two A
        values? ≡ won’t do.</div>
      <div class=""><br class="">
      </div>
      <div class="">(In fact, I wouldn’t know either how to compare two
        <i class="">Nats</i> for equality in Agda, since I could not
        find an <i class="">==</i> operator in <i class="">Data.Nats</i>).</div>
      <div class=""><br class="">
      </div>
      <div class="">Cheers,</div>
      <div class=""><br class="">
      </div>
      <div class="">Philippe</div>
      <div class="">
        <div class=""><br class="">
        </div>
        <div class="">
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(237, 97, 27);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">open</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">import</span><span style="font-variant-ligatures:
              no-common-ligatures; color: #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #c200ff" class="">Data.Nat</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">using</span><span style="font-variant-ligatures:
              no-common-ligatures; color: #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">(</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #4500ff" class="">ℕ</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">)</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(194, 0, 255);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures; color: #ed611b" class="">open</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #ed611b" class="">import</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">Relation.Binary.PropositionalEquality</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #ed611b" class="">using</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">(</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #4500ff" class="">_≡_</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">)</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(237, 97, 27);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">open</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">import</span><span style="font-variant-ligatures:
              no-common-ligatures; color: #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #c200ff" class="">Data.Bool</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; min-height: 21px;" class=""><br
              class="">
            <span style="font-variant-ligatures: no-common-ligatures"
              class=""></span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(237, 97, 27);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">record</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #4500ff" class="">Pair</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">(</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class="">A B </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">:</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" 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; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">:</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #4500ff" class="">Set</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">where</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(237, 97, 27);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures; color: #000000" class="">  </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">field</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo;" class=""><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">    </span><span style="font-variant-ligatures:
              no-common-ligatures; color: #fb198d" class="">fst</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></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo;" class=""><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">    </span><span style="font-variant-ligatures:
              no-common-ligatures; color: #fb198d" class="">snd</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=""> B</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; min-height: 21px;" class=""><span
              style="font-variant-ligatures: no-common-ligatures"
              class=""></span><br class="">
          </div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(237, 97, 27);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">open</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #c200ff" class="">Pair</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">public</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; min-height: 21px;" class=""><span
              style="font-variant-ligatures: no-common-ligatures"
              class=""></span><br class="">
          </div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">{--                         
                                                                       
                                                                       
                                     </span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">_eq_ : {A B : Set} → (a :
              Pair A B) → (b : Pair A B) → Bool                         
                                                                       
                                       </span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">a eq b = (fst a ≡ fst b) ∧
              (snd a ≡ snd b)                                          
                                                                       
                                       </span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">--}</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; min-height: 21px;" class=""><span
              style="font-variant-ligatures: no-common-ligatures"
              class=""></span><br class="">
          </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="">fst_desc_proc</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">:</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">{</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class="">A </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">:</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">Set</span><span style="font-variant-ligatures:
              no-common-ligatures; color: #535353" class="">}</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">→</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">(</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class="">a a' </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">:</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> A</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">)</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">→</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures"
              class="">Bool</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="">fst_desc_proc</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> a a' </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">=</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span style="text-decoration:
              underline ; font-variant-ligatures: no-common-ligatures;
              color: #b42419" class="">a</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span style="text-decoration:
              underline ; font-variant-ligatures: no-common-ligatures;
              color: #b42419" class="">≡</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span style="text-decoration:
              underline ; font-variant-ligatures: no-common-ligatures;
              color: #b42419" class="">a'</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="">fst_desc_proc</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">=</span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #000000" class=""> </span><span
              style="font-variant-ligatures: no-common-ligatures; color:
              #535353" class="">{!!}</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; min-height: 21px;" class=""><span
              style="font-variant-ligatures: no-common-ligatures"
              class=""></span><br class="">
          </div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">{--                         
                                                                       
                                                                       
                                     </span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">snd_desc_proc : {B : Set} →
              (b b' : B) → Bool                                         
                                                                       
                                     </span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">snd_desc_proc b b' = b == b'
              → true                                                   
                                                                       
                                     </span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">snd_desc_proc b b' = b != b'
              → false                                                  
                                                                       
                                     </span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">--}</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">-- _eq_ : {A B : Set} → ((a
              a′ : A) → Bool) → ((b b′ : B) → Bool) → (ab ab′ : Pair A
              B) → Bool</span></div>
          <div style="margin: 0px; font-stretch: normal; line-height:
            normal; font-family: Menlo; color: rgb(203, 36, 24);"
            class=""><span style="font-variant-ligatures:
              no-common-ligatures" class="">-- a eq a' = ?</span></div>
          <div class=""><span style="font-variant-ligatures:
              no-common-ligatures" class=""><br class="">
            </span></div>
          <div class=""><br class="">
          </div>
          <div class=""><br class="">
            <div><br class="">
              <blockquote type="cite" class="">
                <div class="">Le 3 mai 2020 à 19:56, James Wood <<a
                    href="mailto:james.wood.100@strath.ac.uk" class=""
                    moz-do-not-send="true">james.wood.100@strath.ac.uk</a>>
                  a écrit :</div>
                <br class="Apple-interchange-newline">
                <div class="">
                  <div class="">Hi Philippe,<br class="">
                    <br class="">
                    You can see from the source code of
                    `Agda.Builtin.Bool` that it defines<br class="">
                    only `Bool`, `true`, and `false`. If you want some
                    operations on<br class="">
                    Booleans, you can either define them yourself or get
                    them from a<br class="">
                    library, e.g, stdlib's `Data.Bool`. It's best
                    practice to not import<br class="">
                    `Agda.Builtin` modules unless you really have to
                    (e.g, if you are<br class="">
                    writing your own base library). They may change
                    between versions.<br class="">
                    <br class="">
                    For making your `eq` generic, the simplest thing to
                    do would be to take<br class="">
                    as arguments decision procedures for the `fst`s and
                    `snd`s,<br class="">
                    respectively. The type should be `{A B : Set} → ((a
                    a′ : A) → Bool) →<br class="">
                    ((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool`.<br
                      class="">
                    <br class="">
                    Additionally, you might want to add `open Pair
                    public` after your<br class="">
                    definition of `Pair`, so that you don't have to
                    qualify `fst` and `snd`.<br class="">
                    There's an example of this in stdlib's definition of
                    `Σ` (somewhere<br class="">
                    around `Data.Product`).<br class="">
                    <br class="">
                    Regards,<br class="">
                    James<br class="">
                    <br class="">
                    On 03/05/2020 17:50, Philippe de Rochambeau wrote:<br
                      class="">
                    <blockquote type="cite" class="">Hello,<br class="">
                      <br class="">
                      when I load the following script, I get a « not in
                      scope ∧ » error.<br class="">
                      Why is that?<br class="">
                      Furthermore, how can I make the /eq/ function
                      generic, whichever the<br class="">
                      types used in the Pair, as long as the first type
                      is equal to the second?<br class="">
                      Many thanks.<br class="">
                      Philippe<br class="">
                      <br class="">
                      <br class="">
                      openimportAgda.Builtin.Nat<br class="">
                      openimportAgda.Builtin.String<br class="">
                      openimportAgda.Builtin.Bool<br class="">
                      <br class="">
                      recordPair (A B :Set):Setwhere<br class="">
                        field<br class="">
                          fst :A<br class="">
                          snd :B<br class="">
                      <br class="">
                      _eq_ :(a :Pair Nat Nat)→(b :Pair Nat Nat)→Bool<br
                        class="">
                      a eq b =(Pair.fst a == Pair.fst b)∧(Pair.snd a ==
                      Pair.snd b)<br class="">
                      <br class="">
                      <br class="">
                      _______________________________________________<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="">
                      <br class="">
                    </blockquote>
                    _______________________________________________<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>
                </div>
              </blockquote>
            </div>
            <br class="">
          </div>
        </div>
      </div>
      <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>
  </body>
</html>