search

nmvdw / Three-HITs

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

Lemma 13 #4

Closed nmvdw closed 7 years ago

nmvdw commented 7 years ago

Lemma lem:pathext is not proven correctly. I am not sure whether the current formulation is correct.

nmvdw commented 7 years ago

Fixed. It is now split in two lemmas. Also, now the usage of function extensionality becomes clear.