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.
Structuralism, Invariance, and Univalence
https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf
Kind of an introduction to HoTT.
[Thanks to Brett]
https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf
Kind of an introduction to HoTT.
[Thanks to Brett]
Unintentional type theory
http://www.cs.cmu.edu/~cangiuli/sigbovik/unintentional.pdf
(for those people who haven't noticed it so far, this is a joke)
http://www.cs.cmu.edu/~cangiuli/sigbovik/unintentional.pdf
(for those people who haven't noticed it so far, this is a joke)
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
https://arxiv.org/abs/1301.3443
https://arxiv.org/abs/1301.3443
Foundations of Software Science and Computation Structures
https://link.springer.com/book/10.1007%2F978-3-319-89366-2
https://link.springer.com/book/10.1007%2F978-3-319-89366-2
Springer
Foundations of Software Science and Computation Structures | SpringerLink
This book is Open Access under a CC BY licence.
To be or not to be constructive, that is not the question
https://arxiv.org/abs/1704.00462
https://arxiv.org/abs/1704.00462
arXiv.org
To be or not to be constructive, that is not the question
In the early twentieth century, L.E.J. Brouwer pioneered a new philosophy of
mathematics, called intuitionism. Intuitionism was revolutionary in many
respects but stands out -mathematically...
mathematics, called intuitionism. Intuitionism was revolutionary in many
respects but stands out -mathematically...
A synthetic theory of infinity-categories in homotopy type theory
http://www.math.jhu.edu/~eriehl/octoberfest.pdf
http://www.math.jhu.edu/~eriehl/octoberfest.pdf
Applied Category Theory conference
https://www.youtube.com/user/wires0/live
Note that this is a livestream.
https://www.youtube.com/user/wires0/live
Note that this is a livestream.
YouTube
Jelle Herold
... and its programme, thanks to Daniele.
Forwarded from Daniele
ACT 2019 programme.pdf
304.2 KB
Guix: A most advanced operating system
https://ambrevar.xyz/guix-advance/
The superior, purely functional package manager.
https://ambrevar.xyz/guix-advance/
The superior, purely functional package manager.
NixOS
https://nixos.org/nixos/
As well purely functional, with its own advantages and disadvantages compared to Guix.
https://nixos.org/nixos/
As well purely functional, with its own advantages and disadvantages compared to Guix.
Dedukti
https://deducteam.github.io/index.html
Dedukti is a logical framework based on the λΠ-calculus modulo in which many theories and logics can be expressed.
https://deducteam.github.io/index.html
Dedukti is a logical framework based on the λΠ-calculus modulo in which many theories and logics can be expressed.
The Lean Theorem Prover
https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/
https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/
Homotopy Type Theory
The Lean Theorem Prover
Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development fo…
Thanks for 100 members!
As I got a shoutout by @GNUPropaganda, I'd want everyone interested in free software to join there, as well @GNUGroup (you need an invite for that one though). Also, to engage in in-depth discussion about type theory and formal verification, join @deepspec!