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

• 043641462d Prove distributive law for monads! Frederik Hanghøj Iversen 2018-02-26 19:57:05 +0100
• 7cddba97a8 Shorten definition Frederik Hanghøj Iversen 2018-02-25 19:03:30 +0100
• 9c8bc1b1f4 Merge branch 'dev' 1.3.0 Frederik Hanghøj Iversen 2018-02-25 15:38:23 +0100
• 7518a642f6 Update changelog Frederik Hanghøj Iversen 2018-02-25 15:38:12 +0100
• 2c6132768e Remove Pathy and Bij Frederik Hanghøj Iversen 2018-02-25 15:29:52 +0100
• 5caecf9796 Rename properties to yoneda Frederik Hanghøj Iversen 2018-02-25 15:28:42 +0100
• 44526b85eb Move CwF Frederik Hanghøj Iversen 2018-02-25 15:24:44 +0100
• f0beec1530 Rename Opposite to opposite Frederik Hanghøj Iversen 2018-02-25 15:23:33 +0100
• cd98736d02 Add documentation in Category-module Frederik Hanghøj Iversen 2018-02-25 15:21:38 +0100
• 2e7220567a Move lemma into IsCategory Frederik Hanghøj Iversen 2018-02-25 14:44:03 +0100
• d63ecc3a65 Use abbreviation Frederik Hanghøj Iversen 2018-02-25 14:39:11 +0100
• caddf83a09 Let IsCategory reexport RawCategory Frederik Hanghøj Iversen 2018-02-25 14:37:28 +0100
• 5deabb7546 Forgot to add monoid-module Frederik Hanghøj Iversen 2018-02-25 14:28:01 +0100
• ce46e0ae7a Module-ify Frederik Hanghøj Iversen 2018-02-25 14:27:37 +0100
• 12dddc2067 Use a module Frederik Hanghøj Iversen 2018-02-25 03:12:23 +0100
• 4c298855e0 [WIP] Proving other fusion law Frederik Hanghøj Iversen 2018-02-25 03:09:25 +0100
• a6b01929f0 Prove distributive law Frederik Hanghøj Iversen 2018-02-25 01:27:20 +0100
• a447cd9c7c Syntax Frederik Hanghøj Iversen 2018-02-24 20:41:47 +0100
• 9d09363f78 Expand definition of isDistributive somewhat Frederik Hanghøj Iversen 2018-02-24 20:37:21 +0100
• e7abab0e4c Add pure and >=> to kleisli category Frederik Hanghøj Iversen 2018-02-24 19:08:20 +0100
• be505cdfbe Prove IsAssociative Frederik Hanghøj Iversen 2018-02-24 19:07:58 +0100
• 5d9c820fa2 Add note about haskell Frederik Hanghøj Iversen 2018-02-24 15:25:07 +0100
• e4e327d1d2 [WIP] equivalence of kleisli- resp. monoidal- representation of monad Frederik Hanghøj Iversen 2018-02-24 15:13:25 +0100
• 3e12331294 Monoidal monads addendum Frederik Hanghøj Iversen 2018-02-24 14:01:57 +0100
• 4ec13fe509 Implement monads in the kleisli form Frederik Hanghøj Iversen 2018-02-24 14:00:52 +0100
• 0ca11874bc Remove old name for functor composition Frederik Hanghøj Iversen 2018-02-24 12:55:08 +0100
• 8527fe0df4 Rename functor composition - implement monads... Frederik Hanghøj Iversen 2018-02-24 12:52:16 +0100
• cb8533b84a Rename natural transformation composition Frederik Hanghøj Iversen 2018-02-23 17:43:38 +0100
• dd11b69c71 Documentation for natural transformations Frederik Hanghøj Iversen 2018-02-23 17:37:27 +0100
• 689a6467c6 Move stuff about natural transformations to own module Frederik Hanghøj Iversen 2018-02-23 17:33:09 +0100
• f5dded9561 Do not use IsCategory directly Frederik Hanghøj Iversen 2018-02-23 16:41:17 +0100
• 39284b8d99 Changes in CwF Frederik Hanghøj Iversen 2018-02-23 14:13:55 +0100
• 5796b791b8 Almost prove that arrows are sets in the cateogry of families Frederik Hanghøj Iversen 2018-02-23 13:59:35 +0100
• a321a9c8b2 Use hLevels in Fam Frederik Hanghøj Iversen 2018-02-23 13:36:54 +0100
• 29e9ef689a Merge branch 'dev' Frederik Hanghøj Iversen 2018-02-23 13:20:41 +0100
• 3d0916f448 Use correct name for hSets Frederik Hanghøj Iversen 2018-02-23 13:20:30 +0100
• 82c89a78c2 Merge branch 'dev' Frederik Hanghøj Iversen 2018-02-23 13:19:11 +0100
• ee2b30d640 Update commit references Frederik Hanghøj Iversen 2018-02-23 13:18:47 +0100
• 151d5c995b Merge branch 'master' of github.com:fredefox/cat Frederik Hanghøj Iversen 2018-02-23 12:58:57 +0100
• c3b585d03b Merge branch 'dev' 1.2.0 Frederik Hanghøj Iversen 2018-02-23 12:57:19 +0100
• 002badd98d Update changelog Frederik Hanghøj Iversen 2018-02-23 12:57:10 +0100
• 4874ed0795 Rename distrib to isDistributive Frederik Hanghøj Iversen 2018-02-23 12:53:35 +0100
• 7787a8f0be Indentation Frederik Hanghøj Iversen 2018-02-23 12:52:14 +0100
• 48423cc816 Rename arrowIsSet to arrowsAreSets Frederik Hanghøj Iversen 2018-02-23 12:51:44 +0100
• 6446435a49 Rename ident to isIdentity Frederik Hanghøj Iversen 2018-02-23 12:49:41 +0100
• 5cbc409770 Rename assoc to isAssociative Frederik Hanghøj Iversen 2018-02-23 12:43:49 +0100
• 852056cc44 Add type-synonyms in functor Frederik Hanghøj Iversen 2018-02-23 12:41:15 +0100
• a57f45d93f Remove yet another postulate Frederik Hanghøj Iversen 2018-02-23 12:33:20 +0100
• 34dec9406d Do not mention IsFunctor outside the module that defines it Frederik Hanghøj Iversen 2018-02-23 12:29:10 +0100
• e46edf1f68 Chain reexport things in Functor Frederik Hanghøj Iversen 2018-02-23 12:21:16 +0100
• 885fd8fa69 Drastically simplify proofs Frederik Hanghøj Iversen 2018-02-23 12:15:16 +0100
• 3f3247c870 Remove commented code Frederik Hanghøj Iversen 2018-02-23 12:05:38 +0100
• de1d19c442 Readd stuff about the yoneda embedding Frederik Hanghøj Iversen 2018-02-23 11:23:21 +0100
• 954a89f8d1 Expose naturalIsProp Frederik Hanghøj Iversen 2018-02-23 11:12:27 +0100
• bc2129b8fc Readd yoneda embedding Frederik Hanghøj Iversen 2018-02-23 10:53:11 +0100
• 9a4d79fa4e Readd commented code Frederik Hanghøj Iversen 2018-02-23 10:44:23 +0100
• 3032dc6130 Make explicit argument Frederik Hanghøj Iversen 2018-02-23 10:36:59 +0100
• cc1ddaac9f Add new type-synonym Frederik Hanghøj Iversen 2018-02-23 10:35:42 +0100
• a87d404aad Refactor category of categories Frederik Hanghøj Iversen 2018-02-23 10:34:37 +0100
• 32b9ce2ea8 Use new syntax in cat Frederik Hanghøj Iversen 2018-02-22 15:31:54 +0100
• 1b6798f229
  Update README.md Frederik Hanghøj Iversen 2018-02-21 18:23:55 +0100
