Why does equality of Function Setoids have cong baked in?

[TOTBWF]

Right now, we define function setoids as follows (taken from Function.Equality):

setoid : ∀ {f₁ f₂ t₁ t₂}
         (From : Setoid f₁ f₂) →
         IndexedSetoid (Setoid.Carrier From) t₁ t₂ →
         Setoid _ _
setoid From To = record
  { Carrier       = Π From To
  ; _≈_           = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
  ; isEquivalence = record
    { refl  = λ {f} → cong f
    ; sym   = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
    ; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
    }
  }
  where
  open module From = Setoid From using () renaming (_≈_ to _≈₁_)
  open module To = IndexedSetoid To   using () renaming (_≈_ to _≈₂_)

If we look at the definition of _≈_, we can see that it has cong baked into it. This makes working with these equalities awkward, as you essentially perform a proof that f ⟨$⟩ x ≈₂ g ⟨$⟩ x, then perform a cong at the very end to get that g ⟨$⟩ x ≈₂ g ⟨$⟩ y. It seems like the following equivalent definition would be a bit easier to work with:

setoid : ∀ {f₁ f₂ t₁ t₂}
         (From : Setoid f₁ f₂) →
         IndexedSetoid (Setoid.Carrier From) t₁ t₂ →
         Setoid _ _
setoid From To = record
  { Carrier       = Π From To
  ; _≈_           = λ f g → ∀ x → f ⟨$⟩ x ≈₂ g ⟨$⟩ x
  ; isEquivalence = record
    { refl  = λ {f} _ → To.refl
    ; sym   = λ f∼g x → To.sym (f∼g x)
    ; trans = λ f∼g g∼h x → To.trans (f∼g x) (g∼h x)
    }
  }
  where
  open module From = Setoid From using () renaming (_≈_ to _≈₁_)
  open module To = IndexedSetoid To   using () renaming (_≈_ to _≈₂_)

Thoughts?

[MatthewDaggitt]

Hi @TOTBWF, yup agreed these definitions are super-hard to work with. Because of that, we're in the process of trying to define a more useable function hierarchy (see Function.Structures/Bundles) and deprecate Function.Equality and similar files. It should probably be more noticeable, but at the top of the file is the following note pointing in this direction:

agda-stdlib/src/Function/Equality.agda

Line 9 in bc9c1b6

-- Note: use of the standard function hierarchy is encouraged. The

As of yet, we don't have either the construction of the function setoid or a dependant functions in the new function hierarchy. The former should probably live in Function.Relation.Binary.Pointwise. Do you explicitly need the dependent version?

[TOTBWF]

Good to know about the imminent deprecation! I stumbled across this when I was doing some stuff in agda-categories with the category of Setoids, we use it there for morphism equality. AFAIK we only need the non-dependent version, and if push comes to shove it's pretty easy to roll by hand.

[Taneb]

The main thing that's missing from the new Function.Structures/Bundles, as I see it, is a notion of equality of functions, analogous to Function.Equality.setoid in the old style. I'm not sure where this should live or how it should look, however.

[MatthewDaggitt]

I'm not sure where this should live or how it should look, however.

Well the principled place would be Function.Relation.Binary.Pointwise and Function.Relation.Binary.Equality...

[JacquesCarette]

Working on it. I'm first changing all of agda-categories to use the 'simpler' definition of setoid (as above). It requires a lot more changes than I expected (largely good). Then I'll submit a PR here - that way I'll know the definition will have been "battle tested" quite thoroughly.