/sci/ - Science & Math

>>9521909
Hmm, good point. I guess my mistake was that a [math]\Sigma[/math] type is not simply some »[math]\Sigma_{x:A}P x[/math]«, but rather the collection of how to create and annihilate values of that type, and for those we need dependent functions, and for those we need [math]\Pi[/math] types.
In other words, the question was probably wrong, but it took someone else to make me realize it. Thanks :-)

>>9521463
Sup, I am (was) a tripfag back in the days when /sci/ was founded, around 2010/11/12, when I was finishing my Bachelor’s in (experimental) physics, before doing a master’s in theoretical physics. I talked a lot about math and relativity and the quantum world around here, but then lost interest and didn’t come here until now, when I realized I still had my tripcode lying around. And, to my surprise, googling my name with 4chan actually turned up some results.

Back then this board was quite active (no idea how it’s nowadays), people were sometimes discussing proper science, but other than that it was the usual 4chan shitshow. ICP brought up their »fuckin magnets how do they work« song so /sci/ was flooded with memes, [math]0.999\ldots\neq1[/math] trolls posted hourly, we had lots of infinite forces hitting walls of diamond, and we found out that [math]E=c[/math] thanks to Dr. Werner (»homeopathy with Dr. Werner« on Youtube).

Other tripfags I remember were Physics Guy, at the time doing a PhD I believe at CERN, and Harriet/EK which were desparate for attention without knowing shit about anything science, and being fully aware of that.

Oh, and the Emma Stone guy from above was also around during those days, except it seems he never left. :-)

>>9520967
Hacked together on the fly in a tiny textbox. Pic related, a proper version of it, captured from the HoTT intro section.
The general idea is that an existential type can be encoded using only universal quantifiers (as a rank-2 type). My question would now be whether we can somehow use existential quantifiers to encode an existential, going the other way round.
Application: Haskell only has universally quantified types (and rank-N with a language extension), allowing us to express existentials in it. Would it be possible to have a (granted, very esoteric) type system with only existentials that would be just as powerful?

>>9520955
You’re welcome! I learned quite a bit just hanging around there, and even got a free T-Shirt. Hooray! I wear it when bouldering mostly, gotta bring the math to the mountains ;-)

>>9520931
Well, there’s only so much you can do in life, and mathematics is a fairly lonely hobby. I found it very surprising how much of a time vs money trade getting a job was – I thought I spent a lot of time studying/working at uni, but boy is it different compared to a daytime job.

If you’re more knowledgeable, I’ve got a question (normal MLTT): an existentially quantified type can fairly easily be translated to a universally quantified one, [eqn]\sum_{x:A}P(x) = \prod_{y:B}\left(\prod_{x:A} \bigl(x,P(x) \bigr)\rightarrow y)\right) \rightarrow y[/eqn] – is the reverse possible as well somehow? I couldn’t come up with a proof in Agda, but also not a proof of its impossibility :-( (Let’s see how my Latex skills are holding up, fingers crossed…)

>>9520914
git diff :-P
All I know about HoTT is from the book, I’m not following current research on the topic. It’s just a hobby. But I’ve heard people talk about it on conferences a couple of times, typically with a doubting »I don’t think this is worth it« mindset.

>>9520924
At 12 we learn things like [math](a+b)^2 = a^2+2ab+b^2[/math], I don’t think that’s a good age to measure human achievement by.

>>9520894
Well, I graduated, and took a job that I quite enjoy. During my studies I used a lot of C++ and Mathematica (was one of the founders of mathematica.stackexchange.com) so I knew a bit about programming, then got hooked on Haskell and from there it was a slippery slope to learning about type theory on the theoretical, and compilers on the practical side. I’ve got a very nice job working on a compiler nowadays, so I’d say it paid off. High energy particle physics jobs are fairly rare on the free market ;-)

>>9520887
Funny, I went to a lute concert last month by accident – I didn’t know what I was getting into and then this guy started taking a seat on stage and played songs about the Euphrates, and told stories about how Flamenco was heavily influenced by Arabian music.

>>9520870
Interesting! What is it? That old Syrian instrument, what’s it called, Lut?

>>9520850
»Instrument«, I get it ;-)

>>9520823
> 'combined dimensions'.
Sounds very enterprise nonsensy. When I went to the US (from Germany) I flew Iceland or Singapore Air which were quite pleasant, I’ve heard only shitty things about Ryanair so far though so make sure you’ve really got your baggage right.

How about you ship your instrument via umm shipping, would that be an option?

>>9520794
Well, the author list features a couple of well-known mathematicians, including one (more?) Fields Medalists. HoTT is only a couple of years old, and even if I rejected the homotopical part of the book, it would be a very nice introduction to dependent types.
I was much more disappointed by reading about category theory, which was equally hard to understand than type theory, but so much less useful in the end. I guess it’s just not my cup of tea :-/

- /sci/ still exists, cool
- People are still posting my Latex guide, cool
- No magnet threads, no [math]0.999\ldots\neq1[/math] threads, cool
- No Dr. Werner mentioned, uncool. How are people to know that [math]E = c[/math]?

So I’ve left physics for computer science eventually, and instead of relativity I worry about type theory now (pic related, cover of HoTT).

I’ve got two hours to kill, so I’ll stay around a bit. inb4 nobody gives a fuck.

Testing my ancient tripcode… should become Josef !!nUf2NflSAyw, let’s see

Sci was average (!) for a few weeks after release, then the grads were annoyed and left.
After that, it consisted of troll threads (yes, I know, here on 4chan, incredible). See what happens: open another ".999 != 1" thread. Or an immovable object thread. Or a thread about the boy in OP's pic. Or a thread about E=mc^2. Or about Newtonian physics being wrong. You get the drift.
Now back to Stackexchange with me. Josef Hiatus go!

>>4362295
Not anymore, now that I've got Haskell.
Got to go now, need to finish this Mathematica simulation for tomorrow.

>>4362278
You could also use my email address.

>>4362108
>>4362148
Since "part of my answer is not allowed to be posted" (for no reason whatsoever), have an image of my reply.

sup

>>4232095
This.

>>4231937
Choose <span class="math">y=\lfloor x-1\rfloor[/spoiler], then <span class="math">y<x[/spoiler]. Therefore the statement is false.

Woops, spilled my coffee

>A vector is something with direction and magnitude
ASDSADRRRRRRRRRRRR FUCK THIS SENTENCE BECAUSE NO IT IS NOT
(rant ends here)

>Does this also apply for 235g of Uranium-235?
No, since the mass of the atom depends on the core configuration. An atom with mass number 235 only has an approximate mass of 235u.