data-category: Category theory

[ bsd3, category-theory, library, math ] [ Propose Tags ]

Data-category is a collection of categories, and some categorical constructions on them.

You can restrict the types of the objects of your category by using a GADT for the arrow type. To be able to proof to the compiler that a type is an object in some category, objects also need to be represented at the value level. The corresponding identity arrow of the object is used for that.

See the Boolean and Product categories for some examples.

Note: Strictly speaking this package defines Hask-enriched categories, not ordinary categories (which are Set-enriched.) In practice this means we are allowed to ignore undefined (f.e. when talking about uniqueness of morphisms), and we can treat the categories as normal categories.

Versions [faq] 0.0.1, 0.0.2, 0.0.3, 0.0.3.1, 0.1.0, 0.2.0, 0.3.0, 0.3.0.1, 0.3.0.2, 0.3.1, 0.3.1.1, 0.4, 0.4.1, 0.5.0, 0.5.1, 0.5.1.0, 0.5.1.1, 0.6.0, 0.6.1, 0.6.2, 0.7, 0.7.1, 0.7.2, 0.8, 0.8.1, 0.8.2, 0.9, 0.10
Dependencies None [details]
License BSD-3-Clause
Author Sjoerd Visscher
Maintainer sjoerd@w3future.com
Category Math
Home page http://github.com/sjoerdvisscher/data-category
Bug tracker http://github.com/sjoerdvisscher/data-category/issues
Source repo head: git clone git://github.com/sjoerdvisscher/data-category.git
Uploaded by SjoerdVisscher at 2020-05-11T15:33:07Z
Distributions NixOS:0.10
Downloads 16430 total (1423 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2020-05-11 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees