<div dir="ltr">Ah, thanks!<div><br></div><div>With that help, my code is compiling, but I'm getting some unsolved constraint errors:</div><div><br></div><div><font face="monospace">  _82 (C→A⇒D = (λ C₁ â†’ Æ› (λ A₁ â†’ C×A→D (C₁ , A₁)))) = Set<br>  _83 (C→A⇒D = (λ C₁ â†’ Æ› (λ A₁ â†’ C×A→D (C₁ , A₁)))) = C Ã— A<br></font></div><div><br></div><div>I don't really understand them.</div><div>Is there something in the Agda docs on this that you could point me to?</div><div><br></div><div>Thanks,</div><div>-db</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 14, 2021 at 2:29 PM Oleg Grenrus <<a href="mailto:oleg.grenrus@iki.fi">oleg.grenrus@iki.fi</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">See<br>
<a href="https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#example-the-pair-type-constructor" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#example-the-pair-type-constructor</a>,<br>
specifically the last paragraphs about `constructor` keyword.<br>
<br>
- Oleg<br>
<br>
On 15.1.2021 0.21, David Banas wrote:<br>
> Thanks, Oleg!<br>
> Is this correct?:<br>
><br>
>  Â  Â 55 record _×_ (A : Set) (B : Set) : Set where<br>
>  Â  Â 56 Â  field<br>
>  Â  Â 57 Â  Â  fst : A<br>
>  Â  Â 58 Â  Â  snd : B<br>
>  Â  Â 59 Â  Â Â <br>
>  Â  Â 60 _,_ : âˆ€ {A B : Set} A â†’ B â†’ (A Ã— B)<br>
>  Â  Â 61 x , y = record {fst = x; snd = y}<br>
><br>
><br>
> It seems to work, in general, but is giving me the following error,<br>
> re: my Functor instance:<br>
><br>
>  Â  Â ###.agda:112,3-36<br>
>  Â  Â Could not parse the left-hand side<br>
>  Â  Â fmap â¦ƒ ProductFunctor â¦„ f (x , y)<br>
>  Â  Â Operators used in the grammar:<br>
>  Â  Â Â  , (infix operator, level 20) [_,_ (###.agda:60,1-4)]<br>
>  Â  Â when scope checking the left-hand side<br>
>  Â  Â fmap â¦ƒ ProductFunctor â¦„ f (x , y) in the definition of<br>
>  Â  Â ProductFunctor<br>
><br>
><br>
> For reference, here is that Functor instance:<br>
><br>
>  Â  Â 110 instance<br>
>  Â  Â 111 Â  ProductFunctor : âˆ€ {A : Set} â†’ Functor (_× A)<br>
>  Â  Â 112 Â  fmap {{ProductFunctor}} f (x , y) = (f x , y)<br>
><br>
><br>
> Thanks,<br>
> -db<br>
><br>
><br>
>> On Jan 14, 2021, at 12:08 PM, Oleg Grenrus <<a href="mailto:oleg.grenrus@iki.fi" target="_blank">oleg.grenrus@iki.fi</a><br>
>> <mailto:<a href="mailto:oleg.grenrus@iki.fi" target="_blank">oleg.grenrus@iki.fi</a>>> wrote:<br>
>><br>
>> You need to define the type as a record.<br>
>><br>
>> See<br>
>> <a href="https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#eta-expansion" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#eta-expansion</a><br>
>><br>
>> - Oleg<br>
><br>
</blockquote></div>