Regular Language Representations in the Constructive Type Theory of Coq