<div dir="auto">As with the physical entities described by the math in Baez's book, I feel that I have a leg up on understanding the math but not so much on the relationship to the described entities.  It must be my aversion to the real world.<br><br><div data-smartmail="gmail_signature">---<br>Frank C. Wimberly<br>140 Calle Ojo Feliz, <br>Santa Fe, NM 87505<br><br>505 670-9918<br>Santa Fe, NM</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, May 26, 2020, 8:21 PM Jon Zingale <<a href="mailto:jonzingale@gmail.com">jonzingale@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">Glen,<br><br>I am really enjoying steelmaning and getting steel-mansplained,<br>so thank you for the discussion up to this point. For me the<br>images are that of the constructions for <a href="https://en.wikipedia.org/wiki/Free_module" target="_blank" rel="noreferrer">free modules</a> over a ring,<br>dependent types, and <a href="https://en.wikipedia.org/wiki/Algebraic_variety" target="_blank" rel="noreferrer">algebraic varieties</a>. In the first case, there<br>is a natural interplay between the category of sets and the category<br>of modules, equipped with a map describing <i>inclusions</i> of bases into<br>the collection of vectors they span, and a map describing how to<br><i>evaluate</i> a vector in a context to return a single number. The thing<br>I find relevant here is that while the evaluation function does<br>much to <i>found</i> the module (a vector space say), the <i>evaluation</i> is<br>not what is interesting about the module. What is interesting is that<br>we have a playground to talk about <i>dimension</i>, to make metaphors about<br>phenomenological experiences of space, and most importantly to play and<br>entertain one another. The whole game comes to an end the minute we</div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">finally concatenate the <i>evaluation</i> function onto the end of our compositions.</div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">The entire notion of space collapses and we are left with a single number.</div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">To your comments on free/bound variables, I can interpret these bases as</div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">bindings for the underlying ring and the coefficients as representing free</div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">variables (do I have that right?). </div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><br>I don't have much to write that is specific to dependent types<br>that would be all that different from the algebraic variety image,<br>so let me jump next to there. Varieties are often described in terms<br>of comprehension or inverse images. For instance in pseudo-Haskell<br>I can write:<br><br><font face="monospace">conicVariety = [ (x,y,z) | (x,y,z) <- R3, x² + y² + z² == 1]</font><br><br>Varieties as you can image get pretty nasty (singularities, cusps, etc..)<br>This no doubt made the development of algebraic geometry much more<br>treacherous than the study of manifolds, its tamer sibling. What is<br>novel about the varieties like conicVariety above is that it can be<br>understood in terms of sections. We can interpret the function above<br>as asking for the collection of all triples which all map to 1, and<br>when we do we have a fiber in hand. What is relevant here is the image<br>that as we collapse states-of-affairs onto objects of designation,<br>we get variety-like objects in the space of affairs. As conversants<br>collaboratively build fibers over designations, they are constructing<br>eidetic variations of concepts. Somehow in the sense of EricS, the<br>collection of these variety-like concepts are personal and irreducible<br>complexes of meaning.<br></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><br></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">Jon</div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><br></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)">ps. I will look up 'Dies the Fire'</div></div>
-- --- .-. . .-.. --- -.-. -.- ... -..-. .- .-. . -..-. - .... . -..-. . ... ... . -. - .. .- .-.. -..-. .-- --- .-. -.- . .-. ...<br>
FRIAM Applied Complexity Group listserv<br>
Zoom Fridays 9:30a-12p Mtn GMT-6  <a href="http://bit.ly/virtualfriam" rel="noreferrer noreferrer" target="_blank">bit.ly/virtualfriam</a><br>
un/subscribe <a href="http://redfish.com/mailman/listinfo/friam_redfish.com" rel="noreferrer noreferrer" target="_blank">http://redfish.com/mailman/listinfo/friam_redfish.com</a><br>
archives: <a href="http://friam.471366.n2.nabble.com/" rel="noreferrer noreferrer" target="_blank">http://friam.471366.n2.nabble.com/</a><br>
FRIAM-COMIC <a href="http://friam-comic.blogspot.com/" rel="noreferrer noreferrer" target="_blank">http://friam-comic.blogspot.com/</a> <br>
</blockquote></div>