agda
Update definition of morphism equality in Setoids
Right now we use the definition of morphism equality from Function.Equality, which is slated for deprecation in the future (see https://github.com/agda/agda-stdlib/issues/1467). Furthermore, there's a very good reason it's not recommended: it's kind of hard to use!
As a refresher, we use the following definition for our equality (from Function.Equality:
_≈_ = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
This definition has the cong "baked in", which makes proofs a bit clumsy, as you end up proving f ⟨$⟩ x ≈₂ g ⟨$⟩ x then using cong with the x ≈₁ y proof to get the final result. This makes things far more fiddly then they have to, and has been impeding some of the cleanup of the implicit resolution mess found in #264.
I suggest we use the following definition, equivalent instead:
_≈_ = λ f g → ∀ x → f ⟨$⟩ x ≈₂ g ⟨$⟩ x
This should clean up a lot of code, and make dealing with Setoid a lot less of a hassle.
Thoughts?
I'm in favour of changing this. However, I think we should wait until the new Function.Structures/Bundles ecosystem has what we need, and switch wholesale to that when it's ready.
I'm in favour of changing this. However, I think we should wait until the new Function.Structures/Bundles ecosystem has what we need, and switch wholesale to that when it's ready.
Contributions that added to the new ecosystem exactly what you needed would be very welcome!
I suggest we use the following definition, equivalent instead:
_≈_ = λ f g → ∀ x → f ⟨$⟩ x ≈₂ g ⟨$⟩ x
Incidentally, this is the definition we use in Posets. so making this change would unify presentation too.
So I've done some experimentation with this, and I think we should go a step further. This does clean up a lot of stuff, but there are still places where things go sideways. For instance, there are a bunch of places where using Setoidsl.Equiv.refl ought to work, but we've computed too far, and inference falls over.
I think the way to go might be something like:
record _≗_ {c ℓ c′ ℓ′} {A : Setoid c ℓ} {B : Setoid c′ ℓ′} (f g : Func A B) : Set (c ⊔ ℓ′) where
constructor funext
field
pointwise : ∀ x → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ x)
This would prevent us from computing away what setoids we are working with + what the morphisms are, with the cost of having to write funext and pointwise in a bunch of places.
I'm not 100% sold on this, and it would be a decently large change, so I would love to hear opinions on this!
Great!
I think wrapping function equality is worth a try as this has helped in other places.
But if you've already implemented the other change, it might be worth submitting a PR with that first. As a checkpoint.
There's a related question that we should maybe start thinking about: since much of the library is based on setoids, if equality of setoid-maps becomes a record, should we introduce a hierarchy of bundles and structures for notions of equality that relate special types of setoid maps (e.g. functors, NTs, etc.)?
I like the idea of using a record to prevent computing away valuable information. Happy with the name of the record and with pointwise, but less so with funext. I prefer to keep that name for the axiom. funeq ? fun-≈ ?
I agree with submitting lots of incremental PRs (even if they might touch a lot of stuff).
@sstucki can you expand out what you mean in your 'related question'? I'm not grasping exactly what you mean.
I like the idea of using a record to prevent computing away valuable information. Happy with the name of the record and with
pointwise, but less so withfunext. I prefer to keep that name for the axiom.funeq?fun-≈?
What about ⌞_⌟ for the constructor? It's what we use for equivalence of isos and it doesn't add much syntactic noise. Of course if one mixes the two kinds of equality in the same module, there could be conflicts, but that's probably not very likely?
@sstucki can you expand out what you mean in your 'related question'? I'm not grasping exactly what you mean.
Well, it seems that we have similar problems with equalities of a number of structures (isos, natural transformations, setoid-maps, order morphisms) and in each case (unsurprisingly) the equation we wrap into a record is essentially a variant of function extensionality. Often (but not always) it's equality for setoid maps (rather than set maps) because everything is setoid-enriched. My point is simply that, since these are all instances of the same pattern, we could maybe make that explicit? For example, if we're redefining order morphisms to also be a record, then we might as well have a field (derived or real) that witnesses that an order morphism is also a setoid morphism. And similar for their equalities (two pointwise equal order morphisms have equal underlying setoid maps). And then one might as well check what other types of equalities are really setoid-map-equalities with extra structure (e.g. strict functor equality?) I don't know whether much is to be gained from that, honestly. It was just a stray thought.
The reason I didn't use that is that it doesn't play as nice with multiline proofs. For instance, it's very easy to just do
fun-eq λ x →
let someStuff = ...
in someVeryBigThing
The ⌞_⌟ is very cute, but I think for this case something that isn't mixfix is for the best.
The
⌞_⌟is very cute, but I think for this case something that isn't mixfix is for the best.
Makes sense.
these two laws are subtly different. the other one cannot prove the first one. is there any case to motivate the other one?
these two laws are subtly different. the other one cannot prove the first one.
I think they should be equivalent. Because of transitivity. We use similar laws for Posets and these are all degenerate cases of natural transformations/isos.
As for why one is easier to use than the other, I'll let @TOTBWF answer that.
that sounds to me Posets has the wrong definition then. the latter looks a stricter law than the former so the definition would work., but this definition should fail for some laws for Posets consider two sets S and T, where S has two distinct elements a and b, and T has c and d. then we have a function f defined by f(a) = c and f(b) = d. If we let a and b equivalent but keep c and d distinct, then f is not a setoid homomorphism, but admits this law.
after inspection, it turns out that PosetHomomorphism is setoid homomorphic according to the fomer law already, so indeed transitivity can kick in. but this is not generally the case for setoids.
that sounds to me
Posetshas the wrong definition then. the latter looks a stricter law than the former so the definition would work., but this definition should fail for some laws forPosetsconsider two setsSandT, whereShas two distinct elementsaandb, andThascandd. then we have a functionfdefined byf(a) = candf(b) = d. If we letaandbequivalent but keepcandddistinct, thenfis not a setoid homomorphism, but admits this law.
I'm not sure I understand. These are definitions of morphism equality not of being a homomorphism. Of course if something is not a morphism, then the definition does not apply.
If you have two setoid/poset morphisms f, g: A -> B, then, for any x = y in A
f(x) = g(x) = g(y)
where the first step is by the short definition of morphism equality and the second step is by monotonicity/functoriality of g. So the longer definition can be derived from the shorter one.
Am I missing something?
i suppose the issue is about the deifnition of Setoids. The category of setoids requires the morphisms to be homomorphic, so the current definition is correct. if we switch to the proposed law, it will be some category, but not the category of setoids.
as for Posets, one can do that because poset homomorphisms are defined to be setoid homomorphisms, which indeed takes the shortcut. in setoids, g(x) = g(y) doesn't necessarily hold in general, as given by my counterexample.
The two definitions are indeed equivalent.
import Relation.Binary.Reasoning.Setoid as SR
module _ {c ℓ} {A B : Setoid c ℓ} (f g : A ⟶ B) where
module A = Setoid A
module B = Setoid B
new⇒old : (∀ {x} → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ x)) → Setoid._≈_ (A ⇨ B) f g
new⇒old pointwise {x} {y} x≈y = begin
f ⟨$⟩ x ≈⟨ pointwise ⟩
g ⟨$⟩ x ≈⟨ cong g x≈y ⟩
g ⟨$⟩ y ∎
where
open SR B
old⇒new : Setoid._≈_ (A ⇨ B) f g → (∀ {x} → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ x))
old⇒new eq = eq A.refl
The way we were using this equality is proving the f x = g x case, then throwing in a bunch of congs.
The example you are discussing would be a problem, but we can't even define it as a morphims in Setoid to begin with!
X : Setoid 0ℓ 0ℓ
X = record
{ Carrier = Bool
; _≈_ = λ _ _ → ⊤
; isEquivalence = record
{ refl = tt
; sym = λ x → tt
; trans = λ x x₁ → tt
}
}
Y : Setoid 0ℓ 0ℓ
Y = Eq.setoid Bool
foo : X ⟶ Y
foo = record
{ _⟨$⟩_ = λ { true → true; false → false }
; cong = λ { {false} {false} tt → {!!}
; {false} {true} tt → {!!} -- Goal here is false ≡ true
; {true} {false} tt → {!!}
; {true} {true} tt → {!!}
}
}
yes, I realized that. thx for your explanation. indeed, cong here is the kicker.
What's the status of this? Has a PR been done on stdlib? Should it be?
This all seems like the right way to go, BTW. I might finally be in a position to help too.
IIRC it was somewhat unclear what the plans were in the stdlib for the new function hierarchy. Could be misremembering though!
I think the plans are now clear. See https://github.com/agda/agda-stdlib/issues/759#issuecomment-526791198 .