Nate
Reputation
684
Top tag
Next privilege 1,000 Rep.
Create new tags
 Sep 13 accepted Equalizers and Basic limit theorem in Category theory Sep 13 comment Equalizers and Basic limit theorem in Category theory Yeah, it seems that $I$, $J$, ... are indeed intended to index the objects $D_I$, $D_J$, ... of $\textbf{D}$. Apologies; this syntax is somewhat new to me. Sep 13 revised Equalizers and Basic limit theorem in Category theory added 12 characters in body Sep 13 comment Equalizers and Basic limit theorem in Category theory Oh, that was just me being sloppy when summarizing the proof in the book. In the book, $I$ and $J$ are the notation used when referring to elements of $V$ (i.e. only in the indexing of the products), while $D_I$ and $D_J$ are used when referring to objects of $\textbf{D}$ (which are indeed the same, unless I'm missing something). Sorry. I'll go back and edit. Sep 13 comment Equalizers and Basic limit theorem in Category theory @KarlKronenfeld, that's precisely what I was missing, thanks. Care to write up an answer? Sep 13 comment Equalizers and Basic limit theorem in Category theory But limits require that for any limit $X$ with arrow $f_i : X \rightarrow D_i$ in the limit and arrow $g : D_i \rightarrow D_j$ in the diagram, $f_j = g \circ f_i$. If we ignore extra $D_e : D_I \rightarrow D_J$ in the proof then it seems like there are arrows in the diagram (the ignored arrows) that could violate this equation. Sep 13 asked Equalizers and Basic limit theorem in Category theory Aug 4 revised Confusion about Homotopy Type Theory terminology added 17 characters in body Aug 3 comment Confusion about Homotopy Type Theory terminology So the section immediately following dependent sums discusses coproduct types, which answers my first question. I'm still curious as to the nature of superexponential types. Are they inhabited by functions of multiple variables? Aug 3 comment Confusion about Homotopy Type Theory terminology Neat. I suppose you could go a step further and say that there's a Successor type data Succ a = Zero | Succ a (known as Maybe to programmers), and then generalize sum types $A + B$ as dependent succession $Succ_{x:A} B$, and then generalize Succession as dependent unity and complete the pattern. Out of curiosity, what do you call independent types that generalize into dependent exponents (i.e. superexponential types), and what would they look like? Aug 3 accepted Confusion about Homotopy Type Theory terminology Aug 3 comment Confusion about Homotopy Type Theory terminology Oh. Neat. I feel silly now. Want to write that up as an answer? Aug 3 asked Confusion about Homotopy Type Theory terminology Jun 17 comment How do you combine the bipartite function $y=2^{x-1}$ for $x\lt0$ & $y=1-2^{-x-1}$ for $x\ge0$? My confusion was rooted in the fact that the function is not continuously differentiable. Now I feel silly. Jun 17 accepted How do you combine the bipartite function $y=2^{x-1}$ for $x\lt0$ & $y=1-2^{-x-1}$ for $x\ge0$? Jun 17 answered How do you combine the bipartite function $y=2^{x-1}$ for $x\lt0$ & $y=1-2^{-x-1}$ for $x\ge0$? Jun 12 revised How do you combine the bipartite function $y=2^{x-1}$ for $x\lt0$ & $y=1-2^{-x-1}$ for $x\ge0$? Typo fix: the lt/ge signs were swapped. Jun 12 suggested approved edit on How do you combine the bipartite function $y=2^{x-1}$ for $x\lt0$ & $y=1-2^{-x-1}$ for $x\ge0$? Jun 12 comment How do you combine the bipartite function $y=2^{x-1}$ for $x\lt0$ & $y=1-2^{-x-1}$ for $x\ge0$? Sure -- but is their a unified equation for the function? It feels like there should be. Jun 12 asked How do you combine the bipartite function $y=2^{x-1}$ for $x\lt0$ & $y=1-2^{-x-1}$ for $x\ge0$?