Type-Theoretic Approaches to Ordinals