at last

 

(src)

 

A Formal Logic for Formal Category Theory

Max S. New, Daniel R. Licata

We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linear restriction on standard predicate logic, which guarantees that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proofs necessary. Important category theoretic proofs such as the Yoneda lemma and Co-yoneda lemma become simple type theoretic proofs about the relationship between unit, tensor and (ordered) function types, and can be seen to be ordered refinements of theorems in predicate logic. The type theory is sound and complete for a categorical model in \emph{virtual equipments}, which model both internal and enriched category theory. While the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensure that all proofs and constructions carry over to enriched and internal settings as well.

politix

 src (10x zuka )

On one side is the party of far-right, election-denying, coup-supporting, anti-democracy, environment-destroying, racist sexist homophobic transphobic gun-worshipping proslavery “Handmaid’s Tale” Ku Klux Klan fascists who are literal Nazis; on the other side is the party of extreme radical leftist, anti-family, anti-border, pro-rioter, criminal-coddling, tax-raising, economy-wrecking, godless un-American Communist baby-killing groomer pedophile sex perverts.

фраза из дуолинго

"Сегодня они изучают французский, а завтра они пожелают жить во Франции!" 

дыбр

 С утреца долбил этот издательский код, чтобы он ошибки рапортовал правильно, а не валял дурака типа "нету файла с книжкой".

Ну пофиксил все наконец, ворнинги наисправлял, послал на ревью. Теперь уже можно книжку редактировать, но это, take a break, it's New Year.

Дождики идут, но не все время, так что успели сходить погулять. Забрались на второй этаж нашего гаража, там уже так ничо так, стены здания, и стены сортира уже построены. Жизнь идет.

Отметили новый год по французскому времени, шампанское разлили, ну и... и оливье, чо. 

Кстати, на дуолинго я запрыгнул на третье место - а потому что, пока программируешь, так есть время. Ну и сам факт, что могу два дела делать сразу, и координировать - уже хорошо. Это, наверно, таблетки, креатин. А фильм, 10%, смотрю потихонечку. Входя в детали. Comment Chier Quand On Est Amoureux - книга такая, на амазоне рекламируется.



Созвонились со Степой, уже после французского нового года. Поздравили друг друга. Ну, у них-то уже второй час ночи.

Так, ну и все, наверно. Почитал инструкцию к цепной пиле; залил в нее масло; провел инструктаж жене на эту тему. Еще буквально нужно ей книгу позачитывать.

Вообще странное ощущение, когда вроде и есть чем заняться, и лень. Ну, книжку потом почитаю еще, Васильчикову.