Flipper is a small reversible language, implemented and embedded in Agda. Flipper aims to make it syntactically clear what the result of reversal, or 'flipping', will be, and supports many native Agda features including dependent types. For a brief introduction see this paper. The literate Agda source code for the paper is in this repo, filename short-paper.lagda.
Flipper is tested with Agda 2.6.3, and depends on Ulf Norell's agda-prelude.