Opetopes are shapes (akin to globules, cubes, simplices, etc.) introduced to describe laws and coherence in higher categories. Their classical definitions, however, makes them difficult to manipulate efficiently. In this presentation, I will present ongoing works aiming to describe them completely from a type-theoretic standpoint. If time permits, I will showcase a proof checker for opetopes.