• 5b2681392c Merge branch 'dev' 1.1.0 Frederik Hanghøj Iversen 2018-02-21 14:06:24 +0100
• 7ed99a6bb4 Add backlog and changelog Frederik Hanghøj Iversen 2018-02-21 14:06:09 +0100
• a82095604d Remove unused function Frederik Hanghøj Iversen 2018-02-21 14:05:10 +0100
• 7398210a2b Update readme Frederik Hanghøj Iversen 2018-02-21 13:52:51 +0100
• 8f620e0dbe Update commit references Frederik Hanghøj Iversen 2018-02-21 13:43:26 +0100
• 9e96e704e8 Update Fun according to new naming policy Frederik Hanghøj Iversen 2018-02-21 13:40:24 +0100
• 57d7eab4cb Make sets a category according to HoTT Frederik Hanghøj Iversen 2018-02-21 13:37:07 +0100
• ed40824edc Cosmetics Frederik Hanghøj Iversen 2018-02-21 12:59:31 +0100
• edf552cb86 Do not define synonym for contractible Frederik Hanghøj Iversen 2018-02-20 18:15:07 +0100
• d2da84269f Move some more things into RawCategory Frederik Hanghøj Iversen 2018-02-20 18:14:42 +0100
• 0c861c4bde Factor univalence out to a seperate module Frederik Hanghøj Iversen 2018-02-20 18:11:14 +0100
• a4f8a37e36 Proove that IsCategory is a mere proposition! Frederik Hanghøj Iversen 2018-02-20 18:01:26 +0100
• 159bffa6ae Factor out more from IsCategory Frederik Hanghøj Iversen 2018-02-20 17:59:48 +0100
• a016c67b88 Succesfully apply path-induction. Frederik Hanghøj Iversen 2018-02-20 17:44:44 +0100
• ff496aae09 Factor out a useful type-family Frederik Hanghøj Iversen 2018-02-20 17:33:02 +0100
• 860c91f913 Trim mess Frederik Hanghøj Iversen 2018-02-20 16:42:56 +0100
• 8ef61d9db0 Simplify Category Frederik Hanghøj Iversen 2018-02-20 16:25:49 +0100
• 10df9511a4 Move various type-synonyms to RawCategory Frederik Hanghøj Iversen 2018-02-20 16:22:38 +0100
• 38ec53d5c2 Cosmetics Frederik Hanghøj Iversen 2018-02-20 14:08:47 +0100
• 44eda0ced0 Stuff about propositionality of fields of IsCategory Frederik Hanghøj Iversen 2018-02-19 15:46:19 +0100
• bec5acdc59 Move proposition to wishlist Frederik Hanghøj Iversen 2018-02-19 11:25:16 +0100
• 89ad60ffef Stuff about the free category Frederik Hanghøj Iversen 2018-02-19 11:09:49 +0100
• 73ab4d1836 Proove identity laws for natural transformations Frederik Hanghøj Iversen 2018-02-16 12:46:25 +0100
• a64e2484e3 Prove associativity for natural transformations Frederik Hanghøj Iversen 2018-02-16 12:24:58 +0100
• b8994b8f4a Merge branch 'dev' Frederik Hanghøj Iversen 2018-02-16 12:04:29 +0100
• 7dc7a5aee3 Prove that naturalTransformations are sets Frederik Hanghøj Iversen 2018-02-16 12:03:02 +0100
• 23c458983c Rely on global cubical again Frederik Hanghøj Iversen 2018-02-16 11:36:44 +0100
• 8a3a519955 Do not use depend-flag Frederik Hanghøj Iversen 2018-02-16 10:25:33 +0100
• ad84b15da5 [WIP] natural transformations are sets Frederik Hanghøj Iversen 2018-02-16 10:22:46 +0100
• 7d4aae4f49 Try to show that natural transformations are sets Frederik Hanghøj Iversen 2018-02-09 12:09:59 +0100
• 56d689fb4b Use arrowIsSet to simplify equality constructor for functors Frederik Hanghøj Iversen 2018-02-07 20:19:17 +0100
• 4df4231906 Merge branch 'dev' Frederik Hanghøj Iversen 2018-02-06 14:31:28 +0100
• 9349b37550 Refactor Functor - only in module Functor Frederik Hanghøj Iversen 2018-02-06 14:24:34 +0100
• a27292dd53 Stuff about the free category Frederik Hanghøj Iversen 2018-02-06 11:27:22 +0100
• 9f1e82168f Move the free category Frederik Hanghøj Iversen 2018-02-06 10:35:52 +0100
• 0688f5c372 Rename arrowIsSet Frederik Hanghøj Iversen 2018-02-06 10:34:43 +0100
• e8ac6786ff Changes to the category of categories Frederik Hanghøj Iversen 2018-02-05 16:35:33 +0100
• e8215b2c05 Move product, exponential, ... Frederik Hanghøj Iversen 2018-02-05 14:59:53 +0100
• 83ccde62e9 Use co-patterns Frederik Hanghøj Iversen 2018-02-05 14:47:15 +0100