<div dir="ltr">Hi all,<div><br></div><div>In trying to answer the following question from the <i>Negation</i> chapter of PLFA:</div><div><br></div><div><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">Do we also have the following?</p><div class="gmail-language-plaintext gmail-highlighter-rouge" style="color:rgb(17,17,17);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)"><div class="gmail-highlight" style="margin-bottom:15px;background:rgb(238,238,255)"><pre class="gmail-highlight" style="margin-top:0px;margin-bottom:15px;padding:0.4em;font-size:15px;border:1px dashed rgb(201,225,246);border-radius:3px;background-image:initial;background-position:initial;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;overflow-x:auto;break-inside:avoid"><code style="font-size:0.85em;border:0px;border-radius:3px;padding:1px 0px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif">¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
</code></pre></div></div><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?</p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">It seems to me that I ought to be able to define an <i>embedding</i>. That is, I should <i>not</i> have to settle for just an <i>equivalence</i>:</p></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><font face="monospace">×-dual-⊎ : ∀ {A B : Set}<br></font><font face="monospace">    -------------------------<br></font><font face="monospace">  → ¬ (A × B) ≲ (¬ A) ⊎ (¬ B)<br></font><font face="monospace">×-dual-⊎ =<br></font><font face="monospace">  record<br></font><font face="monospace">    { to      = λ ¬A×B → inj₁ (λ a → ¬A×B (a , _))<br></font><font face="monospace">    ; from    = λ { (inj₁ ¬A) → λ (a , _) → ¬A a<br></font><font face="monospace">                  ; (inj₂ ¬B) → λ (_ , b) → ¬B b<br></font><font face="monospace">                  }<br></font><font face="monospace">    ; from∘to = λ ¬A×B → extensionality (λ (a , _) → refl<br></font><font face="monospace">    -- ; to∘from = λ { (inj₁ ¬A) → -- We could write this one.<br></font><font face="monospace">    --               ; (inj₂ ¬B) →<br></font><font face="monospace">    --               -- Can't write this, due to choice of `inj₁` for `to`, above.<br></font><font face="monospace">    --               }<br></font><font face="monospace">    }</font></blockquote><div><br></div><div>However, when I try the code above, I get:</div><div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="monospace">Cannot instantiate the metavariable _140 to solution</font></div><div><font face="monospace">snd(.patternInTele0) since it contains the variable</font></div><div><font face="monospace">snd(.patternInTele0) which is not in scope of the metavariable</font></div><div><font face="monospace">when checking that the expression refl has type</font></div><div><font face="monospace">(λ { (inj₁ ¬A)</font></div><div><font face="monospace">       → λ .patternInTele0 → ¬A (Data.Product.proj₁ .patternInTele0)</font></div><div><font face="monospace">   ; (inj₂ ¬B)</font></div><div><font face="monospace">       → λ .patternInTele0 → ¬B (Data.Product.proj₂ .patternInTele0)</font></div><div><font face="monospace">   })</font></div><div><font face="monospace">(inj₁ (λ a → ¬A×B (a , _snd_140 (¬A×B = ¬A×B) (a = a))))</font></div><div><font face="monospace">.patternInTele0</font></div><div><font face="monospace">≡ ¬A×B .patternInTele0</font></div></blockquote><div><br></div><div>Any thoughts?</div><div><br></div><div>Thanks,</div><div>-db</div><div>:)</div><div><br></div></div>