We're announcing Mikan: a proof assistant for cubical type theory, forked from the Agda codebase (via ehamberg) — discussion

#plt #release