homotopy hypothesis-theorem delooping hypothesis-theorem stabilization hypothesis-theorem Opetopic type theory (Finster 12) is a higher dimensional directed homotopy type theory for omega-categories, i.e. of infinity-categories in the full sense of -categories. Specifically, it realizes the higher-dimensional horn-filler conditions in the definition of opetopic omega-categories due to Palm as inference rules of term introduction for a higher-dimensional kind of formal logic (but it presently...