You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
* Introduction to categorical logic, classifying toposes and the bridge technique - Olivia Caramello [(videos with toc)](https://sites.google.com/site/logiquecategorique/autres-seminaires/ihes/ihestopos/cours/20151124-caramello)
* Introduction to categorical logic, classifying toposes and the bridge technique - Olivia Caramello [(videos)](https://www.youtube.com/@IhesFr/search?query=categorical%20logic%2C%20classifying%20toposes)
*[Toposes in Como 2018](http://tcsc.lakecomoschool.org/) conference: [(video playlist)](https://www.youtube.com/watch?v=85hAGaFCsD8&index=2&list=PLh_3Q6ZRqWs0LBptMGClJ8OArR0fBT6Pp), [(slides from talks)](http://tcsc.lakecomoschool.org/program/); There are introductory lectures [Some glances at topos theory - Francis Borceux](https://www.youtube.com/watch?v=s_fN9euuVAY&list=PLh_3Q6ZRqWs0LBptMGClJ8OArR0fBT6Pp&index=10)
58
-
*[Topos à l’IHES 2015](https://indico.math.cnrs.fr/event/747/) conference: [(video playlist)](https://www.youtube.com/playlist?list=PLx5f8IelFRgFjhhrWWl96sRSClcG5YIx6), includes introductory: [A crash course in topos theory: the big picture - André Joyal](https://sites.google.com/site/logiquecategorique/autres-seminaires/ihes/ihestopos/cours/joyal)
57
+
*[Topos à l’IHES 2015](https://indico.math.cnrs.fr/event/747/) conference: [(video playlist)](https://www.youtube.com/playlist?list=PLx5f8IelFRgFjhhrWWl96sRSClcG5YIx6), includes introductory: A crash course in topos theory: the big picture by André Joyal
59
58
* Higher Topos Theory - Jacob Lurie [(arXiv:math/0608040)](https://arxiv.org/abs/math/0608040)
60
59
*[Basics in category and topos theory - David Janin](https://www.labri.fr/perso/janin/Enseignement/EDMI/full.html)
61
60
* An Introduction to Topos Theory - Ryszard Paweł Kostecki [(lecture notes)](https://www.fuw.edu.pl/~kostecki/ittt.pdf)
@@ -79,7 +78,6 @@
79
78
80
79
* Network Models - John C. Baez, John Foley, Joseph Moeller, Blake S. Pollard [(arXiv)](https://arxiv.org/abs/1711.00037)
81
80
* A coalgebraic model of graphs - Christian Jäkel [(arXiv)](https://arxiv.org/abs/1508.02169)
82
-
* Coalgebraic Modelling Applications in Automata Theory and Modal Logic - Helle Hvid Hansen [(pdf)](https://www.cs.vu.nl/en/Images/HH_Hansen_14-05-2009_tcm210-259639.pdf)
83
81
* Compositional game theory reading list - Jules Hedges [(blog post)](https://julesh.com/2017/11/09/compositional-game-theory-reading-list/)
84
82
* A mathematical theory of resources - Bob Coecke, Tobias Fritz, Robert W. Spekkens [arXiv:1409.5531](https://arxiv.org/abs/1409.5531) (application of CT for resource management)
85
83
* The Mathematical Specification of the [Statebox](https://statebox.org/) Language - Statebox Team: Fabrizio Genovese, Jelle Herold [arXiv:1906.07629](https://arxiv.org/abs/1906.07629) (programming language based on CT and petri nets)
@@ -135,66 +133,6 @@
135
133
*[Fancy Algebra - Part I: Adjoint Functors](http://www.math.miami.edu/~armstrong/FA/FA_part1.pdf)
136
134
*[varkor/quiver](https://github.com/varkor/quiver)Tooll for drawing commuate diagrams
137
135
138
-
## Publications
139
-
140
-
This is very opinionated selection of authors that publish interesting papers about `Category Theory`, `Type Theory` and other branches of `Logic`, `Proof Theory`.
141
-
142
-
* Haskell Wiki [Functional_pearls](https://wiki.haskell.org/Research_papers/Functional_pearls), [Monads and arrows](https://wiki.haskell.org/Research_papers/Monads_and_arrows)
*[Johan Jeuring](https://dblp.uni-trier.de/pers/hd/j/Jeuring:Johan), [Utrecht University page](http://www.staff.science.uu.nl/~jeuri101/homepage/Publications/index.html)
*[Ross Street](http://web.science.mq.edu.au/~street/Publications.htm), [wikipedia has links to publications](https://en.wikipedia.org/wiki/Ross_Street), [arXiv](https://arxiv.org/search/math?searchtype=author&query=Street%2C+R)
193
-
*[Wouter Swierstra](https://dblp.org/pers/hd/s/Swierstra:Wouter), [Utrecht University page](http://www.staff.science.uu.nl/~swier004/publications/)
* DeepSpec Summer School [(2018 videos)](https://deepspec.org/event/dsss18/videos.html)[(2017 video playlist)](https://www.youtube.com/watch?v=jG61w5pOc2A&list=PLovJjGVqXXf3RgVdCXH96pPwSjFLDhSri), based on Software Foundations [(book)](https://softwarefoundations.cis.upenn.edu/)
@@ -228,13 +166,12 @@ This is very opinionated selection of authors that publish interesting papers ab
228
166
* Homotopy Type Theory - Carnegie Mellon University - Robert Harper [(course)](http://www.cs.cmu.edu/~rwh/courses/hott/) lecture notes, papers
229
167
* Computational Higher Type Theory - Carnegie Mellon University - Robert Harper [(course)](http://www.cs.cmu.edu/~rwh/courses/chtt/)
230
168
* Kerodon (book about categorical homotopy theory) [(book)](https://kerodon.net/kerodon.pdf)[(links)](https://kerodon.net/bibliography)
231
-
* Dependent Types in the Idris Programming Language - OPLSS 2017 - Edwin Brady [(slides, examples)](https://www.idris-lang.org/documentation/workshops/oplss-2017-course-materials/)[(video lectures)](https://www.cs.uoregon.edu/research/summerschool/summer17/topics.php)
169
+
* Dependent Types in the Idris Programming Language - OPLSS 2017 - Edwin Brady [(video lectures)](https://www.cs.uoregon.edu/research/summerschool/summer17/topics.php)
232
170
* Advanced Functional Programming (in Agda) - University of Strathclyde - Conor McBride [(github 2017)](https://github.com/pigworker/CS410-17), [(github 2018)](https://github.com/pigworker/CS410-18)
233
171
*[Dependently typed programming in Agda - EUTypes Summer School 2017 - Conor McBride](https://sites.google.com/view/summerschool2017-eutypes/lectures/dependently-typed-programming-in-agda)[(github)](https://github.com/pigworker/Ohrid-Agda)
234
172
* Introduction to programming with dependent types in Scala (2019) - Dmytro Mitin [(course)](https://stepik.org/course/49181/promo), based on library [ProvingGround](http://siddhartha-gadgil.github.io/ProvingGround/) that was used to [solve Polymath 14 problem](https://polymathprojects.org/2018/01/26/spontaneous-polymath-14-a-success/)[resulting](http://math.iisc.ac.in/~gadgil/presentations/HomogeneousLengths.html#/) in [(paper)](https://arxiv.org/abs/1801.03908)
235
173
* On Voevodsky’s Univalence principle - André Joyal [(video, paper)](https://video.ias.edu/VoevodskyMemConf-2018/0911-AndreJoyal) (mathematical foundations behind HoTT and Univalence principle)
236
174
* Introduction to Homotopy Type Theory (Agda) - EUTypes Summer School 2018 - Fredrik Nordvall Forsberg [(slide, exercises src)](https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/ohrid-school-hott2018/)
237
-
* Introduction to Dependent Type Theory - EUTypes Summer School 2018 - Matthieu Sozeau [(slides)](https://www.irif.fr/~sozeau/teaching/TYPES18.en.html)
238
175
* Workshop: "Types, Homotopy, Type theory, and Verification" 2018 [(video playlist)](https://www.youtube.com/playlist?list=PLul8LCT3AJqQxIaZhaSNCTuLYfIFB1AiI), [(schedule, abstracts, links to videos)](https://www.him.uni-bonn.de/programs/past-programs/past-trimester-programs/types-sets-constructions/workshop-types-homotopy-type-theory-and-verification/schedule/)
239
176
* FAMOUS - Foundations of Mathematics: Univalent foundations and set theory 2016 [(video playlist)](https://www.youtube.com/watch?v=slVcTtwX_Sk&list=PLQRKUSOIMEh1Arz0-WBgD_Pol4S50HATv), [(videos, slides, abstracts)](http://fomus.weebly.com/talks-abstracts--videos.html)
240
177
* HOTTEST - Homotopy Type Theory Electronic Seminar Talks - 2018 - present [(links to videos)](https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html), [(youtube videos)](https://www.youtube.com/user/jdchristensen123/videos)
@@ -244,7 +181,7 @@ This is very opinionated selection of authors that publish interesting papers ab
244
181
245
182
* Introduction to Univalent Foundations of Mathematics with Agda - MGS 2019 - Martín Hötzel Escardó [(lecture notes)](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html)[(github)](https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes)
246
183
* Cubical Agda and its extensions, HoTTEST - Andrea Vezzosi [(code)](https://github.com/Saizan/hottest-talk), [(video)](https://www.youtube.com/watch?v=9RFt1Q2pHE8)
247
-
*Cubical Tutorial. Introduction Course - Maxim Sokhatsky [plan and notes of seminar about HoTT and Cubical TT](https://groupoid.space/course/), [more](https://groupoid.space/)Maxim Sokhatsky [plan and notes of seminar about HoTT and Cubical TT](https://groupoid.space/course/), [more](https://groupoid.space/)
184
+
*[groupoid.space](https://groupoid.space/)
248
185
* Cubical Adventures (in Agda) - University of Strathclyde - Conor McBride [(video)](https://www.youtube.com/watch?v=W5-ulP_JzNc)
249
186
* Investigations into cubical type theory - Hugo Herbelin [(video)](https://www.youtube.com/watch?v=zJdwPa_tkSU&list=PLul8LCT3AJqS9FcdKnV4TfiR48Hqcna1I&index=16)
250
187
* Computational Higher Type Theory - Carnegie Mellon University - Robert Harper [(course)](http://www.cs.cmu.edu/~rwh/courses/chtt/)
@@ -277,7 +214,7 @@ SCALING DOT TO SCALA - SOUNDNESS - Martin Odersky [(blog post)](https://www.scal
277
214
* Univalent categories and the Rezk completion - Benedikt Ahrens, Chris Kapulkin, Michael Shulman [(paper)](https://arxiv.org/abs/1303.0584), [(original repository - now merged into UniMath)](https://github.com/benediktahrens/rezk_completion)
278
215
* Displayed Categories - Benedikt Ahrens, Peter LeFanu Lumsdaine [(paper)](https://arxiv.org/abs/1705.04296)
279
216
* Bicategories in Univalent Foundations - Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide [(paper)](https://arxiv.org/abs/1903.01152)
280
-
*[HoTT book - Coq](https://github.com/HoTT/HoTT/tree/master/theories/Categories) described in [HoTT book](https://homotopytypetheory.org/coq/)
217
+
*[HoTT book - Coq](https://github.com/HoTT/HoTT/tree/master/theories/Categories) described in [HoTT book](https://homotopytypetheory.org/book/)
281
218
* (Cubical Agda) Univalent Categories A formalization of category theory in Cubical Agda - Frederik Hanghøj Iversen [(paper)](http://publications.lib.chalmers.se/records/fulltext/256404/256404.pdf), [(fredefox/cat)](https://github.com/fredefox/cat)
282
219
* (Agda) Formalisation of Restriction Categories in Agda [jmchapman/restriction-categories](https://github.com/jmchapman/restriction-categories) for [Introduction to restriction categories - Robin Cockett](http://cs.ioc.ee/~tarmo/tsem12/cockett.html)
0 commit comments