Version of Monday, April 12, 2021, 08:42 AM

Powered by pandoc 2.10.1

Jonathan Prieto-Cubides

That's me visiting the Nasa station in Florida, USA.

Contact information

Welcome, this is my personal website. I’m from the beautiful country Colombia and the capital city Bogotá. I have two first names and two last names as almost everyone in South America. The first last name is by my father, Rafael Prieto, and the other by my mother, Luzmila Cubides. My full name is Jonathan Steven Prieto Cubides. Nowadays, I live in Norway, a fascinating country full of kind people, breathtaking nature, big fjords, good salmon, hansa, deers, and many other cool things.

Research work

I am currently a PhD student in computer science at the University of Bergen in the Deparment of Informatics. My current supervisors are Håkon R. Gylterud and Marc Bezem. The context of my research is within the field of constructive mathematics. I study mathematical constructions within a relatively recent type theory called homotopy type theory. Many type theories have computational meaning, making them practical to use for computing. A type theory can be defined as a formal system and also as a functional programming language. In this view, there is, therefore, no distinction between doing mathematics as proving statements and programming on the computer. For example, my programs usually contain specifications, i.e. lemmas along with their corresponding proofs. Then, one can assess the correctness of the mathematical results with a total level of confidence up-to the correctness of the proof-checker.

keywords: dependent type theory, homotopy type theory, agda, functional programing, proof-assistant, univalence axiom, univalent mathematics

I have other academic interests, e.g. natural language processing, machine learning algorithms, algorithm design, philosophy of sciences, programming language theory, and software development.


Active projects

I am currently working on graph-theoretical constructions using Univalent Foundations. The following address contains a work-in-progress formalisation of this project in the proof-assistant Agda v2.6+.

Former projects

Archived projects

Other initiatives



Seminar talks


I have been teaching assistant for the following courses at University of Bergen:

I taught the following courses:

Some notes

Most recent changes

(2021-04-09) (442e194) [ css ] pic class update.
(2021-04-09) (76cd983) [ css ] pic class update.
(2021-04-09) (36c6f13) fixed some links
(2021-04-09) (5f5bb90) Fixed intro.
(2021-04-09) (140a265) [ css ] fixed image max-width.