Pinned Repositories
agda-stdlib
The Agda standard library
birmingham-theory
The web page for the Birmingham theoretical computer science research group
cubical
EffectfulForcing
Files related to my paper "Continuity of Godel's system T functionals via effectful forcing". MFPS'2013. Electronic Notes in Theoretical Computer Science 01/2013, volume 298, pages 119-141.
HoTT-Agda
Development of homotopy type theory in Agda
hott-notes
15-819 (Homotopy Type Theory) Lecture Notes
HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
HoTTEST-Summer-School
HoTTEST Summer School materials
index
TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
martinescardo's Repositories
martinescardo/HoTTEST-Summer-School
HoTTEST Summer School materials
martinescardo/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
martinescardo/EffectfulForcing
Files related to my paper "Continuity of Godel's system T functionals via effectful forcing". MFPS'2013. Electronic Notes in Theoretical Computer Science 01/2013, volume 298, pages 119-141.
martinescardo/cubical
martinescardo/agda-stdlib
The Agda standard library
martinescardo/birmingham-theory
The web page for the Birmingham theoretical computer science research group
martinescardo/HoTT-Agda
Development of homotopy type theory in Agda
martinescardo/hott-notes
15-819 (Homotopy Type Theory) Lecture Notes
martinescardo/index
martinescardo/mathematics-and-computation
Andrej Bauer's blog "Mathematics and Computation"
martinescardo/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.