> physics is just tricking nature into doing calculations for you

СУКААА

ТЕОРЕТИЧЕСКИЙ ИНФОРМАТИК ИЗ ОДЕССЫ

НА ТУСОВКЕ

РУССКИЙ НАЦИОНАЛИСТ

я пиздел с ним час про рунатскую тусовку

у них есть чат русских националистов в берлине

самое смешное что я общался с ним периодически здесь но на английском и не знал что он говорит по русски

когда я уходил, он обсуждал рецепты борща с немцем, который курит сигары и у него усы как у николая 2

темами для обсуждения за сегодня стали:

теорем пруверы и гомотопичкеская теория типов (да да я)

теорию сложности и вычислимости

рецепты борща

инвазивные виды в америке на примере сверхкабанов (моя любимая тема)

использование машин лернинга для считывания эмоций с мрт

поэзию фернандо пессоа и дмитрия пригова (да да я)

русскую классику (очевидно не читал)

риталин и аддералл

почему не стоит набивать тату с именами партнеров

food forests в морокко

торговля оружия в румынии

рейвы в лесу

как выбирать немецкое пиво

мои пробежки до автобусов в 2 часа ночи

ТЕОРИЯ МНОЖЕСТВ против Кирилла Мартынова

доебываю его вопросами про теорию категорий и HoTT

> I like you. I can't learn shit talking to CS people.

когда такие люди называют себя бегиннерами мне страшно представить в какую категорию вписываюсь я

ай ай ай назадавал сложных вопросов теперь сложно думать и голова болит

WHYYYYY

higher observational type theory? sucks

why does it suck? i don' understand it.

Зафиксирую: HoTT is intensional even though it usually takes FunExt as an axiom or as a theorem, since it doesn't have UIP. UIP holds in set-theoretic models aka "types as sets" of ITT/HoTT, but not in simplicial/cubical-sets models (aka types are indeed 8-grpds, where every model deals with higher paths in its own fashion). In MLTT identity types are inductive type families (thus intensionality and 8-grpd structure) and UA allows to calculфte path spaces of higher inductives. ERR implies UIP since it allows to get definitional equality from an inhabitant of identity type (aka there is a witness of equality between term p of identity type Id_A(a,b) and refl(a)) . In homotopical interpretation UIP trivilizes higher paths ---> UIP + FunExt = extensionality and ERR also implies FunExt. Done.

от меня отписался некий сергей

сергей, вы гей