<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>