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 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 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 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$^-1$(b) \subseteq A$ is finite?"</blockquote> <p>Define for each $n \in N$ the function $f$_n: $N \rightarrow N$ where $f$_n$(x) = max(0, x - n)$.</p> <p>Then any $f$_n or any finite composition thereof has finite inverse images. Yet the "infinite composition" $... f$₁$f$₂$f$₀ 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 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 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 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 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 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.