Agda 2.6.4 #9

With this Agda version there were changes [1] to instance resolution algorithm, from agda changelog: [Breaking] The algorithm for resolution of instance arguments has been simplified. It will now only rely on the type of instances to determine which candidate it should use, and no longer on their values. I've found this thread [2] at zulip, which might be helpful, but I don't know how to fix the issues at felix yet. [1] https://github.com/agda/agda/blob/master/doc/release-notes/2.6.4.md#language [2] https://agda.zulipchat.com/#narrow/stream/238741-general/topic/Issue.20with.20instance.20search.20changes.20in.202.2E6.2E4/near/384560563

This reverts commit 6df31ea.

Furthermore I've added explicit implicit ;) arguments to `Equivalent` fields. Those are actually important and it is impossible to follow hint that was stated in the `TODO` comment, that used to said: > TODO: move a and b arguments from methods to record. Without those implicit args, definitions like: ```agda ∘≈ : ∀ {f g : a ⇨ b} {h k : b ⇨ c} → h ≈ k → f ≈ g → h ∘ f ≈ k ∘ g ``` wouldn't typecheck as the `Equivalent` would lock it's variables during instantiation and we could use only those two (`a` & `b` in this case). `_≈_` would reject morphisms `h` & `k` here as it's objects would be different. There is additional `TODO` comment that says: > TODO: Replace Equivalent by Setoid? Actually moving variables mentioned above would almost turn Equivalent into Setoid (minus `Carrier` as a field). Which isn't really feasible for the reasons already mentioned. I've took a peek how agda-categoris does it [3] and they basically put `Equivalent` into definition of `Category` and call it _Setoid enriched_. I've played with that for a bit. Initially putting `_≈_` into lawful category. That didn't work out however because we need `_≈_` for defining different kinds homomorphisms, where we don't have lawful classes in scope. So I've moved it to the raw `Category`, but the problem with definitions that use multiple equalities still persists. I think that restricting the opening of `Category` class would be too cumbersome. So I think this split to `Equivalent` works nice. I do wonder however if it's worth doing the instance search, if most of the time one has to manually open appropriate one? I've also updated the readme to reflect supported versions. [3] https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Core.agda#L21

Turns out agda can infer proper Equivalent typeclass from the use of `_≈_`, based on the arguments. What is problematic are the implicit arguments to the `trans`, `sym` (and `refl`). But those are used in the proofs. I've noticed that agda-categories [1] put those operators inside their equivalent of `≈-Reasoning` which can (even have to) be opened independently of `Equivalent`. This way we can keep `Equivalent` open in `public` and enjoy nice definitions. What we need to do is a little extra work of opening `≈-Reasoning` with proper Equivalent instance as parameter. In order to signify the change standard functions were renamed: - refl to refl≈ - sym to sym≈ - trans to _;_ I didn't removed flipped trans (_•_) as there were some uses of it in the code. We can remove them separately if that'll be deemed necessary. [1] https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Core.agda#L90

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Agda 2.6.4 #9

Agda 2.6.4 #9

Commits on Feb 17, 2024