Год с небольшим назад вышла статейка “Leibniz Equality is Isomorphic to Martin-Löf IdentityОна люто офигенная. Цитатка: Leibniz equality can be viewed as the Church encoding of Martin-Löf identity ( Read more... )

Зависимые теории типов с иерархиями вселенных не позволяют говорить о вещах типа “категория всех групп”, они лишь позволяют говорить о “категориях всех U-малых групп”, проблема хорошо известная людям, занимающимся теорией категорий в теории множеств Тарского-Гротендика (ZFC + всякое множество содержится в какой-то вселенной Гротендика). Как в ( Read more... )

Металлический водород, если он существует (на днях этому нашлось новое подтверждение: https://arxiv.org/pdf/1906.05634.pdf), вероятнее всего является классическим сверхпроводником с необыкновенно высокой критической температурой. У всех известных классических (т.е. БКШ-) ( Read more... )

Оказывается, с мая сего года есть наконец microSD-карты на 1TB. А Everspin буквально на днях начала производство гигабитных DDR4 чипов STT MRAM (энергонезависимой и очень быстрой памяти).

Доехать на машине из Подберлинья в Подмосковье менее чем за 24 часа двумя водителями с двумя детьми - check. Потребление, кстати, на каждого пассажира 1.8 литра на 100км, раза в полтора-два ниже, чем если самолётом лететь.

Из комментов, цитата 1: «В смысле "когда RedPRL станет столь же удобен как ХХХ, то можно считать, что [..] применима в учебном процессе" - что здесь будет ХХХ?»

Такого XXX сейчас нет целиком, но можно собрать по частям. ( Read more... )

Первая половина 2019-го оказалась урожайна на результаты касательно семантики Гомотопической Теории Типов.( Read more... )

Уж довольно много лет назад, плата за общественное радио и телевидение в Германии перестала взыматься по факту наличия радио или телевизора, а стала просто ещё одним налогом. Не платой за потребление контента а налогом на поддержание платформ, где проходят предвыборные дебаты и другие подобные общественно не просто полезные, но необходимые вещи. ( Read more... )

Я только что обнаружил, что Ален Конн выпустил две новые публикации про топосы и “поле” характеристики 1 - «Spec Z and the Gromov norm» и «Un topo sur les topos». Первую я только начал просматривать, а
вторая оказалась по-французски (так что я там очень не всё понимаю), но не техническая, а обзорная, очень клёвая. Leave a comment

Если говорить про высокий КПД, то нельзя не поговорить об освещении. Раньше были лампочки накаливания и всякие там газоразрядные лампы, сейчас наступил век светодиодов. У обычных светодиодов есть свои известные ограничения, но КПД (в данном случае, правильное мерило - External Quantum Efficiency) у них бывает совершенно умопомрачительный. ( Read more... )