dan/HITs-Examples
1
0
Fork 0
mirror of https://github.com/nmvdw/HITs-Examples synced 2026-05-25 17:20:25 +02:00
Code Issues Releases Wiki Activity

Commit Graph

  • c366c8f59b Use the namespace FSets card dan 2018-02-10 20:06:37 +01:00
  • 7c14d36f7d Universe of finite cardinals dan 2018-02-09 18:19:14 +01:00
  • c05d356bac Show that a type is Kfinite if its truncation is Kfinite hottclasses dan 2018-01-25 18:08:47 +01:00
  • 4c7a2ecd1b Add the Pauli id law example dan 2017-12-15 13:41:41 +01:00
  • 8ce4cb760a Update the code to match the latest HoTT dan 2017-11-06 15:25:56 +01:00
  • 55136b24e7 Add a comment regarding the use of Topped dan 2017-11-01 18:40:23 +01:00
  • 4fafbf175e Port the codebase to HottClasses dan 2017-11-01 17:47:41 +01:00
  • c6f756a856 Clarified proof of notIn_ext_union_singleton master Niels van der Weide 2017-10-11 17:45:37 +02:00
  • 91899aef6f union idem used for comprehension Niels van der Weide 2017-10-11 17:11:07 +02:00
  • 0f44ee009b Merge branch 'cleanupish' dan 2017-10-11 13:50:17 +02:00
  • f9aee7ef23 HTML building instructions cleanupish dan 2017-10-11 13:42:20 +02:00
  • 604a2659df A bit of cleanup dan 2017-10-11 13:40:49 +02:00
  • 91a059bcdf Improved README Niels van der Weide 2017-10-11 13:37:48 +02:00
  • 4d070ba26d Some quickfixes dan 2017-10-11 12:56:29 +02:00
  • 1aebb3879e Add the CPP paper overview dan 2017-10-11 10:03:28 +02:00
  • d0f743432c Added bounded quantification for lists Niels van der Weide 2017-10-09 23:41:29 +02:00
  • 97002d119b Added refinement Niels van der Weide 2017-10-09 14:00:16 +02:00
  • 01d0908b8a Added member as exist Niels van der Weide 2017-10-09 13:59:59 +02:00
  • 16e0e6f63d Shortenings in b_finite Niels van der Weide 2017-10-04 23:00:14 +02:00
  • c7df8ae8aa If Bfin has union, then decidable paths Niels van der Weide 2017-10-04 15:01:15 +02:00
  • b638c2592d Simplified Kfin=>Bfin Niels van der Weide 2017-10-03 21:50:43 +02:00
  • 764b0147fe Simplified proof of Bfin => Kfin Niels van der Weide 2017-10-03 21:34:23 +02:00
  • fffdb87b4f Simplified no union for Bishops Niels van der Weide 2017-10-03 14:45:00 +02:00
  • c9e6b35949 Added proof that Bfin => set if all singletons are Bfin Niels van der Weide 2017-10-03 12:34:12 +02:00
  • 9a2a81047b Added some lemmata from paper Niels van der Weide 2017-10-02 17:23:03 +02:00
  • 81f5dbcbd5 Additions to set interface Niels van der Weide 2017-09-29 23:31:06 +02:00
  • 00d4943e2d Merge branch 'master' of https://github.com/nmvdw/HITs-Examples Niels van der Weide 2017-09-29 15:26:58 +02:00
  • 38a64bae76 Simplification in proof of append_union Niels van der Weide 2017-09-28 14:45:54 +02:00
  • 38d0b07ef8 Add some properties from the Elephant dan 2017-09-26 14:06:42 +02:00
  • 72a44c71f9 Cleaning in length Niels van der Weide 2017-09-26 13:06:47 +02:00
  • d7a95697fb Some cleaning in list representation Niels van der Weide 2017-09-26 11:56:58 +02:00
  • 0e9fcbc588 Show that Kf (A + B) -> Kf A dan 2017-09-25 13:44:11 +02:00
  • 35f0452a6a Merge branch 'master' of https://github.com/nmvdw/HITs-Examples Niels van der Weide 2017-09-25 13:04:28 +02:00
  • 7281bfc0bf Added S1 has merely decidable equality Niels van der Weide 2017-09-25 13:03:51 +02:00
  • 73fbe8716a Minor cleanup dan 2017-09-25 12:38:03 +02:00
  • 617451da28 Some closure properties for K-finite objects dan 2017-09-24 23:35:45 +02:00
  • 74eaddee2a minor cleanup dan 2017-09-24 18:56:32 +02:00
  • bd91e18ad6 Fix the globality of an instance and simplify bfin_union a bit dan 2017-09-24 18:34:35 +02:00
  • 206bf9edb6 Cleanup the Pauli group example dan 2017-09-24 17:55:19 +02:00
  • d5e08c43bf Added example of Pauli matrices Niels van der Weide 2017-09-22 20:30:25 +02:00
  • a0dbf4bfad Added decidable quantification Niels van der Weide 2017-09-22 19:42:25 +02:00
  • 2eace536c2 Added quantifiers and their decidability. Niels van der Weide 2017-09-22 17:24:53 +02:00
  • 6a21e83b6c Added length of disjoint sum Niels van der Weide 2017-09-22 16:16:12 +02:00
  • 344117a9b3 Length of product Niels van der Weide 2017-09-21 23:33:20 +02:00
  • 7b5bc340ff Some cleaning Niels van der Weide 2017-09-21 18:13:34 +02:00
  • f4253520c8 Added proof of inclusion/exclusion. Niels van der Weide 2017-09-21 18:09:40 +02:00
  • bbe8f665df Weakened assumption of singleton_isIn_d Niels van der Weide 2017-09-21 14:24:27 +02:00
  • 7f9b2b7032 Length also uses merely decidable equality Niels van der Weide 2017-09-21 14:17:48 +02:00
  • 39e2ce1c05 Uses merely decidable equality, added length. Niels van der Weide 2017-09-21 14:12:51 +02:00
  • 0def5869cd Quickfix dan 2017-09-19 18:22:22 +02:00
  • 8e143c5285 Cleaning in iso Niels van der Weide 2017-09-19 17:22:15 +02:00
  • 2cd3beec43 commutative -> commutativity dan 2017-09-17 19:45:32 +02:00
  • c2babb9422 Simplify the bfin_union proof. dan 2017-09-17 19:24:17 +02:00
  • 28a9e95fea Minor improvements Niels 2017-09-13 14:22:54 +02:00
  • 7994032d81 Added independence proofs Niels 2017-09-13 14:04:58 +02:00
  • f8234375c8 Decidable emptiness improved Niels 2017-09-07 17:22:14 +02:00
  • 7a636c7035 Moved length Niels 2017-09-07 15:47:46 +02:00
  • bb4add6510 Lists to project Niels 2017-09-07 15:45:43 +02:00
  • 6c86d0c524 Fixes Niels 2017-09-07 15:44:22 +02:00
  • 4ae639ace3 Removed some useless files Niels 2017-09-07 15:24:38 +02:00
  • 474c9324ca A negligible change in the structure Niels 2017-09-07 15:19:48 +02:00
  • 4ab70ae1fe Further cleaning Niels 2017-09-01 17:08:00 +02:00
  • dfd590724b Simplified independence proof Niels 2017-09-01 16:56:49 +02:00
  • 40e1f45cfa Shortened T.v Niels 2017-09-01 16:29:48 +02:00
  • e8560a0c07 tfw importin the middle of the file dan 2017-08-24 18:52:43 +02:00
  • b17a726608 A simple proof that Bfin implies Kfin dan 2017-08-24 18:41:31 +02:00
  • c7aa3d581f Update the README dan 2017-08-24 16:53:58 +02:00
  • c23ea61353 Move aux lemmas into the plumbing file dan 2017-08-24 16:50:11 +02:00
  • 5afb85b000 Merge branch 'ezsplit' dan 2017-08-24 16:45:37 +02:00
  • 5e4091409d The underlying type need not be an hset for the splitting lemma ezsplit dan 2017-08-24 16:36:59 +02:00
  • 431e1b1048 No singletons if the underlying type isnt a set Niels 2017-08-24 14:37:38 +02:00
  • eef533e345 Get rid of cow induction for the proof of closedUnion Bfin Dan Frumin 2017-08-24 11:35:58 +02:00
  • e1a8220ba0 A simpler split fn for B-finite subobjects. Dan Frumin 2017-08-23 22:23:28 +02:00
  • 8a1405a1d8 A cons-based induction principle for FSets dan 2017-08-19 18:55:47 +02:00
  • 39d888951e Merge branch 'master' of https://github.com/nmvdw/HITs-Examples Niels 2017-08-18 11:34:41 +02:00
  • 41b952e0d0 Added alternative definition of k-finite via subobjects Niels 2017-08-18 11:34:04 +02:00
  • 29f3f31cec Improved lattice hints Niels 2017-08-18 11:18:37 +02:00
  • da60017367 Interval is K-finite dan 2017-08-17 22:43:22 +02:00
  • 8ff54def39 Removed View_rec2 Niels 2017-08-17 17:18:57 +02:00
  • ae60ac0146 LEM <~> all K-finite hsets are projective dan 2017-08-16 17:37:12 +02:00
  • 56d6207d07 Circle is Kuratowski-finite dan 2017-08-16 17:13:08 +02:00
  • 809382ba13 Every Bishop-finite set is Kuratowski-finite dan 2017-08-16 17:01:25 +02:00
  • 99dfd73b5a K-finite objects are closed under surjections dan 2017-08-16 16:07:51 +02:00
  • 57a4535f87 B-fin => K-fin if the underlying type has decidable paths dan 2017-08-16 15:59:36 +02:00
  • 920fdd91ab further simplifications Niels 2017-08-15 22:26:26 +02:00
  • e1bc900abc Further simplifications in interface Niels 2017-08-15 22:05:31 +02:00
  • e29e978218 Improved interface.v Niels 2017-08-15 20:08:16 +02:00
  • 06701dcdf8 Simplified proof of extensionalty and proofs in interface.v Niels 2017-08-14 21:38:50 +02:00
  • b274fcddfc Simplified proof of extensionality Niels 2017-08-14 16:39:20 +02:00
  • 0f6e98a377 Strengthened mere choice Niels 2017-08-14 12:43:15 +02:00
  • bf0b9f8771 Added simplified proof of extensionality Niels 2017-08-11 14:17:47 +02:00
  • 5766024f95 path_ishprop now in extensionality Niels 2017-08-11 13:15:31 +02:00
  • 89808c7297 Added proof: Bishop finite => Kuratowski finite Niels 2017-08-10 17:33:56 +02:00
  • 33808928db Clean up trailing whitespaces and an unused definition. dan 2017-08-09 18:05:58 +02:00
  • 31e08af1d1 Prove that the quotient of an implementation is isomorphic to FSet dan 2017-08-09 17:59:11 +02:00
  • bd2ca9a0aa Added separation as operation Niels 2017-08-09 17:03:51 +02:00
  • f08918b60c Move the B-finiteness proofs and simplify them a bit dan 2017-08-09 16:01:35 +02:00
  • cb0af9a36a Added min function with proof of its specification Niels 2017-08-09 15:11:14 +02:00
  • 5233fc6de9 Added proof that the finite sets in HoTTlibrary have no intersection and union Niels 2017-08-09 12:07:43 +02:00
  • c358ef1659 Added notation in Sub.v Niels 2017-08-08 19:56:39 +02:00