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

• 2058154c65 Helpers to work with isomorphisms and equivalences Frederik Hanghøj Iversen 2018-03-19 15:15:03 +0100
• f69ab0ee62 [WIP] Univalence for the category of hSets Frederik Hanghøj Iversen 2018-03-19 14:08:59 +0100
• f7f8953a42 Voe: Use the isomorphism directly for better computation Andrea Vezzosi 2018-03-15 13:39:42 +0000
• 438978973d Construct isomorphism from equivalence Frederik Hanghøj Iversen 2018-03-15 11:04:15 +0100
• 360e2b95dd Make parameter to monad equivalence explicit Frederik Hanghøj Iversen 2018-03-14 11:20:07 +0100
• 7aec22b30a Expose both monad formulations qualified from Cat.Category.Monad Frederik Hanghøj Iversen 2018-03-14 11:00:52 +0100
• 6229decfb2 Merge branch 'master' into dev Frederik Hanghøj Iversen 2018-03-14 10:50:57 +0100
• 41e2d02c8d [WIP] Prove voe §2.3 Frederik Hanghøj Iversen 2018-03-14 10:30:42 +0100
• 091e77b583 Rename IsProduct.isProduct to IsProduct.ump Frederik Hanghøj Iversen 2018-03-14 10:23:23 +0100
• 7065455712 More readable goal for voevodsky's construction Frederik Hanghøj Iversen 2018-03-13 11:29:13 +0100
• 3ab88395dc Merge branch 'dev' 1.4.0 Frederik Hanghøj Iversen 2018-03-13 10:41:54 +0100
• 6db2a3e5d4 Update changelog and backlog Frederik Hanghøj Iversen 2018-03-13 10:40:43 +0100
• 896e0d3d37 Stuff about univalence for the category of functors Frederik Hanghøj Iversen 2018-03-13 10:24:50 +0100
• fe453a6d3a Trying to prove cummulativity of homotopy levels Frederik Hanghøj Iversen 2018-03-12 16:00:27 +0100
• c52384b012 Change name of fromMonad Frederik Hanghøj Iversen 2018-03-12 14:43:43 +0100
• 5e092964c8 Change naming and fuse some modules Frederik Hanghøj Iversen 2018-03-12 14:38:52 +0100
• ccf753d438 Move monoidal and kleisli representation to own modules Frederik Hanghøj Iversen 2018-03-12 14:20:49 +0100
• 8dadfa22a0 Add documentation header to monad module Frederik Hanghøj Iversen 2018-03-12 14:11:31 +0100
• aa645fb11e Move voevodsky's construction to own module Frederik Hanghøj Iversen 2018-03-12 14:04:10 +0100
• c0cf6789cd Use propositions straight from the horses mouth Frederik Hanghøj Iversen 2018-03-12 13:56:49 +0100
• a7214fcc66 Finish equality principle for categories Frederik Hanghøj Iversen 2018-03-12 13:51:29 +0100
• 35390c02d3 Stuff about univalence in the category of sets Frederik Hanghøj Iversen 2018-03-12 13:36:55 +0100
• acb5ff4f2b Closer to showing univalence for the category of sets Frederik Hanghøj Iversen 2018-03-08 14:44:23 +0100
• 52297d9073 Clean-up in the category of categories Frederik Hanghøj Iversen 2018-03-08 11:54:13 +0100
• d01514cbdb Do not use ugly ':'-syntax to disambiguate fields Frederik Hanghøj Iversen 2018-03-08 11:29:16 +0100
• 48672b01bd Use dotted expression in Cat Frederik Hanghøj Iversen 2018-03-08 11:20:51 +0100
• 5ad506a09f Rename func* and func-> to omap and fmap respectively Frederik Hanghøj Iversen 2018-03-08 11:03:56 +0100
• 2fcc583646 Add note Frederik Hanghøj Iversen 2018-03-08 10:50:18 +0100
• 63b5f5c68d Use long name for product object Frederik Hanghøj Iversen 2018-03-08 10:45:15 +0100
• 486238e114 Add goals for propositionality of products Frederik Hanghøj Iversen 2018-03-08 10:38:46 +0100
• 1ef57a19f4 Cosmetics Frederik Hanghøj Iversen 2018-03-08 10:30:35 +0100
• 4e7b350188 Factor out objects Frederik Hanghøj Iversen 2018-03-08 10:28:05 +0100
• 181bd1af53 Factor out category Frederik Hanghøj Iversen 2018-03-08 10:23:37 +0100
• faf4c54188 Make parameters explicit Frederik Hanghøj Iversen 2018-03-08 10:22:21 +0100
• fae492a1e3 Restructure products Frederik Hanghøj Iversen 2018-03-08 10:20:29 +0100
• b61749bb91 Fixup some todo-notes Frederik Hanghøj Iversen 2018-03-08 01:09:40 +0100
• fa9a470875 Update backlog Frederik Hanghøj Iversen 2018-03-08 00:54:42 +0100
• e43bee6d9f Feels really close Frederik Hanghøj Iversen 2018-03-08 00:36:38 +0100
• c8fef1d2b5 Use different name for function composition Frederik Hanghøj Iversen 2018-03-08 00:22:55 +0100
• 36cbe711fb Sort of half of the proof of an inverse Frederik Hanghøj Iversen 2018-03-08 00:09:49 +0100
• 459718da23 Finish proof of equivalence of klesili/monoidal categories!! Frederik Hanghøj Iversen 2018-03-07 17:30:09 +0100
• 19103e1678 Update cubical Frederik Hanghøj Iversen 2018-03-07 16:24:43 +0100
• 50f51db4fc Update readme Frederik Hanghøj Iversen 2018-03-07 15:40:52 +0100
• 3749124d09 Switch to experimental branch of stdlib Frederik Hanghøj Iversen 2018-03-07 15:38:37 +0100
• 93d075a6d3 Attempt at proving pureNTEq Frederik Hanghøj Iversen 2018-03-07 15:23:07 +0100
• bf605e09fe Update commit refs Frederik Hanghøj Iversen 2018-03-07 15:10:36 +0100
• 00e6e1aa66 State problem with approach Frederik Hanghøj Iversen 2018-03-07 11:45:11 +0100
• aa64e01084 Remove some cruft Frederik Hanghøj Iversen 2018-03-07 11:33:08 +0100
• 125123846e Lay out a strategy for showing the equivalence Frederik Hanghøj Iversen 2018-03-07 11:29:58 +0100
• 085e6eb3d7 Stuff about voe-2-3 Frederik Hanghøj Iversen 2018-03-06 23:18:23 +0100
• 110e3510c5 Use postulates Frederik Hanghøj Iversen 2018-03-06 15:55:03 +0100
• 5ae68df582 Prove that fmap is mapped correctly Frederik Hanghøj Iversen 2018-03-06 15:52:22 +0100
• 4d528a7077 Clean-up Frederik Hanghøj Iversen 2018-03-06 11:25:29 +0100
• 485703c85e Tidy up Frederik Hanghøj Iversen 2018-03-06 10:16:42 +0100
• 0cebe1e866 Make private Frederik Hanghøj Iversen 2018-03-06 10:06:45 +0100
• 4de27aa06c Naming Frederik Hanghøj Iversen 2018-03-06 10:05:35 +0100
• 9173468b03 Use omap/fmap Frederik Hanghøj Iversen 2018-03-06 09:56:44 +0100
• bdd67aee53 Rename RR to Romap Frederik Hanghøj Iversen 2018-03-06 09:55:18 +0100
• c57cd5c991 Define stuff in monoidal record Frederik Hanghøj Iversen 2018-03-06 09:52:01 +0100
• cfb7925cb5 Renaming Frederik Hanghøj Iversen 2018-03-06 09:45:04 +0100
• b6457a0b14 Add comment Frederik Hanghøj Iversen 2018-03-06 09:41:29 +0100
• 7647a452cd Tidy up proof a bit Frederik Hanghøj Iversen 2018-03-06 09:39:48 +0100
• 35419ad86e Rename eta and mu Frederik Hanghøj Iversen 2018-03-06 09:30:41 +0100
• f8e08288a0 Cosmetics Frederik Hanghøj Iversen 2018-03-05 17:31:13 +0100
• 9ec6ce9eba Use other equality principle Frederik Hanghøj Iversen 2018-03-05 17:10:41 +0100
• 3151fb3e46 Prove propositionality for naturality Frederik Hanghøj Iversen 2018-03-05 16:35:47 +0100
• 7f4a8a65b8 More stuff about opposite being an involution Frederik Hanghøj Iversen 2018-03-05 16:10:27 +0100
• b26ea18257 Cleanup in nattrans Frederik Hanghøj Iversen 2018-03-05 15:04:16 +0100
• ddd5f17c05 Move propositionality stuff about natural transformations to that module Frederik Hanghøj Iversen 2018-03-05 15:02:36 +0100
• 2b92cee254 Prettier names in Fun Frederik Hanghøj Iversen 2018-03-05 14:53:32 +0100
• bb379fa196 Implement category of presheaves Frederik Hanghøj Iversen 2018-03-05 14:50:53 +0100
• ce4dd83969 Prove that the yoneda embedding is distributive Frederik Hanghøj Iversen 2018-03-05 14:42:12 +0100
• 7fbca1aeeb Clean-up yoneda embedding Frederik Hanghøj Iversen 2018-03-05 14:04:04 +0100
• 1bf565b87a Have yoneda without having a category of categories Frederik Hanghøj Iversen 2018-03-05 13:52:41 +0100
• 5c3616bca5 Make argument to presheaf explicit Frederik Hanghøj Iversen 2018-03-05 11:17:31 +0100
• 059c74b687 Use already defined category Frederik Hanghøj Iversen 2018-03-05 11:15:45 +0100
• a4890a42cf Define Monoidal categories without depending on category of categories Frederik Hanghøj Iversen 2018-03-05 11:13:37 +0100
• 5902c6121b Further reduce dependency on impossible facts. Frederik Hanghøj Iversen 2018-03-05 11:01:36 +0100
• 77006011d3 Minimize dependency on category of categories Frederik Hanghøj Iversen 2018-03-05 10:35:33 +0100
• 8f8800cb67 More stuff about kleisli \equiv monoidal Frederik Hanghøj Iversen 2018-03-05 10:28:16 +0100
• b079f5e426 Prove propositionality for IsMonad Frederik Hanghøj Iversen 2018-03-02 13:31:46 +0100
• c4e3625746 Finish proof of distributivity Frederik Hanghøj Iversen 2018-03-01 20:47:36 +0100
• 2ceb027f7a Prove monad-equality principle for kleisly monads Frederik Hanghøj Iversen 2018-03-01 20:23:34 +0100
• f2164a6717 Prove equality principle for monads Frederik Hanghøj Iversen 2018-03-01 20:12:49 +0100
• a7f31bb3e2 Prove "foreign naturality condition" Frederik Hanghøj Iversen 2018-03-01 18:00:51 +0100
• f526fd6010 Prove inverse law Frederik Hanghøj Iversen 2018-03-01 17:50:06 +0100
• ff2952e9ad Make postulate Frederik Hanghøj Iversen 2018-03-01 14:58:49 +0100
• ae46a48861 Define goals in Kleisli Frederik Hanghøj Iversen 2018-03-01 14:58:01 +0100
• 64a0292755 Cosmetics Frederik Hanghøj Iversen 2018-03-01 14:19:46 +0100
• e8b29e1f7f \mu is join and it's a natural transformation! Frederik Hanghøj Iversen 2018-02-28 23:41:59 +0100
• 9d3b17245f Provide \zeta Frederik Hanghøj Iversen 2018-02-28 19:31:53 +0100
• f2b1a36a75 Define and use Endofunctor Frederik Hanghøj Iversen 2018-02-28 19:03:11 +0100
• 3c77c69cf6 Move functor definition to Kleisli.Monad Frederik Hanghøj Iversen 2018-02-28 19:00:21 +0100
• 70221377d3 Move proof of equivalence to IsMonad making them lemmas Frederik Hanghøj Iversen 2018-02-28 18:55:32 +0100
• 1aaf81552c Move another proof to category definition Frederik Hanghøj Iversen 2018-02-26 20:36:39 +0100
• 101b2639e1 Move proof to category definition Frederik Hanghøj Iversen 2018-02-26 20:31:47 +0100
• 5b5d21f777 Formatting Frederik Hanghøj Iversen 2018-02-26 20:23:31 +0100
• a0944d69b1 Documentation in Monad Frederik Hanghøj Iversen 2018-02-26 20:08:48 +0100
• 67993be27b Add reverse function composition to category Frederik Hanghøj Iversen 2018-02-26 19:59:11 +0100
• 47882b1110 Rename zeta to pure Frederik Hanghøj Iversen 2018-02-26 19:58:27 +0100