co-dan/hott-snippets
1
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
snippin
7 commits 1 branch 0 tags 50 KiB
  • Rocq Prover 99%
  • Agda 1%
Find a file
Exact
Dan Frumin 0257a0e921 [Cubes] SquareOver and Torus recursion principle
2018-02-19 15:43:09 +01:00
vK Initial import 2018-02-14 12:37:18 +01:00
.gitignore Initial import 2018-02-14 12:37:18 +01:00
_CoqProject Start formalising the cubical approach to homotopy 2018-02-18 12:33:32 +01:00
Ab.v Initial import 2018-02-14 12:37:18 +01:00
Circ.v Initial import 2018-02-14 12:37:18 +01:00
Cubes.v [Cubes] SquareOver and Torus recursion principle 2018-02-19 15:43:09 +01:00
fibers_transport.v Initial import 2018-02-14 12:37:18 +01:00
Hedberg.v Initial import 2018-02-14 12:37:18 +01:00
HitTactics.v Local copy of HitTactics 2018-02-14 13:40:41 +01:00
Interval.v Initial import 2018-02-14 12:37:18 +01:00
J.v Initial import 2018-02-14 12:37:18 +01:00
K.v Initial import 2018-02-14 12:37:18 +01:00
monoid.v Initial import 2018-02-14 12:37:18 +01:00
Munkres.v Initial import 2018-02-14 12:37:18 +01:00
Paths.v Initial import 2018-02-14 12:37:18 +01:00
README Local copy of HitTactics 2018-02-14 13:40:41 +01:00
Root.v [root.v] Minor cosmetic tweaks 2018-02-18 12:32:52 +01:00
Trunc.v Initial import 2018-02-14 12:37:18 +01:00
yoneda.agda Initial import 2018-02-14 12:37:18 +01:00

README 

Make sure to grab the HoTT library [1] beforehand.

[1]: https://github.com/HoTT/HoTT