User matthew willis - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-21T07:10:43Z http://mathoverflow.net/feeds/user/5700 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system What is the intuitive meaning of star and box in a pure type system? Matthew Willis 2010-04-29T19:56:34Z 2011-01-29T18:55:35Z <p>The systems of the &lambda;-cube have the axiom $\star:\square$.</p> <p>I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\square$ in each interpretation?</p> <p>$t : T : \star : \square$</p> <p><strong>Programs:</strong> t is a program of type T. (Possibility: T is a program of type $\star$?)</p> <p><strong>Proofs:</strong> t is a proof of theorem T. It's hard to see T as a proof of $\star$, though.</p> <p><strong>Set elements:</strong> t is a member of set T. (Possibility: T is a member of the universe $\star$ of sets. Then it seems difficult to assign a meaning to $\square$ that avoids the membership $\square : \star$.)</p> <p>I'd like to fill out this table both vertically and horizontally, with both further interpretations and the missing descriptions of $\star$ and $\square$, and possibly meanings of $T : \square$ for $T \neq \star$.</p> <p>Thank you!</p> http://mathoverflow.net/questions/23250/what-is-the-earliest-definition-given-by-a-universal-mapping-property What is the earliest definition given by a universal mapping property? Matthew Willis 2010-05-02T11:53:55Z 2010-05-05T01:22:29Z <p>As I study category theory, I'm finding the use of universal mapping properties in defining basic concepts to be both simple and clever. Yet, the idea seems non-obvious enough that I expect quite a bit of mathematics had been done before the discovery of the technique.</p> <blockquote>What is the chronologically earliest abstract definition given by a universal mapping property?</blockquote> <p>Note that this question is not intended to be restricted to category theory.</p> <p>Thank you!</p> http://mathoverflow.net/questions/22941/is-an-infinite-compositions-of-arrows-meaningful Is an "infinite compositions of arrows" meaningful? Matthew Willis 2010-04-29T05:17:36Z 2010-04-29T06:08:34Z <p>For example, deciding whether or not the following is a category seems to depend on the above question (from Awodey's Category Theory, pg. 6):</p> <blockquote>"What if we take sets as objects and as arrows, those $f : A \rightarrow B$ such that for all $b \in B$, the subset $f$<sup>-1</sup>$(b) \subseteq A$ is finite?"</blockquote> <p>Define for each $n \in N$ the function $f$<sub>n</sub>: $N \rightarrow N$ where $f$<sub>n</sub>$(x) = max(0, x - n)$.</p> <p>Then any $f$<sub>n</sub> or any finite composition thereof has finite inverse images. Yet the "infinite composition" $... f$<sub>1</sub>$f$<sub>2</sub>$f$<sub>0</sub> has an infinite inverse image for 0, and so the above does not meet the definition of a category.</p> <p>If this "infinite composition" is legit, does it follow from the basic definition of a category, or must the definition be made more flexible or precise to accommodate it?</p> <p>For reference, this is Awodey's definition concerning composition:</p> <blockquote>"Given arrows $f : A \rightarrow B$ and $g : B \rightarrow C$, [...] there is given an arrow: $g$ o $f : A \rightarrow C$ called the composite of $f$ and $g$."</blockquote> <p>Thank you for your insight.</p> http://mathoverflow.net/questions/29499/yet-another-roadmap-style-request-a-second-bite-of-the-cherry/29569#29569 Comment by Matthew Willis Matthew Willis 2010-06-26T05:54:45Z 2010-06-26T05:54:45Z By independent study course are you referring to meeting periodically with a professor without being enrolled at their (or any) university? http://mathoverflow.net/questions/23250/what-is-the-earliest-definition-given-by-a-universal-mapping-property Comment by Matthew Willis Matthew Willis 2010-05-02T12:16:03Z 2010-05-02T12:16:03Z Thank you for the citation! To clarify, I'm asking not about when the idea of a UMP was itself generalized, but rather the first instance of the (I expect) many cases from which the generalization was eventually drawn. http://mathoverflow.net/questions/23032/what-is-the-intuitive-meaning-of-star-and-box-in-a-pure-type-system/23044#23044 Comment by Matthew Willis Matthew Willis 2010-04-30T02:10:15Z 2010-04-30T02:10:15Z Then for the &quot;Programs&quot; interpretation we have: t is a program of type T classified by * classified by square. I was hoping that the relationships would stay the same within a given interpretation: if we say that t is a program of type T, then it seems that T should be some kind of program of type *. Then perhaps * is the type of type-checking programs? http://mathoverflow.net/questions/22941/is-an-infinite-compositions-of-arrows-meaningful/22947#22947 Comment by Matthew Willis Matthew Willis 2010-04-29T11:39:58Z 2010-04-29T11:39:58Z I haven't learned about limits and colimits in categories yet. Perhaps that will shed some light on the subject. http://mathoverflow.net/questions/22941/is-an-infinite-compositions-of-arrows-meaningful/22945#22945 Comment by Matthew Willis Matthew Willis 2010-04-29T11:36:58Z 2010-04-29T11:36:58Z @Pete: This makes the question even more striking in my view. For example, let's say we have the monoid {0,1} with operation xor and try to count its arrows. Should it have two arrows corresponding to the two elements of the monoid? What about the infinite composition ..0101.. (or the source-target-friendly 1..0101..0), which is neither equal to 0 nor to 1? I think this is the essence of my original question.