Commit graph

Select branches

Hide pull requests

dev

0.0.1

1.0.0

1.0.1

1.1.0

1.2.0

1.3.0

1.4.0

1.4.1

1.5.0

1.6.0

Mono Color

• aa52bc8f07 Move lemmas about equivalences to that module Frederik Hanghøj Iversen 2018-04-23 17:04:27 +0200
• 313c7593d1 Distinguish isomorphism of categories and of types Frederik Hanghøj Iversen 2018-04-19 12:20:44 +0200
• 92fb53098a Implemented ntypeCumulative Andrea Vezzosi 2018-04-15 13:49:46 +0200
• 98b90f2370 Clean-up names a bit Frederik Hanghøj Iversen 2018-04-13 15:35:56 +0200
• b7c0fe64cf Remove work-in-progress for functors Frederik Hanghøj Iversen 2018-04-13 15:30:20 +0200
• 6b7d66b7fc Formatting Frederik Hanghøj Iversen 2018-04-13 15:26:46 +0200
• 7b45b5cdc3 Show that objects are groupoids Frederik Hanghøj Iversen 2018-04-13 15:22:13 +0200
• 5afa835787 Category.Product complete step2 Andrea Vezzosi 2018-04-13 14:35:54 +0200
• 6023a49da6 Category.Product: get rid of the yellow Andrea Vezzosi 2018-04-13 14:35:10 +0200
• c1f58b1a4f univalence in product-category step1 Andrea Vezzosi 2018-04-13 14:18:28 +0200
• e25ef31907 Construct the morphism for equivalence 2 Frederik Hanghøj Iversen 2018-04-13 13:24:17 +0200
• 0ced448fa6 Progress on univalence Frederik Hanghøj Iversen 2018-04-13 09:40:09 +0200
• 5bbb40b664 Make progress with univalence in product-category Frederik Hanghøj Iversen 2018-04-12 13:16:25 +0200
• 7fcd8e631a Modified verion of 9.1.9 Frederik Hanghøj Iversen 2018-04-12 11:21:05 +0200
• 7eac677efb Prove 9.1.9 Frederik Hanghøj Iversen 2018-04-12 10:05:02 +0200
• 5c4b4db692 Simplifications Frederik Hanghøj Iversen 2018-04-11 14:10:01 +0200
• 1c963db7e6 Make AreInveres an alias for \Sigma Frederik Hanghøj Iversen 2018-04-11 13:53:33 +0200
• e6a2e3a0f0 Reduce applications of symmetry Frederik Hanghøj Iversen 2018-04-11 13:18:34 +0200
• 770bce52a2 Use 3rd formulation of univalence Frederik Hanghøj Iversen 2018-04-11 12:54:22 +0200
• 4ff8f155ab [QED] Get equivalence from 3rd formulation Frederik Hanghøj Iversen 2018-04-11 12:46:22 +0200
• c23c2716a5 Move lemma to equivalence-module Frederik Hanghøj Iversen 2018-04-11 12:27:33 +0200
• db5fb3603a Banish qualified import of Function - use \o for fun-comp! Frederik Hanghøj Iversen 2018-04-11 11:10:33 +0200
• c90b064bb0 Rename \o to <<< Frederik Hanghøj Iversen 2018-04-11 10:58:50 +0200
• 6d59a8f79e Add note about proving 9.1.9 Frederik Hanghøj Iversen 2018-04-10 17:33:22 +0200
• 772e6778f3 [WIP] Univalence in ad-hoc category in product Frederik Hanghøj Iversen 2018-04-10 17:17:04 +0200
• fd18985e53 Export TypeIsomorphism as an alias for Equivalence.Isomorphism Frederik Hanghøj Iversen 2018-04-09 18:10:39 +0200
• 8c6e327b1c Write stuff about implementation in report Frederik Hanghøj Iversen 2018-04-09 18:02:54 +0200
• 04144db606 Simplifications and renaming Frederik Hanghøj Iversen 2018-04-09 18:02:39 +0200
• 735b25de23 Simplify proof and move propUnivalent to a more general setting Frederik Hanghøj Iversen 2018-04-09 16:03:43 +0200
• 472dbba84d Update backlog Frederik Hanghøj Iversen 2018-04-09 16:03:02 +0200
• 69689e7b2a Use a single version of \simeq Frederik Hanghøj Iversen 2018-04-06 18:27:24 +0200
• 36d92c7ceb Make the category an index of PreCategory Frederik Hanghøj Iversen 2018-04-06 17:09:15 +0200
• 23b562a873 Provide preorder instance for some things - more work on product cat Frederik Hanghøj Iversen 2018-04-06 16:54:00 +0200
• 5db1a1e791 Report-stuff Frederik Hanghøj Iversen 2018-04-05 20:41:36 +0200
• bbe9460647 Provide composition of isEquiv's Frederik Hanghøj Iversen 2018-04-05 20:41:14 +0200
• be56027c37 Remove bad lemma for showing univalence Frederik Hanghøj Iversen 2018-04-05 15:23:05 +0200
• e69ace21a0 Rename id-to-iso to idToIso Frederik Hanghøj Iversen 2018-04-05 15:21:54 +0200
• b5f89322ac Add notion of strict category Frederik Hanghøj Iversen 2018-04-05 15:13:59 +0200
• 6c5b68a8ac Add notion of pre-category Frederik Hanghøj Iversen 2018-04-05 14:37:25 +0200
• 8276deb4aa Rename proj. to fst and snd Frederik Hanghøj Iversen 2018-04-05 10:41:56 +0200
• d78965d73f Try to use lemma for proving univalence of product-category thing Frederik Hanghøj Iversen 2018-04-04 17:45:36 +0200
• 84f88ac2ae Change what is needed Frederik Hanghøj Iversen 2018-04-04 12:01:29 +0200
• f66d180ec3 [WIP] Stronger lemma for univalence Frederik Hanghøj Iversen 2018-04-04 11:27:03 +0200
• 172287f0a7 [QED] The ad-hoc product category has hom-sets that are h-sets Frederik Hanghøj Iversen 2018-04-03 15:23:11 +0200
• 1e5fb7d50a [WIP] Arrows are sets in special product category Frederik Hanghøj Iversen 2018-04-03 14:46:36 +0200
• 467c5d9c0c [WIP] Propositionality of products Frederik Hanghøj Iversen 2018-04-03 12:40:20 +0200
• 1c6d9ad2b5 Rename identity in category to ascii-name Frederik Hanghøj Iversen 2018-04-03 11:36:09 +0200
• 41b442c0d8 Merge remote-tracking branch 'Saizan/dev' into dev Frederik Hanghøj Iversen 2018-03-30 12:23:29 +0200
• 34e633902f Category.Product: Factor out use of arrowAreSets to shorten proofs Andrea Vezzosi 2018-03-30 11:06:45 +0200
• ba80fe96dc [WIP] Propositionality for products Frederik Hanghøj Iversen 2018-03-30 00:12:01 +0200
• 432cc78821 Prove assoc and ident for funky category Frederik Hanghøj Iversen 2018-03-29 15:47:43 +0200
• ffedb83210 Initial objects are also propositional Frederik Hanghøj Iversen 2018-03-29 14:31:03 +0200
• 52ac9b4b78 Terminal objects are propositional Frederik Hanghøj Iversen 2018-03-29 14:26:47 +0200
• af25db7e31 Merge remote-tracking branch 'Saizan/dev' into dev Frederik Hanghøj Iversen 2018-03-29 13:36:09 +0200
• 2f6b129ed6 Move proposal to report, use xelatex Frederik Hanghøj Iversen 2018-03-29 13:32:48 +0200
• 8752b1435d Update report Frederik Hanghøj Iversen 2018-03-29 13:32:06 +0200
• 8ac6b97213 isProp (Product C A B) setup Andrea Vezzosi 2018-03-29 00:07:49 +0200
• facd1167e0 Fix unique existential Frederik Hanghøj Iversen 2018-03-27 14:18:13 +0200
• b7a80d0b86 Proof: Being an initial- terminal- object is a mere proposition Frederik Hanghøj Iversen 2018-03-27 12:20:24 +0200
• 9898685491 Prove that the opposite category is a category Frederik Hanghøj Iversen 2018-03-26 14:11:15 +0200
• d3864dbae5 Move properties about natural transformations to that module Frederik Hanghøj Iversen 2018-03-23 15:20:26 +0100
• ef688202a2 Move identity functor laws to functor module... Frederik Hanghøj Iversen 2018-03-23 13:55:03 +0100
• a713d560d5 Preview target Frederik Hanghøj Iversen 2018-03-23 11:33:55 +0100
• 1dde3f8e74 Restructure latex-stuff Frederik Hanghøj Iversen 2018-03-23 11:22:17 +0100
• 8ff93e04ec Move proposal to doc/ Frederik Hanghøj Iversen 2018-03-23 11:13:52 +0100
• c8c61a8d03 Half-time report Frederik Hanghøj Iversen 2018-03-23 11:11:44 +0100
• 96fb1d3a3b Formatting Frederik Hanghøj Iversen 2018-03-23 10:08:28 +0100
• 73c3b35631 Merge branch 'dev' 1.4.1 Frederik Hanghøj Iversen 2018-03-22 14:52:01 +0100
• 4ae898dfe0 Update backlog and changelog Frederik Hanghøj Iversen 2018-03-22 14:51:43 +0100
• ac01b786a7 Cleanup Frederik Hanghøj Iversen 2018-03-22 14:27:16 +0100
• ebcab2528e Prove second inverse law for from/to-isomorphism Frederik Hanghøj Iversen 2018-03-22 13:49:53 +0100
• 0246c1b5ab Readability Frederik Hanghøj Iversen 2018-03-22 12:25:12 +0100
• d816ba657b QED! Show that the category of homotopic sets are univalent. Frederik Hanghøj Iversen 2018-03-22 12:11:27 +0100
• 52ca0b6732 Merge remote-tracking branch 'Saizan/dev' into dev Frederik Hanghøj Iversen 2018-03-22 11:54:22 +0100
• d12122ce60 Add another approach for univalence in Set Frederik Hanghøj Iversen 2018-03-22 11:50:07 +0100
• 66ab7138a6 generalized lem3 and made progress for Sets univalence Andrea Vezzosi 2018-03-22 10:41:38 +0000
• 807a0f3dcd Slight readability improvement Frederik Hanghøj Iversen 2018-03-21 18:05:25 +0100
• 181edc0cd5 Prove step 3 in proof of unvivalence for hSet without ua Frederik Hanghøj Iversen 2018-03-21 17:52:32 +0100
• 8f67ff9f36 Use explicit parameter for hSet Frederik Hanghøj Iversen 2018-03-21 15:01:31 +0100
• ae0ff092f8 Use prelude everywhere Frederik Hanghøj Iversen 2018-03-21 14:56:43 +0100
• 29f45d1426 Delete equality module Frederik Hanghøj Iversen 2018-03-21 14:47:01 +0100
• 183906dc8c Define and use custom prelude Frederik Hanghøj Iversen 2018-03-21 14:39:56 +0100
• 084befbbc6 Merge remote-tracking branch 'Saizan/dev' into dev Frederik Hanghøj Iversen 2018-03-21 13:27:57 +0100
• cd3514c8cf Formatting Frederik Hanghøj Iversen 2018-03-21 13:25:24 +0100
• ed3b3047e6 Progress on univalence for sets. Andrea Vezzosi 2018-03-21 12:00:47 +0000
• 890154a81d Simplify qualified imports, change make-target: clean Frederik Hanghøj Iversen 2018-03-21 12:28:26 +0100
• e98ed89db5 Make propositionality a submodule of the actual proposition Frederik Hanghøj Iversen 2018-03-21 12:17:10 +0100
• 4beb48e066 Use correct order for left- and right identity Frederik Hanghøj Iversen 2018-03-21 11:46:36 +0100
• 71d9acff9a Stuff about half-time report Frederik Hanghøj Iversen 2018-03-20 17:27:41 +0100
• 31257a4d97 Do not export helpers in Fun Frederik Hanghøj Iversen 2018-03-20 16:50:03 +0100
• 629115661b Formatting in yoneda Frederik Hanghøj Iversen 2018-03-20 16:43:48 +0100
• b6a9befd9c Naming and formatting Frederik Hanghøj Iversen 2018-03-20 16:26:23 +0100
• 63a51fbfdc Include modules in "everything"-module Frederik Hanghøj Iversen 2018-03-20 16:08:37 +0100
• 811a6bf58e Make univalence a submodule of RawCategory Frederik Hanghøj Iversen 2018-03-20 15:19:28 +0100
• b03bfb0c77 Restructure in free monad Frederik Hanghøj Iversen 2018-03-20 14:58:27 +0100
• 66cb5b363d [WIP] Finnish all intermediate steps for univalence of hSets Frederik Hanghøj Iversen 2018-03-20 13:26:40 +0100
• 2188e690a0 Prove identity law for coercions. Frederik Hanghøj Iversen 2018-03-20 12:12:09 +0100
• 30725d71b6 [WIP] Scary goal Frederik Hanghøj Iversen 2018-03-20 11:58:54 +0100
• 32d1833d51 [WIP] A long way towards proving univalence in the category of hSets Frederik Hanghøj Iversen 2018-03-20 11:26:48 +0100
• 43563d1ad9 [WIP] Univalence for category of homotopy sets Frederik Hanghøj Iversen 2018-03-19 16:27:03 +0100