Add antisym-≡ to Data.Vec.Relation.Binary.Pointwise.Inductive

[Taneb]

By analogy to what exists in, for example, Relation.Binary.Construct.Add.Infimum.NonStrict.

Something similar could also be added to Data.Vec.Relation.Binary.Pointwise.Extensional

[gallais]

This feels like a consequence of antisym and the fact that pointwise propositional
equality is equivalent to propositional equality.

[jamesmckinna]

This feels like a consequence of antisym and the fact that pointwise propositional equality is equivalent to propositional equality.

Fairbairn threshold?

[Taneb]

This composes better if you're using nested Pointwise than combining antisym and Pointwise-≡⇒≡.

Compare:

foo : ∀ {a ℓ m n} {A : Set a} {P : Rel A ℓ} → Antisymmetric _≡_ P → Antisymmetric _≡_ (Pointwise (Pointwise P {n}) {m})
foo antisym = Pointwise.antisym-≡ (Pointwise.antisym-≡ antisym)

bar : ∀ {a ℓ m n} {A : Set a} {P : Rel A ℓ} → Antisymmetric _≡_ P → Antisymmetric _≡_ (Pointwise (Pointwise P {n}) {m})
bar antisym a b = Pointwise.Pointwise-≡⇒≡ (Pointwise.antisym (λ c d → Pointwise.Pointwise-≡⇒≡ (Pointwise.antisym antisym c d)) a b)

That said, I realised as I was writing that that the lambdas were unnecessary with Function.Base._∘₂_:

baz : ∀ {a ℓ m n} {A : Set a} {P : Rel A ℓ} → Antisymmetric _≡_ P → Antisymmetric _≡_ (Pointwise (Pointwise P {n}) {m})
baz antisym = Pointwise.Pointwise-≡⇒≡ ∘₂ Pointwise.antisym (Pointwise.Pointwise-≡⇒≡ ∘₂ Pointwise.antisym antisym)

But while that's a better way to do this than what I was doing, I still think adding this is worth it.

---

I initially implemented this directly to avoid reordering the module. Pointwise-≡⇒≡ is defined almost right at the end, and I wanted antisym-≡ to remain near antisym. I don't think it would be that bad to move the Pointwise _≡_ is equivalent to _≡_ proofs earlier in the module, though. If we conclude that this does pass the Fairbairn threshold after all, then I'll do that and redefine antisym-≡ accordingly.

[jamesmckinna]

I think that moving code is always OK, so long as the dependency order is respected, and I certainly agree with wanting the keep any definition of antisym-≡ spatially near to that of antisym.

As for Fairbairn, for sure I felt obliged to raise the question, but I'd be OK with adding this lemma.