formalization

Collaborative formalization.

Setup

• VSCode.
• Agda.
• VSCode Agda plugin.
• VSCode Live Share plugin.
• Agda libraries (instructions on configuration):
  • standard library.
  • HoTT library.
    • Andrew Swan's branch that works with Agda 2.6.1.
  • cubical library.

Resources

• EPIT-2020 workshop:
  • Repo.
  • especially Anders Mortborg's cubical notes.
  • YouTube videos.
• David Jaz Myers' formalization of Mike Shulman's Real Cohesion:
• Felix Cherubino (formerly Wellen) differential cohesion repo.
• Agda.
• Cubical Agda.
• Martin Escardo's one-page intro to Univalent Foundations.

Tips

My ~/.agda/default:

standard-library
hott-core
HoTT-Intro
cubical

My ~/.agda/libraries:

/usr/local/lib/agda/standard-library.agda-lib
$HOME/proj/HoTT-Agda-awswan/hott-core.agda-lib
$HOME/proj/HoTT-Agda-awswan/hott-theorems.agda-lib
$HOME/proj/cubical/cubical.agda-lib
$HOME/proj/HoTT-Agda-Egbert/HoTT-Intro.agda-lib