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

Arseniy Alekseyev arseniy.alekseyev at gmail.com
Mon Apr 8 02:01:19 CEST 2013

```{-

Dear Serge,

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
```