search

nmvdw / Three-HITs

All higher inductive types can be obtained from three simple HITs.
17 stars 2 forks source link

Colimits in HoTT #1

Closed andrejbauer closed 7 years ago

andrejbauer commented 7 years ago

There is an outstanding PR request for a colimits library in HoTT, see https://github.com/HoTT/HoTT/pull/850. We probably shouldn't duplicate the effort needlessly.

andrejbauer commented 7 years ago

So do these help us in any way?

nmvdw commented 7 years ago

It would shorten the code since the definition of the colimit can then be imported. I don't know yet how to import it.