564 reputation
210
bio website natesoares.com
location
age 24
visits member for 3 years, 1 month
seen 2 days ago

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 suggested 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$?
Jun
10
awarded  Yearling
Jun
10
comment Why do we write second derivatives like $\frac{d^2x}{dt^2}$
This makes very little sense to me. How come we can separate the $d$ from $x$ in $dx$, but we can't separate the $d$ from $t$ in $dt$? What are these $d$ things anyway, and why do we treat the one attached to $x$ differently from the one attached to $t$?
Jun
10
asked Why do we write second derivatives like $\frac{d^2x}{dt^2}$
May
23
awarded  Popular Question
Oct
28
awarded  Popular Question
May
23
revised Generalizing an alternative derivation of distance
added 85 characters in body
May
22
comment Generalizing an alternative derivation of distance
@JonasMeyer you're right, it's independent of the cosine rule and just dependent upon the definition of cosine -- I just didn't notice it until I was working through the derivation of the Pythagorean theorem from the cosine rule alone.