European Calcified Tissue Society. ectsoc.org

ETCS sorry :P

ncatlab.org/nlab/show/ETCS

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

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

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

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

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

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

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

gosh, messages sent here really are logged for eternity

Yes, that PRISM program is quite thorough.

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.

oh no, arnav got redacted

maybe he was snowden the whole time?!!

You guys might appreciate this: familyecho.com/…

well that's nice

anybody know what scheme takes a ring $R$ to the set $R[x]/(x^n)$?