Consists of the Agda model for The Essence of Ornaments by Pierre-Evariste Dagand, with additional code by myself in the Leo directory as well as minor modifications of the original code.
In addition the Ko directory contains the code for Programming with Ornaments, specifically taken from here.