[Agda] congruence on dependent types
Sergei Meshveliani
mechvel at botik.ru
Thu Jun 20 20:49:02 CEST 2013
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
?
More information about the Agda
mailing list