[Agda] congruence on dependent types

[Sergei Meshveliani]

We wrote

>> I knew the meaning of dotted patterns, but decided to avoid them --
>> while possible, and see further. I have forgotten of them, and now 
>> was
>> not able to use them in this concrete example.
>>
>> Further, I have a feeling that something is strange in the Language.
>> Suppose that a type
>>                      Foo a
>>
>>   depends on  a : C,  A : Setoid,  C = Carrier A,
>>   the equivalence  p : a \~~ b   is proved,
>>   f : Foo a  is built,
>>   and we need to return  f : Foo b,
>>   and also somehow to express that  f : Foo a  can be replaced with
>>   f : Foo b    if  a \~~ b.
>>
>> Can this be expressed in Agda ?

> No, you can't prove this for any dependent type `Foo`. If it is true 
> in your particular case, you will need to prove it specifically for 
> that.
>
> To see why it's not true in general, pick any `a : C`, and define
>
>    Foo : C → Set
>    Foo x = a ≡ x
>
> Now, if you had:
>
>    cong≈ : (a ≈ b) → Foo a → Foo b
>
> you could prove:
>
>    discr : (b : C) → a ≈ b → a ≡ b
>    discr b p = cong≈ p refl
>
> which, abstracted on `a`, would imply that `A` is discrete.


There remains a certain deviation of Agda from mathematics. 
Consider the example. 
For a  CommutativeMonoid M,  an element  a ∈ M,  
call a  p-Subsemigroup  <a>   in  M  a semigroup of the set 
                                                 {x ∙ a | x ∈ M}.                                                      Hence  <a> and
Hence  <a> and <b>  is the same p-subsemigroup in M  iff  
                                                  associated a b  
  where 
  associated a b =  ∃₂ λ (x y : C) →  (x ∙ a) ≈ b  ×  (y ∙ b) ≈ a
  
  -- that is  a  and  b  divide each other. 

Hence, if  assoc-a-b : associated a b,  then   f ∈ <a>  
can be replaced with                           f ∈ <b>
in a mathematical proof.

Now, it is desirable for an  algebraic domain  to be expressed in Agda as a
_dependent type_.  Respectively,  f ∈ <a>  need to correspond to  f : PSSmg a,
where  PSSmg a  is the type expressing  <a>.

I can express in Agda the  Set of all  p-subsemigroups in M,  and the equality
_=pss_  on this set,  with  _=pss_  defined via   associated a b.
But for  p : associated a b  the  type checker  will not allow to replace   
f : PSSmg a  with  f : PSSmg b.

Is it possible to add some construct  foo  to the  language  so that the checker 
would allow to replace  f : PSSmg a  with  f : PSSmg b,  if   p : associated a b  
and  foo  is set for  PSSmg
?

May be, this is rather naive.
All right, if this is not possible, still dependent types make a great deal.

Here is the implementation for the  Set of all  p-subsemigroups  which I keep in mind:

------------------------------------------------------------------------
module SubsemigroupPack (c l : Level) (M : CommutativeMonoid c l)
  where
  C   = CommutativeMonoid.Carrier M
  _≈_ = CommutativeMonoid._≈_ M
  _∙_ = CommutativeMonoid._∙_ M

  associated : C → C → Set _           	       -- a  and  b  divide each other                
  associated a b =  ∃₂ λ (x y : C) →  (x ∙ a) ≈ b  ×  (y ∙ b) ≈ a
  --                                                                                          
  -- <a> == <b>  iff  associated a b                                                          

  record PSSmg (a : C) : Set (c ⊔L l)   -- p-Subsemigroup generated by  a                     
    where                                                                  
    constructor pSSmg

    field  factor : C

    element : C
    element = factor ∙ a

    -- Example.  pSSmg 3  : PSSmg 5                                                           
    --           expresses  15  as an element of the subsemigroup of <5>.                     

    _=s_ : Rel C _
    x =s y =  (x ∙ a) ≈ (y ∙ a)

  data PSSmgs : Set (c ⊔L l) where          -- the set of p-subsemigroups in M                
                             pssmg : (a : C) → PSSmg a → PSSmgs

  _=pss_ : Rel PSSmgs _
  (pssmg a smg) =pss (pssmg b smg') =  associated a b
---------------------------------------------------------------------------

So a p-subsemigroup  <a>  is a type, and it can be made a Semigroup, and 
a program can compute over  <a>.
And also a program can compare <a> and <b>, and to have the Setoid of
p-subsemigroups in M. 
And there remains this difference:

What to add to the language in order to make this possible: 
   postulate p0 :  extSmg@(pssmg a smg) =pss extSmg'@(pssmg b smg')                   
   postulate f  :  smg                                                                          
   g : smg'                                                                                   
   g = f                 
?