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

[Serge D. Mechveliani]

On Mon, Apr 08, 2013 at 01:01:19AM +0100, Arseniy Alekseyev wrote:
> [..]
> Your original type for
> 
>     Preserves2-3 : {a b lA : Level} {A : Set a} {B : Set b} ->
> [..]
> 
> 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.
> [..]

Great! It works. Thank you.
Also I expected that  Preserves2-3  can be nicely expressed via  
                                                            _Preserves_2.
And indeed, your provide such and expression via  uncurry, \o, and proj_1.  
I think, it is the nicest way.

Thanks,

------
Sergei