<div dir="auto">Just want to post some other things if someone is interested about using Yoneda.<div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">Because Void -> a is unique, (Yo void) is terminal in [C, Set].  We can convert the (a -> void) -> (b -> void) as Yo a ~> Yo b.</div><div dir="auto"><br></div><div dir="auto">Some details are attached.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, May 16, 2020, 3:58 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank" rel="noreferrer">olf@aatal-apotheke.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> 2. Double negation enables a translation of classical logic in <br>
> intuitionistic logic, here embedded in Haskell:<br>
> <br>
Below I'll give a variant of Li-yao's logic language in Haskell98. <br>
Again, the open set model may help to visualize CPS translation: <br>
<br>
Consider all open sets A on the real line which are fixed points of<br>
double negation. All intervals are of this kind, but poking holes in<br>
them destroys this property:<br>
<br>
---(====)(====)--- A<br>
===)----------(=== Not A<br>
---(==========)--- Not (Not A)<br>
<br>
Denote the collection of open sets invariant under double negation by<br>
X. As the example above demonstrates, X is not closed under set union.<br>
But set intersection preserves membership of X. So we have a funny<br>
logic that has (&&) but no (||). The CPS trick is now to define a new<br>
(||) by means of double negation:<br>
<br>
---(====)--------- A<br>
---------(====)--- B<br>
---(====)(====)--- set union of A and B<br>
---(==========)--- A || B, double negation of set union.<br>
<br>
In fact X is the largest Boolean algebra contained in the Heyting<br>
algebra of open sets. In terms of Haskell, we define a new Either:<br>
<br>
Either' a b = ((Either a b) -> Void) -> Void<br>
<br>
Looks familiar? Indeed, in this thread we already proved<br>
<br>
Either' a (Not a).<br>
<br>
This says that Not A is the Boolean complement of A in X. Using (,) and<br>
Either' for (&&) and (||) you can realize all proofs of classical<br>
propositional logic in Haskell without GADTs. <br>
<br>
Olaf<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>