<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body dir="auto">
There is no information in the left hand side but there is one bit of information on the right. Where should it come from?
<div><br>
</div>
<div>Knowing that it cannot be that both A and B are false doesn’t tell you which is not false.</div>
<div>
<div><br>
<div dir="ltr">Sent from my iPhone</div>
<div dir="ltr"><br>
<blockquote type="cite">On 22 Aug 2020, at 22:48, David Banas <capn.freako@gmail.com> wrote:<br>
<br>
</blockquote>
</div>
<blockquote type="cite">
<div dir="ltr">
<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>
<span>_______________________________________________</span><br>
<span>Agda mailing list</span><br>
<span>Agda@lists.chalmers.se</span><br>
<span>https://lists.chalmers.se/mailman/listinfo/agda</span><br>
</div>
</blockquote>
</div>
</div>
<PRE>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</PRE></body>
</html>