SIL + Ownership in Agda Agda can be installed following the guide at PLFA Typecheck and load the file using C-c C-l in Emacs. The file Sil.agda contains inline documentation.