Globular
http://globular.science/
http://globular.science/
Category Theory in Context
http://www.math.jhu.edu/~eriehl/context.pdf
http://www.math.jhu.edu/~eriehl/context.pdf
Category Theory for Programmers
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Bartosz Milewski's Programming Cafe
Category Theory for Programmers: The Preface
Table of Contents Part One Category: The Essence of Composition Types and Functions Categories Great and Small Kleisli Categories Products and Coproducts Simple Algebraic Data Types Functors Functo…
General Remark
This channel is intended as a place to dump resources about a somewhat general topic. It's probably already reached a point where no person would be able to actually understand all the topics once mentioned here, but that was never the point anyway. It was more intended as a place where readers could expand their knowledge regarding things they are somewhat experienced with, or learn new things (see the introductory material in one of the first messages, that will be reworked soon as well). Of course, many papers etc. posted here are still worth a look, no matter your experience. But don't expect to understand more than a very small amount of what actually gets posted, neither do I.
Considering this, content is always welcome, if you would like to share something you made or found, just DM me. The topics have become a bit more broad, anything regarding (somewhat) pure mathematics and sometimes, theoretical CS, should be welcome.
TL;DR: Don't expect to understand more than a tiny fraction of the posts, one can't be an expert on everything.
This channel is intended as a place to dump resources about a somewhat general topic. It's probably already reached a point where no person would be able to actually understand all the topics once mentioned here, but that was never the point anyway. It was more intended as a place where readers could expand their knowledge regarding things they are somewhat experienced with, or learn new things (see the introductory material in one of the first messages, that will be reworked soon as well). Of course, many papers etc. posted here are still worth a look, no matter your experience. But don't expect to understand more than a very small amount of what actually gets posted, neither do I.
Considering this, content is always welcome, if you would like to share something you made or found, just DM me. The topics have become a bit more broad, anything regarding (somewhat) pure mathematics and sometimes, theoretical CS, should be welcome.
TL;DR: Don't expect to understand more than a tiny fraction of the posts, one can't be an expert on everything.
General Topology
https://www.maths.ed.ac.uk/~tl/topology/topology_notes.pdf
https://www.maths.ed.ac.uk/~tl/topology/topology_notes.pdf
A slow-paced introduction to reflection in Agda
https://github.com/alhassy/gentle-intro-to-reflection
[Thanks to ptrcmd]
https://github.com/alhassy/gentle-intro-to-reflection
[Thanks to ptrcmd]
GitHub
GitHub - alhassy/gentle-intro-to-reflection: A slow-paced introduction to reflection in Agda. ---Tactics!
A slow-paced introduction to reflection in Agda. ---Tactics! - GitHub - alhassy/gentle-intro-to-reflection: A slow-paced introduction to reflection in Agda. ---Tactics!
Compiling with Classical Connectives
https://arxiv.org/abs/1907.13227
https://arxiv.org/abs/1907.13227
A simple model for quotient times
https://link.springer.com/chapter/10.1007/BFb0014055
[Thanks to T. Heindel]
https://link.springer.com/chapter/10.1007/BFb0014055
[Thanks to T. Heindel]
SpringerLink
A simple model for quotient types
We give an interpretation of quotient types within in a dependent type theory with an impredicative universe of propositions (Calculus of Constructions). In the model, type dependency arises only at...
Constructive reverse mathematics
https://arxiv.org/pdf/1804.05495.pdf
https://arxiv.org/pdf/1804.05495.pdf
Formal Reasoning About Programs
http://adam.chlipala.net/frap/frap_book.pdf
http://adam.chlipala.net/frap/frap_book.pdf
Persistent Homology - a Survey
https://www.maths.ed.ac.uk/~v1ranick/papers/edelhare.pdf
[Thanks to kl mw]
https://www.maths.ed.ac.uk/~v1ranick/papers/edelhare.pdf
[Thanks to kl mw]
Normal Derivability and First-Order Arithmetic
https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093883058
https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093883058
projecteuclid.org
Tosi : Normal derivability and first-order arithmetic.
Project Euclid - mathematics and statistics online
How to Write Seemingly Unhygienic and Referentially Opaque Macros with Syntax-rules
http://okmij.org/ftp/Scheme/Dirty-Macros.pdf
A bit more programming-related, but still close enough to matter :)
[Thanks to Freddie]
http://okmij.org/ftp/Scheme/Dirty-Macros.pdf
A bit more programming-related, but still close enough to matter :)
[Thanks to Freddie]
Fast and Loose Reasoning is Morally Correct
https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf
https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf
Understanding and Using Spector’s Bar Recursive Interpretation of Classical Analysis
https://www.eecs.qmul.ac.uk/~pbo/papers/paper011.pdf
https://www.eecs.qmul.ac.uk/~pbo/papers/paper011.pdf
Elements of Finite Model Theory
https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf
https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf
Model theory Notes
https://math.berkeley.edu/~scanlon/225af13lectures/ModelTheoryNotes.pdf
https://math.berkeley.edu/~scanlon/225af13lectures/ModelTheoryNotes.pdf