Agda code for draft paper by Larry Diehl and Tim Sheard (submitted for consideration to TyDe 2016):
You can build the paper in the paper
directory with a command like:
agda --latex-dir=. -i /PATH/TO/AGDA-STDLIB/src/ -i . --latex infir.lagda && pdflatex infir.tex
Additionally, a universe polymorphic version of the generic open universe.
The code is released under an MIT license