lean2/hott/hit
Floris van Doorn 9a17a244c9 move more results and make arguments explicit
More results from the Spectral repository are moved to this library
Also make various type-class arguments of truncatedness and equivalences which were hard to synthesize explicit
2018-09-11 17:06:08 +02:00
..
coeq.hlean various cleanup changes in library 2018-09-10 17:59:11 +02:00
colimit.hlean various cleanup changes in library 2018-09-10 17:59:11 +02:00
default.hlean chore(hott): update default files and some markdown files 2016-07-09 10:20:21 -07:00
groupoid_quotient.hlean various cleanup changes in library 2018-09-10 17:59:11 +02:00
hit.md feat(hit): add construction of propositional truncation to the library 2016-07-09 10:20:21 -07:00
prop_trunc.hlean move more results and make arguments explicit 2018-09-11 17:06:08 +02:00
pushout.hlean various cleanup changes in library 2018-09-10 17:59:11 +02:00
quotient.hlean various cleanup changes in library 2018-09-10 17:59:11 +02:00
refl_quotient.hlean refactor(hott): rename apdo to apd 2016-04-11 09:45:59 -07:00
set_quotient.hlean move more results and make arguments explicit 2018-09-11 17:06:08 +02:00
trunc.hlean move more results and make arguments explicit 2018-09-11 17:06:08 +02:00
two_quotient.hlean various cleanup changes in library 2018-09-10 17:59:11 +02:00