last day (1849 days later) » 

8:00 PM
European Calcified Tissue Society. ectsoc.org
 
aha i see
 
but what does make sense in that context is taking pullbacks
 
right
 
and so yes it ETCS you have a natural numbers object
and that is similar
it's a type generated by a point and a function
 
8:03 PM
aha yeah.... just.... keep going around the circle
lol
 
$ 0 : \mathbb{N}$ and $S : \mathbb{N} \to \mathbb{N}$
 
i mean not really. but i get what you're saying
 
but these are just type constructors really
 
i'd never heard of ETCS actually, but I like that
right, i remember those at least, haha
 
like if you were to define natural numbers in a programming languages like that
 
8:04 PM
yeah totally
 
(although it kind of means doing it in unary)
a natural number is 0 or it is the successor of a natural number
 
soooooo is HOTT, is $S^1$ something like the natural numbers object for $\infty$-topoi?
 
well no
 
oh, bummer
 
I was just saying that $\mathbb{N}$ is an example of a type given by type constructors
 
8:05 PM
sure
 
but there everything was just at the level of ordinary logic or whatever
 
whereas here we're allowed higher homotopical type constructors
 
right. like, paths between paths
 
yes
 
8:06 PM
yeah, it's funny, from that POV it seems like logic is really uneccesarily truncated
 
yes
 
plus I think it's close to a lot of standard ways of doing things
e.g. when you're presenting groups
 
oh, like ,internal hom objects?
 
no I mean a group presentation
 
8:09 PM
oh, you're referring to type constructors
 
instead of being generated by some elements subject to some axioms (relations)
you're generated by some elements and some paths between elements
 
uhuh. sure. yeah
so is this what you work on? I'm not really clear on who you are.
 
I guess I'm not really saying anything, I just love Euler characteristic
hahaha no I just picked up on this when the HoTT book came out
 
i see
yeah i wish it had been out about 1.5 years ago, when i was trying to understand this stuff
now i've kind of veered off onto something else, i guess trying to write a thesis that won't require me to learn a programming language or something
and also, a thesis that my advisor and the people at my school actually know stuff about, haha, which is nice.
or are at least interested in knowing stuff about
so somehow.... yeah, it seems like types corresponding to systems of equations should somehow be connected to AG in some way
 
although I guess "algebraic varieties up to homotopy" is not something you want to be seen thinking about
 
8:14 PM
well
i mean.... motives... right?
i kind of got the sense that's what motives were kind of getting at, in some sense
 
yes but that's not the same notion of homotopy
 
homotopy theory of schemes, in some sensible way
yeah.... i guess not
 
8:52 PM
gosh, messages sent here really are logged for eternity
 
Yes, that PRISM program is quite thorough.
 
9:08 PM
that's somewhat unsettling i guess. but on the other hand, i don't suppose i have too much to hide
 
i'm prone to gossip which is why i'm nervous
 
I'm prone to making Coq-related double entendres.
 
10:09 PM
oh no, arnav got redacted
maybe he was snowden the whole time?!!
 
 
1 hour later…
11:20 PM
You guys might appreciate this: familyecho.com/…
 
11:48 PM
well that's nice
anybody know what scheme takes a ring $R$ to the set $R[x]/(x^n)$?
 

  last day (1849 days later) »