Setoid instances

[jkopanski]

Following discussion we had last week I've started to define those
instances and it occurred to me that they would make nice addition to
the base library.

I've removed requirement for Products (Set q) instance from lawful
CartesianClosed. It seems it wasn't used anywhere and I didn't know
what that would be here.

Provided instances quantify Levels individually as they're different
for different typeclasses. Quantifiyng that at the module level would
mean that we wouldn't be able to substitute it differently. For
example: Products can use Setoid c ℓ as obj. But
Exponentials require that obj is Setoid (c ⊔ ℓ) (c ⊔ ℓ), which
in turns requires Products for the same obj. Fixing c and ℓ
at the module would prohibit Exponentials to get required
Products.

One module (Function.Construct.Setoid) was copied from
agda-categories, and there it was copied from old standard library, as
it got removed from the 2.0 version.

Last commit is my attempt at defining Traced, but I can't quite get it
work. See the commit comment.

[conal]

Thanks, Jakub! I think we will need this category.

[conal]

I've removed requirement for Products (Set q) instance from lawful
CartesianClosed. It seems it wasn't used anywhere and I didn't know
what that would be here.

Great. Perhaps this constraint was needed at one time and then no longer.

[conal]

Provided instances quantify Levels individually as they're different
for different typeclasses. Quantifiyng that at the module level would
mean that we wouldn't be able to substitute it differently. For
example: Products can use Setoid c ℓ as obj. But
Exponentials require that obj is Setoid (c ⊔ ℓ) (c ⊔ ℓ), which
in turns requires Products for the same obj. Fixing c and ℓ
at the module would prohibit Exponentials to get required
Products.

:D !

[conal]

One module (Function.Construct.Setoid) was copied from agda-categories, and there it was copied from old standard library, as it got removed from the 2.0 version.

Where was this functionality in the pre-2.0 agda-stdlib?

[jkopanski]

One module (Function.Construct.Setoid) was copied from agda-categories, and there it was copied from old standard library, as it got removed from the 2.0 version.

Where was this functionality in the pre-2.0 agda-stdlib?

I think it was Function.Equality.⇨.

[jkopanski]

Provided instances quantify Levels individually as they're different
for different typeclasses. Quantifiyng that at the module level would
mean that we wouldn't be able to substitute it differently. For
example: Products can use Setoid c ℓ as obj. But
Exponentials require that obj is Setoid (c ⊔ ℓ) (c ⊔ ℓ), which
in turns requires Products for the same obj. Fixing c and ℓ
at the module would prohibit Exponentials to get required
Products.

:D !

does that mean my explanation is incomprehensible? I don't know what you mean by that smiley

[conal]

One module (Function.Construct.Setoid) was copied from agda-categories, and there it was copied from old standard library, as it got removed from the 2.0 version.

Where was this functionality in the pre-2.0 agda-stdlib?

I think it was Function.Equality.⇨.

Thank you! That's the definition I was trying to remember. Do you have any idea why it was removed?

[jkopanski]

One module (Function.Construct.Setoid) was copied from agda-categories, and there it was copied from old standard library, as it got removed from the 2.0 version.

Where was this functionality in the pre-2.0 agda-stdlib?

I think it was Function.Equality.⇨.

Thank you! That's the definition I was trying to remember. Do you have any idea why it was removed?

I was trying to look up the relevant agda-categories commit history in hopes to figure out more. I know nothing for sure but my guess it was just forgotten.

Note that Jacques already opened this as an stdlib PR with v2.1 tag.

[conal]

:D !

does that mean my explanation is incomprehensible? I don't know what you mean by that smiley

I meant I liked what you did.

[conal]

There are a lot of opportunities to use standard categorical operations here. Did you consider doing so?

[jkopanski]

There are a lot of opportunities to use standard categorical operations here. Did you consider doing so?

Not really, it was mostly mechanistic translation from Function instances. I do however think that might be the case to cracking Traced as it would perhaps allow me to not reference directly the value that comes from well foundedness and instead do the same operation on the both sides of equality.

