584f9e3f49
This commit also removes many (now unnecessary) folds from the HoTT library. See issue #692 We still have to implement support for recursive definitions based on brec_on that recurse over inductive families. |
||
|---|---|---|
| .. | ||
| circle.hlean | ||
| coeq.hlean | ||
| colimit.hlean | ||
| cylinder.hlean | ||
| hit.md | ||
| interval.hlean | ||
| pushout.hlean | ||
| quotient.hlean | ||
| red_susp.hlean | ||
| refl_quotient.hlean | ||
| set_quotient.hlean | ||
| sphere.hlean | ||
| susp.hlean | ||
| torus.hlean | ||
| trunc.hlean | ||
| two_quotient.hlean | ||