A new Categories library for Agda
Home Page: https://agda.github.io/agda-categories
License: MIT License
Note that this README is only about Agda, not its standard library. See the Agda Wiki for information about the library.
HACKING
![dependabot[bot] avatar](https://avatars.githubusercontent.com/in/29110?v=4 "dependabot[bot]")
as @sstucki pointed out, there are predicates having the names of properties. this is ultimately due to the old library. on the other hand, we want to keep the style of this library as close to stdlib as possible, so it does make sense to define X and IsX separately.
No, not monads on a bicategory (though these seem interesting too), but rather a twining of a monad and a comonad. https://arxiv.org/abs/0710.1163.
extending #5 (comment)
Square is more than squares. potentially Morphism.Reasoning a better place for it?
agda-categories/Categories/Category/Monoidal/Braided.agda
Lines 37 to 53 in 2eb7858
I believe the definition of a braided category should also include the small axiom:
triangle : [ X ⊗₀ unit ⇒ X ]⟨
B ⇒⟨ unit ⊗₀ X ⟩
unitorˡ.from
≈ unitorʳ.from
⟩
I tried to prove this, got a fair ways in, and got stuck. I don't think it is fundamental, just that I'm missing something that will likely turn out to be simple. Also, my definitions might be off a bit, which certainly wouldn't help matters.
I've pushed my attempts onto branch 'CatsCCC' (as I can't attach .agda files easily here). Holes 3 and 5 in particular. I think the rest are ok, just tedious.
the equivalence of Grothendieck construction looks strange to me.
consider the following diagram:
the current definition only has f and g equivalent, but I suppose the triangle in category FB does not necessarily commute, does it?
I noticed that there are names in some definitions that are not quite reasonable.
For example, https://github.com/agda/agda-categories/blob/master/Categories/Object/Product/Core.agda
commute₁ : π₁ ∘ ⟨ h , i ⟩ ≈ h
commute₂ : π₂ ∘ ⟨ h , i ⟩ ≈ i
universal : π₁ ∘ h ≈ i → π₂ ∘ h ≈ j → ⟨ i , j ⟩ ≈ hhere universal shouldn't be universal, but unique, because it reflects the uniqueness of product. rather, commutes are universality.
probably the names should be reviewed to achieve consistency.
compatibility with unitors.
c.f. https://ncatlab.org/nlab/show/braided+monoidal+category
these names are too general and hard to ring a bell in a proof because f and g just look like normal morphisms. so it's probably a good idea to change them to from and to.
agda-categories/Categories/Category/CartesianClosed.agda
Lines 166 to 169 in 7c22ad4
the notion is inconsistent. to write as -^-, it means the bifunctor needs to have type Bifunctor 𝒞 𝒞.op 𝒞 but the current type is more typical. probably some other notation is needed, something like _⇨_.
the idea of to define assoc-sym. the motivation is that this allows op of op to be definitionally equal to the original category. this is a handy treatment to avoid unnecessary setup.
See the Coq code at https://github.com/ekiciburak/ComparisonTheorem-MacLane . There's a paper too. Looks like fun.
I should acquaint myself with all the current code that @HuStmpHrrr has written.
I am tempted to show Cats has all exponentials, which makes Cats a cartesian closed category. the problem is that the proof of cartesian closed category is in Monoidal, and where should cartesian closed category lives. I figure that probably Category.Instance.Cats.Properties is a better place to fit all these properties and is a single place to find the properties of Cats. Sets, Setoids have a similar situation.
see commit 08df00c
I think the library is close to being in a state to be officially released. I think #23 should be fixed first, just so that it works with a currently-released library. What other issues should be closed before a release?
I might wish to call the release 0.1. There's still lots to do, but it is quite usable as is.
Compiling Everything fails with the error
Categories/Category/Construction/Graphs.agda:29,8-86
Failed to find source of module
Relation.Binary.Construct.Closure.ReflexiveTransitive.Equivalence
I'm using the latest version (master) of the standard library. Am I missing a patch?
As discussion on various issues make clear (#44 being just the latest), it would be quite useful to have parts of the library, especially that part which makes strong use of ≡ such as StrictCats, also be able to use the K axiom. But the whole library is currently built using --without-K` (on purpose).
So this leads to a non-trivial organization question. For example, should there be a WithK hierarchy right below Categories (or even parallel to it?) for that? Or should they be intertwined, the way it is for stdlib? I see pros and cons to both, and am undecided which I prefer.
agda-categories/Categories/Category/Instance/Properties/Setoids.agda:81,22-28
Ambiguous name Cocone. It could refer to any one of
Categories.Diagram.Cocone.Cocone bound at
agda-categories/Categories/Diagram/Cocone.agda:20,8-14
Categories.Category.Construction.Cocones.Cocone bound at
agda-categories/Categories/Diagram/Cocone.agda:20,8-14
Categories currently don't carry an explicit notion of equality on objects. This seems to be a "standard" way to mechanize categories constructively (as far as I'm aware), it is in line with the principle of equivalence, and it also simplifies the definition of Category greatly.
However, I'm worried that some rather elementary category theory silently assumes that objects really do have an equality (despite all the talk about this being evil). For example, one may define things like the hom-functor Hom : Cᵒᵖ × C → Sets from some category C to the category of sets. But in a constructive setting, we surely want to remember the notion of equality on morphisms in C so it's more accurate to type this as Hom : Cᵒᵖ × C → Setoids. (And this is indeed what seems to be implemented in Categories.Functor.Hom).
Another example is the adjunction between the forgetful functor from Cats to Sets and the Discrete functor in the opposite direction. In text-book category theory, both Cats and Sets are CCCs, so this adjunction should consist of a pair of cartesian functors. Following a short discussion with @JacquesCarette on Twitter, I have tried to mechanize this IMO very elementary result, but have failed so far. Here's a summary of what I've tried so far:
Sets is cartesian closed — this fails because it seems to require function extensionality (at least as Sets is currently defined).Setoids, which is a CCC, instead of Sets. Now we need to pick a notion of equality on objects as we go from Cats to Setoids.
There might be other options, but ultimately I think that if one wanted to mechanize a "classic" text-book on category theory, one would be forced to use a more "evil" notion of constructive categories, such as Palmgren's H-categories. I don't think that's too bad though. I see no reason that the two notions of categories could coexist in the same library, in principle.
I was looking at Bicategory and realized that what is defined as 2-Category is in fact bicategory, as their difference is merely that in 2-Category equivalence between 1-cells is strict equality while in Bicategory such equivalence becomes natural isomorphism. the current definition of 2-Category lies in the later definition. I propose let's make it clear and rename it to Bicategory.
it appears that in order to define 2-Category in the sense of traditional CT, it requires to express strict categories and comparison for strict equality of functors, and that probably requires K.
the problem lies in that the two functors map to setoids category in different universe level.
this is kind of bad, because it means going from the naturally isomorphic hom functors to unit-counit definition also would not work.
I suppose the workaround is to implement Lift functor: https://github.com/copumpkin/categories/blob/master/Categories/Lift.agda
It isn't used all that often, and so probably belongs on its own.
This is present in both Object.Power and in pi-dual. Should be in neither!
I think type check now requires more memory.
Checking Categories.Category.Instance.Zero (/home/hu/projects/agda-categories/Categories/Category/Instance/Zero.agda).
Checking Categories.Category.Monoidal.Properties (/home/hu/projects/agda-categories/Categories/Category/Monoidal/Properties.agda).
Checking Categories.Category.Monoidal.Closed.IsClosed (/home/hu/projects/agda-categories/Categories/Category/Monoidal/Closed/IsClosed.agda).
agda: Heap exhausted;
agda: Current maximum heap size is 5368709120 bytes (5120 MB).
agda: Use `+RTS -M<size>' to increase it.
Makefile:6: recipe for target 'test' failed
make: *** [test] Error 251
there is definitely something can be done on Agda's side.
Right now, it is defined in Morphism, but it is really about two objects being isomorphic. Defining Epi and Mono in Morphism makes sense.
there is no need to redefine the same concept. should get this fixed.
As per comments on c968c74, we need to set up a Travis instance with sanity checks to enforce the agreed upon conventions.
it appears that all concepts defined by records have eta expansion. the problem I suppose to have is that, with eta expansion, type unification can get very slow because it requires to unify more holes than the case without eta expansion. is it worth trying to disable eta expansion of all records? I hope this does not break anything because in the proof relevant context, if Agda figures out two records are unified, the chances are they are the same record.
Consider the following:
Zero′ : Category o ℓ e
Zero′ = record
{ Obj = Lift o ⊥
; _⇒_ = λ _ _ → Lift ℓ ⊤
; _≈_ = λ _ _ → Lift e ⊤
; id = lift tt
; _∘_ = λ _ _ → lift tt
}
Zero′-⊥ : Initial
Zero′-⊥ = record
{ ⊥ = Zero′
; ! = record
{ F₀ = λ { (lift x) → ⊥-elim x }
; F₁ = λ { {A = lift () } }
; identity = λ { {A = lift () } }
; homomorphism = λ { {()} }
; F-resp-≈ = λ { {()} }
}
; !-unique = λ f → record
{ F⇒G = record { η = λ {()} ; commute = λ { {()} } }
; F⇐G = record { η = λ {()} ; commute = λ { {()} } }
; iso = λ ()
}
}which shows that Agda is just as happy with this definition of 'the' initial object of Cats. This feels vaguely suspicious. What am I missing?
bicategory ought to have triangle and pentagon equality as coherence conditions, according to https://ncatlab.org/nlab/show/bicategory. note that there is no such requirement for 2-category, because unitors and associator in 2-category are simply identities.
Consider porting all of the following:
The library should aim to be usable to those who do not make use of bleeding-edge Agda releases.
I found the definition is weird and realized that the adjoint functors need to be related by mates, so that the adjoint functors are actual "natural".
@andreasabel said (at 2d81933#r34263025) :
For the new categories library, did you consider using copattern matching instead of records? What is the policy for chosing one over the other?
Definition by copattern is more lazy, which might have a positive effect on the performance of Agda type-checking. Did you make some experiments?
I personally have not yet used copatterns in any code, so to use them right from the start of this library would have been a big jump. But I have been wanting to experiment with that in some of my code for Pi (the reversible programming language) and RigCategories, where this lazyness might be quite beneficial.
Having said that, as a user of the library, I definitely count on a lot of beta-reduction to happen (at least under C-u C-u C-c C-. ) to 'specialize' from general categorical stuff to the situation I am working in. Even in the categorical context, getting things like Categories/Functor/Instance/Discrete.agda to work. So really understanding exactly the lazyness of copatterns is very important.
As to the deepest question: is there a settled policy on record/copattern? I would say that there is not. I happen to like records - they match my mental picture of how this information should be captured. But I am definitely willing to be convinced. [Can't speak for @HuStmpHrrr ]
For example, the type-checking time of Categories/Category/Monoidal.agda and Categories/Category/Monoidal/Properties.agda is a bit sluggish. If judicious use of definitions by copatterns would help with that, that would be quite a valuable piece of information.
remove
levelOf : ∀ {o ℓ e} → Category o ℓ e → Level this function should go to stdlib.
similarly, Discrete, Slice and SubCategory?
these two definitions ought to be in Category.Construction. additionally, the modules should reexport Cone and Cocone to avoid redundant imports whenever Cones and Cocones are used.
agda-categories/Categories/Object/BinaryProducts.agda
Lines 82 to 86 in ab86789
Related to #35 .
So in branch Strict, I implemented a lot of Strict category theory, with a particular design in mind: That Category itself wouldn't be parametrized by an equality, but would use the surrounding propositional equality ≡ instead. Quite a lot of stuff can be defined. But eventually things "stop working". Here are some of them:
≡ doesn't quite work, as Functor contains functions, and we don't have extensionality. One can definitely define
_≡F_ : ∀ {o ℓ} {o′ ℓ′} {C : Category o ℓ} {D : Category o′ ℓ′} → (F G : Functor C D) → Set (ℓ′ ⊔ ℓ ⊔ o ⊔ o′)≡ 'on the nose'. Now, it's quite close, and one would hope to be able to define an eliminator from that data into ≡. Alas, as far as I can tell, that needs axiom K to work.≡ is again really hard without extensionality and without proof irrelevance. In other words, one needs to assume that the carrier is a set (in the HoTT sense of the word). This isn't so weird for Monoid. But for Cats (the category of categories) things get worse, and brings us back to _≡F_ : since Functors are not nicely 'equal', one needs to instead use (weak) Category that allows us to give a _≡_ parameter. Then things do work (but the proofs are painful).2-Category needs to use the weak definition of Enriched because the resulting Monoidal 2-Category Cats over which we enrich is weak.Functors Category can't really even be written down! It is supposed to be a strict category, but proving associativity (etc) requires equality of Natural Transformations, whose equality is even more difficult to write down properly (η is a function whose rhs is dependently typed).In other words, if the meta-theory is intensional, using propositional equality as a stand-in for "equality" for Strict categories just doesn't work. This is where CT seems to be very sensitive to its meta-theory, and its usual meta-theory is still haunted by set-theoretic, extensional thinking.
https://ncatlab.org/nlab/show/idempotent+monad
Seems to have all sorts of useful applications.
agda-categories/Categories/Bicategory.agda
Lines 148 to 149 in 68f0c99
whisker is in a wrong direction.
Toying with come copy of the old code, I finally encountered one problem: the definition of Monad doesn't go through without irrelevance, as least in the way it was defined in the old library. In particular, one gets the error
F₁ (Category.id C) != Category.id C of type
(C Category.⇒ F₀ (F₀ A)) (F₀ (F₀ A))
when checking that the expression μ ∘ʳ F has type
NaturalTransformation (F ∘F F ∘F F) (F ∘F F)
on the line
assoc : (μ ∘₁ (F ∘ˡ μ)) ≡T (μ ∘₁ (μ ∘ʳ F))Those two are, of course, "equal", but not definitionally equal.
I am completely convinced that Heterogeneous equality is not the solution. A different definition of the associativity law is probably the way to go. One that does not require that definitional equality as an intermediate step.
This is an issue for discussion about how the library should be design, from various aspects, including module structure and naming conventions. The overall principle should be to stay close with style guideline in standard library.
I propose that the libary should contain the following top level modules:
Object, which contains definitions of objects, e.g. initial and terminal objects, products, and exponentials.Morphism, which contains definitions of morphisms, e.g. epis and monos.Diagram, which contains definitions of diagram in a category, e.g. pullbacks and limits.Category, which contains definitions of various categories, e.g. monoidal category, bi-category and ccc.Functor, which contains definitions of various functors, e.g. hom functors, profunctors.NaturalTransformation, which contains definitions of natural transformations, e.g. natural isomorphisms.Adjoint, which contains definitions of adjoint functors, e.g. proadjoint.I suppose there will be needs for other top level modules, e.g. Algebra, Coalgebra. We can add more once there is a need.
Naming conventions should comply with standard library. For example, module names are usually singular, with the exception of the top level module Categories and Properties.
For variables, I propose following conventions.
A, B, C, D, X, Y, Z are for objects.f, g, h, i, a, b, c for morphisms.C, D, E are for categories. Clearly, the conventions for objects and categories collide. Sometimes it is not a problem, but when it does, I propose to use calligraphic letters 𝒞, 𝒟, ℰ, for categories. They can be input in emacs by \McC, \McD, \McE.F, G, H, I for functors.α, β, γ, η for natural transformations.When defining structures, I propose the names should match the idea of UMP. e.g. if it's a universality property, then it should be called universal; if it is a uniqueness property, then it should be called unique.
I believe _⟩∘⟨refl should have a different precedence than _⟩∘⟨_ and refl⟩∘⟨_ as I had some issues with agda struggling to parse expressions like ⟨ refl⟩∘⟨ something ⟩∘⟨refl ⟩ and since we want right associativity, _⟩∘⟨refl should have the higher precedence so I would propose changing it to a 5. For me, doing this little change made the quoted expression work in the end.
What do you think?
In the original library, there are many conclusions which make use of K. The same as stdlib, we can also have WithK submodules for those conclusions.
id-comm is defined in Categories.Category.Core as a definitional extension to a Category record.
Is that really where it belongs? It seems really out of place. Feels like it ought to be in Categories.Morphism, for example.
Also, almost all uses are actually of the 'other' version, so the code has a lot of Equiv.sym id-comm (in various guises) strewn around. That is quite ugly, so I think that ought to have its own name. But I reluctant to add it to the Category record.
Hi!
I just cloned and tried to load your library but I get the error:
.../agda-categories/Categories/Morphism/Isomorphism.agda:181,41-51
Function does not accept argument {i = _}
when checking that {i = _ ∼⁺⟨ [ f ] ⟩ [ g ]} {j = [ h ]} eq are
valid arguments to a function of type
{A B : Obj} → ≅⁺⇒⇒⁺ Preserves ≃⁺ ⟶ ≈⁺
Any idea why that might be and what I can do to make the library loadable?
Thank you!
The module Categories.Category.Construction.Graphs should be refactored.
The module currently contains
* basic definitions (graphs and their morphisms),
* the definition of the category of graphs,
* the functor mapping graphs to their free categories,
* an adjunction between the forgetful functor and the free functor,
* various helper/utility constructs and lemmas (e.g. path equality, etc.).
These should probably all go in separate modules. Some of the code should be moved to the standard library.
(See comments in the code for more details.)
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.