[Agda] What is the type of the diagonal function?
Jacques Carette
carette at mcmaster.ca
Wed Apr 24 18:05:43 CEST 2013
The naive version of diagonal, i.e.
diag x = x , x
has the 'obvious' type. But this is rather unsatisfactory because it
loses all dependency information. So one idea is to use
data <_> {a : Level} {A : Set a} (x : A) : Set a where
singleton : (y : A) → y ≡ x -> < x >
and then do
diag x = x , singleton x refl
so that diag now has a very precise type [and good computational
properties]. But this is not quite satisfactory either.
Has anyone looked into creating a "diagonal" function with a precise
type? Eventually, I want to be able to pattern-match on this, to enforce
that my 'input' can only be such a dependent pair. [Actually, it gets a
little trickier still, but this is the first interesting stumbling block].
Jacques
More information about the Agda
mailing list