[Agda] Respects2 in IsPreorder is derivable

[kahl at cas.mcmaster.ca]

Is there a particular reason why IsPreorder in
the standard library module Relation.Binary
includes  ∼-resp-≈  as a field,
although it is easily derivable from the other fields?


Wolfram


{-# OPTIONS --universe-polymorphism #-}

module Relation.Binary.Preorder where

open import Data.Product
open import Function
open import Level
open import Relation.Binary.Consequences
open import Relation.Binary.Core hiding (refl)
open import Relation.Binary

record IsPreorder' {a ℓ₁ ℓ₂} {A : Set a}
                  (_≈_ : Rel A ℓ₁) -- The underlying equality.
                  (_∼_ : Rel A ℓ₂) -- The relation.
                  : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isEquivalence : IsEquivalence _≈_
    -- Reflexivity is expressed in terms of an underlying equality:
    reflexive     : _≈_ ⇒ _∼_
    trans         : Transitive _∼_

  ∼-resp-≈ : _∼_ Respects₂ _≈_
  ∼-resp-≈ =    ( λ x≈y z∼x → trans z∼x (reflexive x≈y) )
              , ( λ x≈y x∼z → trans (reflexive (IsEquivalence.sym isEquivalence x≈y)) x∼z )

  isPreorder : IsPreorder _≈_ _∼_
  isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive = reflexive
    ; trans = trans
    ; ∼-resp-≈ = ∼-resp-≈
    }

  module Eq = IsEquivalence isEquivalence

  refl : Reflexive _∼_
  refl = reflexive Eq.refl