[Agda] Ornamental Algebras, Algebraic Ornaments

[conor at strictlypositive.org]

Friends

After a busy day hacking, here's the development of
ornaments, with the Hutton's Razor example, to boot.

Phew!

Conor
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Ornament.agda
Type: application/octet-stream
Size: 8204 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20081202/fdf42f07/Ornament.obj