[Agda] Preserves-by-2-of-3

[Arseniy Alekseyev]

{-

Dear Serge,

Your original type for

    Preserves2-3 : {a b lA : Level} {A : Set a} {B : Set b} ->
               (f : (x y : A) → B -> A) → Rel A lA → Set (lA ⊔ (b ⊔ a))

is not dependent enough. Specifically, you need to have `B` depend on
the value of `y`. I changed the type of `B` to `A → Set b` and instantiated it
accordingly.

I've additionally declared `Cong-Foo'`, which is logically
equivalent to `Cong-Foo`, but may or may not be simpler to work with.

Cheers!
Arseniy

-}

module t2 where

open import Level using (Level; suc; _⊔_)
open import Relation.Nullary.Core using (¬_)
open import Relation.Binary using (Rel; _Preserves₂_⟶_⟶_)
open import Algebra using (Monoid; module Monoid)

Preserves2-3 : {a b lA : Level} {A : Set a} {B : A → Set b} ->
               ((x y : A) → B y -> A) → Rel A lA → Set (lA ⊔ (b ⊔ a))
-- "Preserves by first 2 arguments of 3".
Preserves2-3 {_} {_} {_} {A} {B} f _≈_ =
             {x y x' y' : A} -> {z : B y} {z' : B y'} ->
             x ≈ x' → y ≈ y' -> (f x y z) ≈ (f x' y' z')

open import Data.Product
open import Function

record Foo (c l : Level) (M : Monoid c l) : Set (suc (c ⊔ l))
  where
  open Monoid M renaming (Carrier to C)
  field
    foo : (x y : C) -> ¬ y ≈ ε -> C

  Cong-Foo = Preserves2-3 foo _≈_

  Cong-Foo' = (uncurry ∘ foo) Preserves₂ _≈_ ⟶ _≈_ on proj₁ ⟶ _≈_

  to : Cong-Foo → Cong-Foo'
  to f = f
  from : Cong-Foo' → Cong-Foo
  from f = f

  field
    cong-foo : Cong-Foo