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

[Jacques Carette]

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