[Agda] Preserves-by-2-of-3
Arseniy Alekseyev
arseniy.alekseyev at gmail.com
Mon Apr 8 02:01:19 CEST 2013
{-
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
More information about the Agda
mailing list