8:00 PM
European Calcified Tissue Society. ectsoc.org

ETCS sorry :P

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

yeah

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)$?