Archived tweet #5507 from the @leastfixedpoint Twitter Archive

Here's @ezyang's interesting re-presentation (in Coq) of @pigworker's "Elimination with a Motive": web.mit.edu/~ezyang/Public…