Introductions on Topology
http://pi.math.cornell.edu/~matsumura/math4530/IntroToTopology.pdf
https://www.math.colostate.edu/~renzo/teaching/Topology10/Notes.pdf
https://math.bme.hu/~kalex/Teaching/Spring10/Topology/TopNotes_Spring10.pdf
This is not directly related, but it might be considered useful.
http://pi.math.cornell.edu/~matsumura/math4530/IntroToTopology.pdf
https://www.math.colostate.edu/~renzo/teaching/Topology10/Notes.pdf
https://math.bme.hu/~kalex/Teaching/Spring10/Topology/TopNotes_Spring10.pdf
This is not directly related, but it might be considered useful.
Proofs are programs: 19th century logic and 21st century computing
"For my money, Gentzen’s natural deduction and Church’s lambda calculus are on a par with Einstein’s relativity and Dirac’s quantum physics for elegance and insight. And the maths are a lot simpler." - Wadler, 2000.
https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
"For my money, Gentzen’s natural deduction and Church’s lambda calculus are on a par with Einstein’s relativity and Dirac’s quantum physics for elegance and insight. And the maths are a lot simpler." - Wadler, 2000.
https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
A Monoid Is a Category With Just One Object. So What's the Problem?
https://k-bx.github.io/articles/boring-monoid-category.html
An introduction on category theory as well as on proof assistants.
[Thanks to Brett]
https://k-bx.github.io/articles/boring-monoid-category.html
An introduction on category theory as well as on proof assistants.
[Thanks to Brett]
What is a Natural transformation?
https://www.math3ma.com/blog/what-is-a-natural-transformation
https://www.math3ma.com/blog/what-is-a-natural-transformation
Math3Ma
What is a Natural Transformation? Definition and Examples
I hope you have enjoyed our little series on basic category theory. (I know I have!) This week we'll close out by chatting about natural transformations which are, in short, a nice way of moving from one functor to another. If you're new to this mini-series…
Computational higher type theory
https://arxiv.org/abs/1604.08873
https://arxiv.org/abs/1604.08873
The elements of an inductive type
http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/
http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/
Approximate Normalization for Gradual Dependent Types
https://arxiv.org/abs/1906.06469
[OP is Brett, fixed format]
https://arxiv.org/abs/1906.06469
[OP is Brett, fixed format]
Combinatorial Species and Labelled Structures
http://ozark.hendrix.edu/~yorgey/pub/thesis.pdf
http://ozark.hendrix.edu/~yorgey/pub/thesis.pdf
Linear logic for constructive mathematics
https://arxiv.org/abs/1805.07518
https://arxiv.org/abs/1805.07518
arXiv.org
Affine logic for constructive mathematics
We show that numerous distinctive concepts of constructive mathematics arise automatically from an "antithesis" translation of affine logic into intuitionistic logic via a Chu/Dialectica...
nevermind, posted this before
Cartesian Cubical computational type theory
https://hott-uf.github.io/2018/slides/FavoniaHoTTUF2018.pdf
https://hott-uf.github.io/2018/slides/FavoniaHoTTUF2018.pdf
Univalent foundations
https://www.ias.edu/ideas/2014/voevodsky-foundations-video
https://www.ias.edu/ideas/2014/voevodsky-foundations-video
Institute for Advanced Study
Univalent Foundations: New Foundations of Mathematics
In Voevodsky’s experience, the work of a mathematician is 5% creative insight and 95% self-verification. Moreover, the more original the insight, the more one has to pay for it later in self-verification work. The Univalent Foundations project, started at…
Seven sketches in composability
http://math.mit.edu/~dspivak/teaching/sp18/
http://math.mit.edu/~dspivak/teaching/sp18/
math.mit.edu
Seven Sketches in Compositionality
Category theory is a relatively new branch of mathematics that has
transformed much of pure math research. The technical advance is that
category theory provides a framework in which to organize formal systems
and by which to translate between them, allowing…
transformed much of pure math research. The technical advance is that
category theory provides a framework in which to organize formal systems
and by which to translate between them, allowing…
The Catsters' category theory videos
https://www.youtube.com/playlist?list=PLlGXNwjYhXYxKVa67r0pKuYufECy713bv
https://www.youtube.com/playlist?list=PLlGXNwjYhXYxKVa67r0pKuYufECy713bv
YouTube
The Catsters' Category Theory Videos - YouTube
Type-driven development in Idris
https://www.manning.com/books/type-driven-development-with-idris
A practical programming language with dependent types.
https://www.manning.com/books/type-driven-development-with-idris
A practical programming language with dependent types.
Manning Publications
Type-Driven Development with Idris - Edwin Brady
Write safer, faster code! Learn type-driven development with Idris, from the language's creator.
Functional design and architecture
https://graninas.com/functional-design-and-architecture-book/
https://graninas.com/functional-design-and-architecture-book/
Inside a Black Hole
Functional Design and Architecture: Examples in Haskell (Manning Publications)
FDaA: EH is an advanced book about building real programs with an engineering approach in statically typed functional languages. Buy here: Functional Design and Architecture: Example in Haskell It …
Sets, Logic, Computation
http://builds.openlogicproject.org/courses/phil379/phil379-screen.pdf
http://builds.openlogicproject.org/courses/phil379/phil379-screen.pdf
The Rascal Metaprogramming language
https://www.rascal-mpl.org/
https://www.rascal-mpl.org/
Agda base
https://github.com/pcapriotti/agda-base/tree/master/src
A Agda library with HoTT support, not requiring cubical anything, which is simple and runs on any modern agda version, unlike HoTT-Agda.
https://github.com/pcapriotti/agda-base/tree/master/src
A Agda library with HoTT support, not requiring cubical anything, which is simple and runs on any modern agda version, unlike HoTT-Agda.
GitHub
pcapriotti/agda-base
Base library for HoTT in Agda. Contribute to pcapriotti/agda-base development by creating an account on GitHub.