9 Commits

Author	SHA1	Message	Date
Dan Frumin	4fafbf175e	Port the codebase to HottClasses ... Initial work + use the latest version of HoTT	2017-11-01 17:47:41 +01:00
Niels van der Weide	91899aef6f	union idem used for comprehension	2017-10-11 17:11:07 +02:00
Niels van der Weide	d7a95697fb	Some cleaning in list representation	2017-09-26 11:56:58 +02:00
Dan Frumin	617451da28	Some closure properties for K-finite objects	2017-09-24 23:35:45 +02:00
Niels van der Weide	6a21e83b6c	Added length of disjoint sum	2017-09-22 16:16:12 +02:00
Niels van der Weide	f4253520c8	Added proof of inclusion/exclusion.	2017-09-21 18:09:40 +02:00
Niels van der Weide	39e2ce1c05	Uses merely decidable equality, added length.	2017-09-21 14:12:51 +02:00
Niels	f8234375c8	Decidable emptiness improved	2017-09-07 17:22:14 +02:00
Niels	474c9324ca	A negligible change in the structure	2017-09-07 15:19:48 +02:00