Toward Higher Inductive Types

University of California, San Diego; Member, School of Mathematics