Inductive types for large countable ordinal notations.
Hermann Ruge Jervel has a nice system that goes all the way to the Bachmann-Howard ordinal based on labelled trees.  See: http://folk.uio.no/herman/logsem.pdf

I also like his book on proof theory, which discusses this system: http://folk.uio.no/herman/bevisteori.ps