[Agda] Agda formalization of Dijkstra's algorithm?

[Kenichi Asai]

Are there any formalizations of Dijkstra's shortest path algorithm in
Agda?  In other proof assistants, I found:

J. S. Moor and Q. Zhang
"Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2"
TPHOLs 2005, LNCS 3603, pp. 373-384, 2005

and references therein.  I welcome information on any formalizations
both in Agda and other proof assistants.

Thank you in advance.

Sincerely,

-- 
Kenichi Asai