[Agda] Academic reference for the Fin data type

[Nicolas Pouillard]

Hello,

I'm looking for a paper to cite about the Fin data type and its use
to represent binders (say λ-terms). (I already have those about the
approach with nested data types).

Any idea?

Thanks in advance,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr