What are the existing formalizations of category theory in proof assistants?
I'm primarily interested in public-domain code implementing category theory in a proof assistant (Coq, Agda, Isabelle/H...

We show that Voevodsky's univalence axiom for intensional type theory is
valid in categories of simplicial presheaves on elegant Reedy categories. In
addition to diagrams on inverse categories, as...

Mike Shulman announces full proof of the Awodey conjecture https://t.co/9GZZdBDmDU yesterday at "Geometry in Modal HoTT" https://t.co/n9GMFZa8ab See slides 5-10 here: https://t.co/ZWuJHHM3rd

We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be
presented by a Quillen model category that interprets homotopy type theory with
strict univalent universes. Thus, homotopy...

Видимо, более наглядно, чем Милевский, никто не описывал.
https://bartoszmilewski.com/2017/04/17/kan-extensions/
https://bartoszmilewski.com/2018/01/23/pointwise-kan-extensions/
Нутам, частично не удовлетворяет "хацкель не предлагать" ;-)
На первый взгляд, очень так —
https://en.wikipedia.org/wiki/Kan_extension
Но имхо, надо ещё понять (ко)концы, это важная, очень важная тема.
Ну это всё (пределы-сопряжённости-(ко)концы-расширенияКана) между собой очень хорошо так завязано.
Ну и имхо, на каком-то этапе, таки желательно почитать Маклейна, он хорош, хоть и примеры у него такие вот ;-)
#link