next day →
last day (3404 days later) »
05:00 - 06:00
06:00 - 07:00
07:00 - 20:00
20:00 - 00:00
Jon Beardsley
8:00 PM
European Calcified Tissue Society.
ectsoc.org
Will
ETCS sorry :P
ncatlab.org/nlab/show/ETCS
Jon Beardsley
aha i see
Will
but what does make sense in that context is taking pullbacks
Jon Beardsley
right
Will
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
Jon Beardsley
8:03 PM
aha yeah.... just.... keep going around the circle
lol
Will
$ 0 : \mathbb{N}$ and $S : \mathbb{N} \to \mathbb{N}$
Jon Beardsley
i mean not really. but i get what you're saying
Will
but these are just type constructors really
Jon Beardsley
i'd never heard of ETCS actually, but I like that
right, i remember those at least, haha
Will
like if you were to define natural numbers in a programming languages like that
Jon Beardsley
8:04 PM
yeah totally
Will
(although it kind of means doing it in unary)
a natural number is 0 or it is the successor of a natural number
Jon Beardsley
soooooo is HOTT, is $S^1$ something like the natural numbers object for $\infty$-topoi?
Will
well no
Jon Beardsley
oh, bummer
Will
I was just saying that $\mathbb{N}$ is an example of a type given by type constructors
Jon Beardsley
8:05 PM
sure
Will
but there everything was just at the level of ordinary logic or whatever
Jon Beardsley
yeah
Will
whereas here we're allowed higher homotopical type constructors
Jon Beardsley
right. like, paths between paths
Will
yes
Jon Beardsley
8:06 PM
yeah, it's funny, from that POV it seems like logic is really uneccesarily truncated
Will
yes
Jon Beardsley
:)
Will
plus I think it's close to a lot of standard ways of doing things
e.g. when you're presenting groups
Jon Beardsley
oh, like ,internal hom objects?
Will
no I mean a group presentation
Jon Beardsley
8:09 PM
oh, you're referring to type constructors
Will
instead of being generated by some elements subject to some axioms (relations)
you're generated by some elements and some paths between elements
Jon Beardsley
uhuh. sure. yeah
so is this what you work on? I'm not really clear on who you are.
Will
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
Jon Beardsley
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
Will
although I guess "algebraic varieties up to homotopy" is not something you want to be seen thinking about
Jon Beardsley
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
Will
yes but that's not the same notion of homotopy
Jon Beardsley
homotopy theory of schemes, in some sensible way
yeah.... i guess not
Eric
8:52 PM
gosh, messages sent here really are logged for eternity
Evan Jenkins
Yes, that PRISM program is quite thorough.
Jon Beardsley
9:08 PM
that's somewhat unsettling i guess. but on the other hand, i don't suppose i have too much to hide
Eric
i'm prone to gossip which is why i'm nervous
Evan Jenkins
I'm prone to making Coq-related double entendres.
Matthew Pancia
10:09 PM
oh no, arnav got redacted
maybe he was snowden the whole time?!!
1 hour later…
Evan Jenkins
11:20 PM
You guys might appreciate this:
familyecho.com/…
Jon Beardsley
11:48 PM
well that's nice
anybody know what scheme takes a ring $R$ to the set $R[x]/(x^n)$?
05:00 - 06:00
06:00 - 07:00
07:00 - 20:00
20:00 - 00:00
next day →
last day (3404 days later) »
all rooms
Transcript for
Jun '13
27
Jun
28
Homotopy Theory
A room for anyone interested in homotopy theory, or any nearby...
homotopy-theory
join this room
about this room
00:00
06:00
12:00
18:00
all times are UTC
site design / logo © 2024 Stack Exchange Inc;
legal
mobile