[Agda] congruence on dependent types

[Andreas Abel]

Probably this does not answer your question, but if you wonder how to 
treat ideals <a> in Agda, I would model them as predicates, not as types.

   < a > : C -> Set
   < a > b = exists \ x -> b == x * a

Basically < a > b is just "a divides b".

If you want to prove that associated a, b give rise to identical ideals, 
you would prove logical equivalence of predicates.

Cheers,
Andreas

On 20.06.13 8:49 PM, Sergei Meshveliani wrote:
> 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
> ?
>
>
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/