copumpkin / categories Goto Github PK
View Code? Open in Web Editor NEWCategories parametrized by morphism equality, in Agda
License: Other
Categories parametrized by morphism equality, in Agda
License: Other
This library is **obsolete** and does not work with newer versions of Agda. It sort-of works with 2.5.2, but less and less so afterwards. It is completely broken from 2.6 onwards. Users should instead try https://github.com/agda/agda-categories. It is not completely compatible, but close. And it is supported. ---------------------------------------------------------------------------------------------------------------------------------- One of the main goals of this library is to be as general as possible by abstracting over notions of equality between morphisms. Another is to keep the definitions of categorical structures as simple as possible and then where possible to prove that the simple definition is equivalent to more interesting formulations. For example, we can define a monad as recording containing a functor and two natural transformations. Separately, we can show that a monoid object in the monoidal category of endofunctors is an equivalent definition, and that the composition of an adjoint pair of functors leads to monads, and so on. The module structure is a mess, I realize. A lot of the parametrized modules should not be. Naming of things in general could also be made cleaner, but I've been more interested in definitions and proofs so far. A lot of this is based on http://web.student.chalmers.se/~stevan/ctfp/html/README.html, but with some design changes that I thought were necessary. It's still very much a work in progress. Other parts (mostly produts) are borrowed from Dan Doel
Categories/Lift.agda & Categories/Support/Equivalence.agda are affected
assoc = A.assoc , B.assoc
is the first problematic line. Didn't investigate it any further yet
In particular Categories.NaturalIsomorphisms does not build (the very last line of my-iso is no longer well-formed).
There seems to be issues with Categories.Morphisms.Iso as well, but I believe I've dealt with those (in my fork).
More specifically, I am currently getting
/Users/carette/Agda/categories/Categories/NaturalIsomorphism.agda:213,3-18
Functor.F₀ F₁ x != w of type D.Obj
when checking that the type
(F₁ : Functor C D) (x₁ : C.Obj) (w : D.Obj) (G₁ : Functor C D)
(F≡G₁
: {A B : C.Obj} (f : A C.⇒ B) → Functor.F₁ F₁ f ∼ Functor.F₁ G₁ f)
(G≡F₁
: {A B : C.Obj} (f : A C.⇒ B) →
Functor.F₁ G₁ f ∼ Functor.F₁ F₁ f) →
(.Categories.NaturalIsomorphism...my-η {.o} {.ℓ} {.e} {.o′} {.ℓ′}
{.e′} {C} {D} F G F≡G F₁ G₁ F≡G₁ x₁
| w | Functor.F₀ G₁ x₁ | oneway-helper (F≡G₁ C.id))
D.∘
(.Categories.NaturalIsomorphism...my-η {.o} {.ℓ} {.e} {.o′} {.ℓ′}
{.e′} {C} {D} F G F≡G G₁ F₁ G≡F₁ x₁
| Functor.F₀ G₁ x₁ | w | oneway-helper (G≡F₁ C.id))
D.≡ D.id
of the generated with function is well-formed
where 'oneway-helper' is my short name for the "helper" function buried under oneway (just to make debugging easier). I am quite willing to help, I am just rather stuck at the moment.
/tmp/nix-build-categories-33409120d071656f5198c658145889ae2e86249c.drv-0/categories-3340912/Categories/Morphism/Indexed.agda:54,15-57
Xs IxOb.! .i != (B IxOb.! Xs) .i of type S
when checking that the expression
≣-cong (P.uncurry _⇒_ ⋆′ F) (cong₀ Xs i≈j) has type
my-Carrier .i ≣ my-Carrier .j
builder for ‘/nix/store/wgp5ilsf16y3c0ng70p0mcdbr575qfv4-categories-33409120d071656f5198c658145889ae2e86249c.drv’ failed with exit code 1
error: build of ‘/nix/store/wgp5ilsf16y3c0ng70p0mcdbr575qfv4-categories-33409120d071656f5198c658145889ae2e86249c.drv’ failed
Bar
In 2.5.4.2, horizontal composition of natural transformations doesn't compile anymore, due to failure of inference of metavariables. I am not sure whose problem it is. Any chance you can take a look?
line 60, unsolved implicit arguments to flattenPⁿ
Seem be the of the same kind as #19 and related to inability to infer composition
I don't know is this type checker behaviour correct. The documentation states:
By default, all (inductive) record types enjoy eta-equality if the positivity checker has confirmed it is safe to have it. The keywords eta-equality/no-eta-equality enable/disable eta rules for the record type being declared.
But without eta-equality keyword
Category.op (Category.op c) ≢ c
and same for Functor.
For example this breaks DinaturalTransformation.agda
It needs hiding.
Affected files are
Categories/Object/BinaryProducts/N-ary.agda
Categories/Object/Products/N-ary.agda
I am wondering how far is it to resolve the incompatibilities of this library to up-to-date agda?
Agda has reached 2.6 and I am eager to try in near future but I am not sure how far is it for this library to be ready.
Finished Categories.Discrete.
Checking Categories.End (/tmp/nix-build-categories.drv-0/git-export/Categories/End.agda).
Checking Categories.DinaturalTransformation (/tmp/nix-build-categories.drv-0/git-export/Categories/DinaturalTransformation.agda).
/tmp/nix-build-categories.drv-0/git-export/Categories/DinaturalTransformation.agda:39,24-25
No variable of type
ClimbBuilder (_Y_287 eta alpha f) (_Z_288 eta alpha f)
(_S_290 eta alpha f)
was found in scope.
when checking that (H.F₁ (f , C.id))
((η (c′ , c′) ∙ α c′) ∙ F.F₁ (C.id , f)) are valid arguments to a
function of type
({X Y Z : Obj} {s : Level} {S : Set s}
{{Sb : ClimbBuilder Y Z S}} →
S →
{t : Level} {T = T₁ : Set t} {{Tb : ClimbBuilder X Y T₁}} →
T₁ → Climb X Z)
builder for `/nix/store/80v6hmj6ng5gr4dl99zwgrsrz5g1996s-categories.drv' failed with exit code 1
error: build of `/nix/store/80v6hmj6ng5gr4dl99zwgrsrz5g1996s-categories.drv' failed
Relation.Binary.Indexed does not exist anymore
I've been constructing some categorical stuff using this library.
One of these constructions is the delay monad using sized types in the category Categories.Agda.ISetoids
.
For now it is part of an external development; but if you are interested I could prepare a PR.
Let me know and thanks for all the proofs!
I get
Checking Categories.Equivalence.Strong (/afs/csail.mit.edu/u/j/jgross/category-coq-experience-tests/copumpkin/categories/Categories/Equivalence/Strong.agda).
/afs/csail.mit.edu/u/j/jgross/category-coq-experience-tests/copumpkin/categories/Categories/Equivalence/Strong.agda:29,29-30
(Category o′ ℓ′ e′) !=< (Iso (_C_147 x) (_f_150 x) (_g_151 x))
of type (Set (suc e′ ⊔ (suc ℓ′ ⊔ suc o′)))
when checking that the expression D has type
Iso (_C_147 x) (_f_150 x) (_g_151 x)
Affected file is Categories/Support/ZigZag.agda
Hello!
I tried loading your library with agda 2.5.2 but I got this error:
.../categories/Categories/Power.agda:163,1: Parse error
overlap
: ∀ {D E} (H : Bifunctor D D ...
It's very weird as it looks completely innocuous.
Are you aware of this? Do you have any idea as to what might be causing it?
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 is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
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.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.