[Agda] congruence, Preserves_2

[Serge D. Mechveliani]

On Mon, Sep 10, 2012 at 10:21:40AM +0200, Andreas Abel wrote:
>
>
> On 08.09.12 8:38 PM, Serge D. Mechveliani wrote:
[..]
>>   proo : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
>>   proo m n p =  ?
>>
>> (for this letter I replace
>>       \bn -> Nat,  _\equiv_ -> ==,  _\~~_ -> ~~,  \. -> op,  \_2 -> _2,
>> ).
[..]
>>   proo m n p =  cong (_+_ m) p
[..]
>> II. In a general situation, one probably needs to apply  op-cong  from
>>      Semigroup. I tried this approach for Nat.
>> [..]
>> proo m n p =  +cong <what to set here ?>
>>    where
>>    isCSemir  = NatProp.isCommutativeSemiring
>>    [..]
>>    +cong : _+_ Preserves_2 == -> == -> ==        -- what must be here?
>>    +cong = IsCommutativeMonoid.op-cong +isComMon
[..]
>> "Could not parse the application _+_ Preserves_2 ==
>>   when scope checking _+_ Preserves_2 ==


> I think you could start trying _==_ instead of ==.

As a wrote above,   ==  stands for  _\equiv_   

for this letter, and probably you mean the same.

Improvement for this report:
it is better to put          \equiv -> ==,  
and, respectively:

  proo : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
  proo m n p =  +cong <what to set here ?>
    where
    isCSemir  = NatProp.isCommutativeSemiring
    +isComMon = IsCommutativeSemiring.+-isCommutativeMonoid isCSemir
    +comm = IsCommutativeMonoid.comm  +isComMon -- Commutative _==_ _+_

    +cong : _+_ Preserves_2 _==_ -> _==_ -> _==_  -- what must be here?
    +cong = IsCommutativeMonoid.op-cong +isComMon

"Could not parse the application _+_ Preserves_2 _==_
 when scope checking _+_ Preserves_2 _==_   

a) What is the type of this  +cong ?
b) For the value    ``+cong = IsCommutativeMonoid.op-cong  +isComMon'',
   can Agda itself show the type of  +cong  ?
c) What to set in the RHS of   proo m n p =  ...   ?

Thanks,

------
Sergei