Algebraic Topology (Lecture Notes)
https://www.mit.edu/~sanathd/main.pdf
https://www.mit.edu/~sanathd/main.pdf
An Introduction to Higher Categorical Algebra
https://arxiv.org/abs/1907.02904
https://arxiv.org/abs/1907.02904
Higher Topos Theory
https://arxiv.org/abs/math/0608040v4
https://arxiv.org/abs/math/0608040v4
Higher Algebra
https://arxiv.org/abs/math/0608040v4
https://arxiv.org/abs/math/0608040v4
Towards Observational Type Theory
http://strictlypositive.org/ott.pdf
http://strictlypositive.org/ott.pdf
Topology without Tears
http://www.topologywithouttears.net/topbook.pdf
http://www.topologywithouttears.net/topbook.pdf
Exhaustible Sets in Higher-type Computation
https://www.researchgate.net/publication/220346819_Exhaustible_Sets_in_Higher-type_Computation
(free to download, no request required)
https://www.researchgate.net/publication/220346819_Exhaustible_Sets_in_Higher-type_Computation
(free to download, no request required)
ResearchGate
(PDF) Exhaustible Sets in Higher-type Computation.
PDF | We say that a set is exhaustible if it admits algorithmic universal quantification for continuous predicates in finite time, and searchable if... | Find, read and cite all the research you need on ResearchGate
Infinite Sets that admit fast exhaustive search
https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.3062
https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.3062
citeseerx.ist.psu.edu
CiteSeerX — Infinite sets that admit fast exhaustive search
CiteSeerX - Document Details (Isaac Councill, Lee Giles, Pradeep Teregowda): Abstract. Perhaps surprisingly, there are infinite sets that admit mechanical exhaustive search in finite time. An old example is the Cantor space of infinite sequences of binary…
The Strict ω-Groupoid Interpretation of Type Theory
https://mawarren.net/papers/crmp1295.pdf
https://mawarren.net/papers/crmp1295.pdf
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