-
Notifications
You must be signed in to change notification settings - Fork 23
/
idris-ct.ipkg
100 lines (91 loc) · 2.71 KB
/
idris-ct.ipkg
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
package idris-ct
{-
SPDX-License-Identifier: AGPL-3.0-only
This file is part of `idris-ct` Category Theory in Idris library.
Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU Affero General Public License for more details.
You should have received a copy of the GNU Affero General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
-}
modules
= Basic.Category
, Basic.DiagonalFunctor
, Basic.Functor
, Basic.Isomorphism
, Basic.NaturalIsomorphism
, Basic.NaturalTransformation
, Booleans.BooleanCoLimits
, Booleans.BooleanLimits
, Booleans.Booleans
, Cats.CatsAsCategory
, Cats.FunctorsAsCategory
, CoLimits.CoCone
, CoLimits.CoConeCat
, CoLimits.CoLimit
, CoLimits.CoLimitAsInitialObject
, CoLimits.CoProduct
, CoLimits.InitialObject
, CoLimits.InitialObjectAsCoLimit
, CoLimits.Pushout
, Comma.CommaCategory
, Comma.OverCategory
, Comma.UnderCategory
, CommutativeDiagram.Diagram
, Comonad.Comonad
, Day.CovariantDayConvolution
, Discrete.DiscreteCategory
, Discrete.DiscreteFunctor
, Dual.DualCategory
, Dual.DualFunctor
, Empty.EmptyCategory
, Empty.EmptyFunctor
, Graph.FreeFunctor
, Graph.Graph
, Graph.Path
, Graph.PathCategory
, Hom.HomFunctor
, Idris.EitherAsCoProduct
, Idris.FunctorAsCFunctor
, Idris.PairAsProduct
, Idris.TypesAsCategory
, Idris.TypesAsCategoryExtensional
, Lens.Lens
, Lens.SimpleLens
, Limits.Limit
, Limits.Pullback
, Limits.TerminalObject
, Monad.IOMonad
, Monad.KleisliCategory
, Monad.Monad
, Monad.VerifiedMonadAsMonad
, Monoid.Monoid
, Monoid.MonoidAsCategory
, Monoid.MonoidMorphism
, Monoid.MonoidMorphismAsFunctor
, Monoid.MonoidsCategory
, MonoidalCategory.MonoidalCategory
, MonoidalCategory.MonoidalCategoryHelpers
, MonoidalCategory.MonoidalFunctor
, MonoidalCategory.StrictMonoidalCategory
, MonoidalCategory.SymmetricMonoidalCategory
, MonoidalCategory.SymmetricMonoidalCategoryHelpers
, PointedTypes.PointedTypesAsCategory
, Preorder.MonotoneMap
, Preorder.MonotoneMapAsFunctor
, Preorder.PreorderAsCategory
, Preorder.UniquePreorder
, Product.ProductCategory
, Product.ProductFunctor
, Profunctors.Profunctor
, Unit.UnitCategory
, CategoryReasoning
, Utils
sourcedir = src
pkgs = contrib