copumpkin / categories Goto Github PK

assoc = A.assoc , B.assoc

is the first problematic line. Didn't investigate it any further yet

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?

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?

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.

It needs hiding.

Affected files are

Categories/Object/BinaryProducts/N-ary.agda
Categories/Object/Products/N-ary.agda

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

Bar

Categories/Lift.agda & Categories/Support/Equivalence.agda are affected

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

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.

Relation.Binary.Indexed does not exist anymore

line 60, unsolved implicit arguments to flattenPⁿ

Seem be the of the same kind as #19 and related to inability to infer composition

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!