# [Agda] What is the type of the diagonal function?

Jacques Carette carette at mcmaster.ca
Thu Apr 25 01:36:23 CEST 2013

```On 13-04-24 03:27 PM, Andreas Abel wrote:
> Sorry, I do not see where you are heading, so it is hard to be helpful.

I am trying to model what happens in a meadow, a field-like structure
where 1/0 is defined to be 0, along with the (total) axioms 1/(1/x) == x
and x*(x*1/x) == x.  These axioms are understood to have computational
content, so are modelled as combinators [one for each direction of an
equality].

x*(x*1/x) == x is non-linear, unlike other axioms (like commutativity,
i.e. x*y = y*x) where each variable only occurs once on each side.  So
in using the combinator which transforms x*(x*1/x) needs to know that
the same x occurs 3 times in the rhs.  This is of course trivial to do
at the term level with a conditional.  The aim is to do this at the type
level.

In other words, I want my combinator foo which transforms x*(x*1/x) into
x to only be applicable to values which are exactly of that kind  [you
can model * and 1/ completely formally, as syntax for the purposes of
this problem, although that is not what I am doing].

It is ok to assume that x belongs in an enumerable type with decidable
equality, if that helps.

>
> [...] but frankly, I do not see the point of a singleton type, since
> it does not bear any more information than the unit type. If you want
> to store a y that is equal to x, why don't you take x right away?

Because I want to generate things like x*(x*1/x), then treat the result
as a "general product", and have the values drift apart from each
other.  Then I will want to later have these values "come back
together", and use the eliminator.  Which should not type if it is not
statically apparent that these are exactly x*(x*1/x).

[If it helps, this is related to one way of looking at the eta/epsilon
operators for a traced monoidal category].

Jacques
```