Toward Higher Inductive Types - Michael Shulman