`Monotonicity` implies `Congruence` for `Antisymmetric` orderings

[jamesmckinna]

An IsOrderHomomorphism

agda-stdlib/src/Relation/Binary/Morphism/Structures.agda

Lines 60 to 66 in 54f5c38

	record IsOrderHomomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
	(_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
	(⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
	where
	field
	cong : Homomorphic₂ _≈₁_ _≈₂_ ⟦_⟧
	mono : Homomorphic₂ _≲₁_ _≲₂_ ⟦_⟧

between partial orders is necessarily congruent, by virtue of monotonicity (and antisymmetry on the codomain)?

So: should we have a Relation.Binary.Morphism.Biased.Structures definition to reflect that? How best (eg wrt parametrisation) to define it?

[jamesmckinna]

Ach! This is

agda-stdlib/src/Relation/Binary/Consequences.agda

Lines 88 to 92 in 54f5c38

	mono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
	∀ {f} → Monotonic₁ ≤₁ ≤₂ f → Monotonic₁ ≈₁ ≈₂ f
	mono⇒cong sym reflexive antisym mono x≈y = antisym
	(mono (reflexive x≈y))
	(mono (reflexive (sym x≈y)))

... which I wrote so chalk one up to brain-fade... sigh.