What did occur to me after this is that Func.to is homomorphism into Function, and that could be used to transfer properties

[jkopanski]

There are a lot of opportunities to use standard categorical operations here. Did you consider doing so?

I've tried this exercise and it blew my mind ;) see, comments attached to a related commit: 78e655a

[conal]

There are a lot of opportunities to use standard categorical operations here. Did you consider doing so?

I’ve tried this exercise and it blew my mind ;) see, comments attached to a related commit: 78e655a

Terrific! It sounds like you’re having the experience I hoped you would. Start with poetic rephrasings, see what new hints appear, and follow where the beauty seems to lead.

[conal]

What did occur to me after this is that Func.to is homomorphism into Function, and that could be used to transfer properties

For properties to transfer, equivalence on the homomorphism’s source must be defined as equivalence of homomorphic images. When the homomorphism maps representations to their meanings, this definition of equivalence is necessary (I think) for non-leaky abstraction. What notion or notions of morphism equivalence make sense in a Setoid category?

[conal]

From commit 78e655a:

This has completely stunned me. Law for the categorical operator holds by the definition of this operator in different category! I find it amazing!

I’m glad that you found this surprise yourself and that you enjoy the gift! I’ve stumbled onto such homomorphic gems often enough that I now know to dig for them. Finding them in logic/proofs is even more satisfying than in implementations, further rewarding the switch from Haskell to Agda.

[jkopanski]

What did occur to me after this is that Func.to is homomorphism into Function, and that could be used to transfer properties

For properties to transfer, equivalence on the homomorphism’s source must be defined as equivalence of homomorphic images. When the homomorphism maps representations to their meanings, this definition of equivalence is necessary (I think) for non-leaky abstraction. What notion or notions of morphism equivalence make sense in a Setoid category?

IIUC that is exactly the case for equivalence in category of setoids: ∀ x → to f x ≈ to g x. Ok now that I've pasted this in, it is not exactly the case, as in both categories we pointwise equality and it's not exact. So it should be rewritten in terms of _≈_ from Equivalent for function instance?

[conal]

IIUC that is exactly the case for equivalence in category of setoids: ∀ x → to f x ≈ to g x. Ok now that I've pasted this in, it is not exactly the case, as in both categories we pointwise equality and it's not exact. So it should be rewritten in terms of _≈_ from Equivalent for function instance?

If we want equational properties (laws etc) to transfer backward through to in the standard homomorphic way, I think we’d have to define _≈_ = _≈_ on to, i.e., f ≈ g = to f ≈ to g, i.e., f ≈ g = ∀ x → to f x ≡ to g x. (You might enjoy reading through Relation.Binary.Construct.On if you haven’t already.) This _≈_ definition doesn’t, however, match the intent of Setoid.

An alternative is to use a homomorphism going the other way: specify the function category (“Set”) via a homomorphism to the setoid category rather than vice versa.

[conal]

How tidy could these definitions become if rewritten via the categorical vocabulary?

[jkopanski]

oh, I took me way too long to notice, still can't replace cong one as I can't guide Agda to pick proper instances, which I myself don't know in full details. I was hoping agda would figure it out. All I see is the pattern for distribl/r

[jkopanski]

Ok, the issue here is that constructors (inj₁/inj₂) used at cong are coming from Pointwise and we don't have any category instance that would use this as coproducts*. I've tried using map from that module but I have trouble convincing Agda is complaining about stuff that I don't know how to solve.

• What would that category be? Category of REL A C? This one?

[conal]

Ok, the issue here is that constructors (inj₁/inj₂) used at cong are coming from Pointwise [...]

I don't know, and I like this question a lot! If we come up with a good answer, this whole Setoid category might come out beautifully.

[conal]

Note that categorical products and coproducts in Rels are necessarily (isomorphic to) sum types.

[conal]

How pretty could these proofs look if expressed via categorical vocabulary?

[jkopanski]

basically variation of the (Setoid.refl ▿ Setoid.refl) ∘ exr but the level inference for proper categorical instances are killing me

[conal]

This one feels a little off to me. How about you?