<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Thorsten,<div class=""><br class=""></div><div class="">I agree + is well behaved. The problem with \cup (in the context of set theory) is the disembodied idea of element. To go back to your original example, with {1,2} and {1,2,3,4} I can think of 1 as both in the first and the second set, so they are not disjoint, whereas {t,f} has empty intersection with {1,2,3,4} so their union is disjoint. (In fact the definition of + below takes care of making A and B disjoint.) </div><div class=""><br class=""></div><div class="">But I think the big defect, as I said, is the notion of “belongs to,” more than the notion of union per se. And again, the union is not just a coproduct: if I can avail myself of elements and of the intersection, then the union of A and B should be the pushout over A \cap B. Of course this bites its own tail, because how do you get a clean definition of intersection? If you can work over a base, say S, then given A —> S and B —> S, then you can define A \cap B as a fibered product and then A \cup B as a pushout. I believe that this way it should be invariant under isomorphisms. The troubles with elements remain, however.</div><div class=""><br class=""></div><div class="">—Ettore<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 5, 2020, at 15:01, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" class="">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" class="">
<div dir="auto" class="">
Hi Ettore,
<div class=""><br class="">
</div>
<div class="">We can look at both operations in the context of set theory. The sum is just the disjoint union ie </div>
<div class="">A+B = { (0,a) | a \in A } \cup { (1,b) | b \in B }<br class="">
<div class="">Now + preserves isomorphism of sets but \cup doesn’t. Hence in set theory we have both structural operations and non-structural ones while in Type Theory all operations are structural, ie preserve isomorphisms.</div>
<div class=""><br class="">
</div>
<div class="">Thorsten</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
<div dir="ltr" class="">Sent from my iPhone</div>
<div dir="ltr" class=""><br class="">
<blockquote type="cite" class="">On 5 Mar 2020, at 16:32, Ettore Aldrovandi <<a href="mailto:ealdrov@math.fsu.edu" class="">ealdrov@math.fsu.edu</a>> wrote:<br class="">
<br class="">
</blockquote>
</div>
<blockquote type="cite" class="">
<div dir="ltr" class=""> Hi Thorsten,
<div class=""><br class="">
</div>
<div class="">of course you are correct about the union of two sets (\cup). What I thought was not correct as an example is the comparison between \cup and +, because those are two different constructions, the latter being a disjoint union, or \sqcup, if we
want to use a different notation. </div>
<div class=""><br class="">
</div>
<div class="">I think I agree with the idea that types help hide the implementation, but the example as a whole does not support it because of \cup vs. \sqcup. From a categorical viewpoint, those are different types of colimits. The union, as in the rest of
my example, is a colimit along the index category {* <- * -> *}, whereas the disjoint union is a colimit along { * *} .</div>
<div class=""><br class="">
</div>
<div class="">I hope this clarifies it. Sorry for the confusion,</div>
<div class=""><br class="">
</div>
<div class="">—Ettore</div>
<div class=""><br class="">
<div class=""><br class="">
<blockquote type="cite" class="">
<div class="">On Mar 5, 2020, at 10:39, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" class="">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div class="WordSection1" style="page: WordSection1; caret-color: rgb(0, 0, 0); font-family: AgmenaPro-Regular; font-size: 16px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<span class="">Hi Ettore,<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<span class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<span class="">In set theory the union of two sets (written \cup) is the set which contains the elements which are in one set or the other. Hence I cannot see what is “mathematically incorrect” in my example<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<span class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<span class="">Cheers,<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<span class="">Thorsten<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<span class=""><o:p class=""> </o:p></span></div>
<div style="border-style: solid none none; border-top-width: 1pt; border-top-color: rgb(181, 196, 223); padding: 3pt 0cm 0cm;" class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<b class=""><span style="font-size: 12pt;" class="">From:<span class="Apple-converted-space"> </span></span></b><span style="font-size: 12pt;" class="">Ettore Aldrovandi <<a href="mailto:ealdrov@math.fsu.edu" class="">ealdrov@math.fsu.edu</a>><br class="">
<b class="">Date:<span class="Apple-converted-space"> </span></b>Wednesday, 4 March 2020 at 21:59<br class="">
<b class="">To:<span class="Apple-converted-space"> </span></b>Thorsten Altenkirch <<a href="mailto:psztxa@exmail.nottingham.ac.uk" class="">psztxa@exmail.nottingham.ac.uk</a>><br class="">
<b class="">Cc:<span class="Apple-converted-space"> </span></b>"<a href="mailto:coq-club@inria.fr" class="">coq-club@inria.fr</a>" <<a href="mailto:coq-club@inria.fr" class="">coq-club@inria.fr</a>>, agda-list <<a href="mailto:agda@lists.chalmers.se" class="">agda@lists.chalmers.se</a>>,
"<a href="mailto:coq+miscellaneous@discoursemail.com" class="">coq+miscellaneous@discoursemail.com</a>" <<a href="mailto:coq+miscellaneous@discoursemail.com" class="">coq+miscellaneous@discoursemail.com</a>>, lean-user <<a href="mailto:lean-user@googlegroups.com" class="">lean-user@googlegroups.com</a>><br class="">
<b class="">Subject:<span class="Apple-converted-space"> </span></b>Re: [Agda] [Coq-Club] Why dependent type theory?<o:p class=""></o:p></span></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
Hi,</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
I think the example below is not mathematically correct. The problem is that \cup is not the same as \sqcup. The latter is of course a coproduct in the category of sets, whereas the former is a push-out, so a colimit of a more complicated diagram. In the line </div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<blockquote style="margin-top: 5pt; margin-bottom: 5pt;" class="" type="cite">
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
{0,1} \cup {0,1,2,3} = {0,1,2,3}</div>
</div>
</blockquote>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
of course the two sets {0,1} and {0,1,2,3} are not disjoint, whereas in the line </div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<blockquote style="margin-top: 5pt; margin-bottom: 5pt;" class="" type="cite">
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
{true , false} \cup {0,1,2,3} = {true,false,0,1,2,3}</div>
</div>
</blockquote>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
the union is actually disjoint, i.e. a coproduct. In the example with the sum, </div>
</div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<blockquote style="margin-top: 5pt; margin-bottom: 5pt;" class="" type="cite">
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
<span lang="DE" class="">{0,1} + {0,1,2,3} = {in1 0,in1 1,in2 0,in2 1,in2 2,in2 3}</span></div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;">
<span lang="DE" class=""> </span></p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
<span lang="DE" class="">{true , false} + {0,1,2,3} = {in1 true,in1 false ,in2 0,in2 1,in2 2,in2 3}</span></div>
</div>
</blockquote>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
in the first line {0,1} is actually made disjoint from {0,1,2,3}. To turn this around, suppose you do a push-out</div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
{true, false} \coprod_{0,1} {0,1,2,3}</div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
where you use the maps f : {0,1} -> {true, false} and i : {0,1} ->{0,1,2,3} . Then, since f is an isomorphism, you get something isomorphic to the union. </div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
So, this example doesn’t really show that \cup exposes the implementation. But part of this example becomes possible because in sets we have naively “disembodied” elements leading to constructions of this sort…</div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
…I guess, I’m just learning this stuff myself. (First post here, actually!)</div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
Best,</div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
—Ettore</div>
</div>
<div class="">
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 12pt; font-size: 11pt; font-family: Calibri, sans-serif;">
<o:p class=""> </o:p></p>
<blockquote style="margin-top: 5pt; margin-bottom: 5pt;" class="" type="cite">
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
On Mar 4, 2020, at 04:42, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" style="color: blue; text-decoration: underline;" class="">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:</div>
</div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
<div class="">
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
First of all I don’t like the word “dependent type theory”. Dependent types are one important feature of modern Type Theory but hardly the only one.</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
To me the most important feature of Type Theory is the support of abstraction in Mathematics and computer science. Using types instead of sets means that you can hide implementation choices which is essential if you want to build towers of abstraction. Set
theory fails here badly. Just as a very simple example: in set theory you have the notion of union, so for example</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
{0,1} \cup {0,1,2,3} = {0,1,2,3}</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
However, if we change the representation of the first set and use lets say {true,false} we get a different result:</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
{true , false} \cup {0,1,2,3} = {true,false,0,1,2,3}</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
This means that \cup exposes implementation details because the results are not equivalent upto renaming. In Type Theory we have the notion of sum, sometimes called disjoint union, which is well behaved</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
<span lang="DE" class="">{0,1} + {0,1,2,3} = {in1 0,in1 1,in2 0,in2 1,in2 2,in2 3}</span></div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;">
<span lang="DE" class=""> </span></p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
<span lang="DE" class="">{true , false} + {0,1,2,3} = {in1 true,in1 false ,in2 0,in2 1,in2 2,in2 3}</span></div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
<span lang="DE" class=""> </span></p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
Unlike \cup, + doesn’t reveal any implementation details it is a purely structural operation. Having only structural operations means that everything you do is stable under equivalence, that is you can replace one object with another one that behaves the same.
This is the essence of Voevodsky’s univalence principle.</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
There are other nice aspects of Type Theory. From a constructive point of view (which should come naturally to a computer scientists) the proporsitions as types explanation provides a very natural way to obtain “logic for free” and paedagogically helpful since
it reduces logical reasoning to programming.</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
There are performance issues with implementations of Type Theory, however, in my experience (mainly agda) the execution of functions at compile time isn’t one of them. In my experience the main problem is to deal with a loss of sharing when handling equational
constraints which can blow up the time needed for type checking. I think this is an engineering problem and there are some suggestions how to fix this.</div>
</div>
<div class=""><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;">
</p>
</div>
<div class="">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
Thorsten</div>
</div>
</div>
</blockquote>
</div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">
<o:p class=""> </o:p></div>
</div>
</div>
<pre style="caret-color: rgb(0, 0, 0); font-size: 16px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">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>
<br class="Apple-interchange-newline">
</div>
</blockquote>
</div>
<br class="">
</div>
</div>
</blockquote>
</div>
</div>
<pre class="">
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></div>
_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>