My research field is in formal methods. I'm particularly interested in expressing mathematical concepts in (dependent) type theories, specifically, in univalent type theory. Briefly, a type theory is formal system that can serve as a foundation for mathematics where objects are mere constructions of others. What makes really interesting type theory is the huge interaction of ideas coming from fields like category theory, functional programing, homotopy theory, among many others. For a type theorist, there is no distinction between doing mathematics and programming. Type theories have computational meaning that makes them practical to use for computing. Thus, the proofs I produce for my research are verified by the computer in a programming language called Agda. The topic I am currently working with is graph theory and the notion of planarity. This approach gives a theoretical development correct up-to the correctness of the proof-checker.