Updates

I recently gave a talk at HoTT/UF2024 hosted by KU Leuven. You can find details about the talk, along with a recording, under the talks section on the following page.

Bio

I graduated summa cum laude from the University of Colorado, Boulder with a bachelors of arts in mathematics and in philosophy. For my honors, I defended a thesis in the mathematics department titled “Eckmann-Hilton and the Hopf Fibration in Homotopy Type Theory”. I have presented the results of my thesis at multiple international math confrences, which you can find in the Talks section.

Within mathematics, I have a focus in higher category theory and homotopy theory, in type theory and the foundations of math, and in connections between these subjects and computer science, such as functional programming and the formal verification of proofs and programs.

I also have an interest in mathematical cryptography, combinatorics and probability theory. I enjoy writing python programs implementing ideas from these subjects. You can find some of these projects on my github, or under the projects section of this website.

As an application of my focus in functional programming, I am a contributor to the agda-unimath repository, an encyclopedia of formalized mathematics and certified programs. This is a collaborative and sprawling formal verification project comprising over 300K lines of code. Written in Agda, a dependently typed pure functional programming language, agda-unimath uses a variant of Martin L"of Type Theory combined with univalence and postulated higher inductive types to provide a foundations for mathematics. I am currently working to formalize the results of my thesis in the agda-unimath repository.

Mathematics

My areas of specialization with in mathematics include higher category theory and homotopy theory, the foundations of mathematics and formal verification, as well as bringing these subjects closer together. I am particularly interested in synthetic approaches to higher category theory and homotopy theory. I favor univalent approaches to the foundations of mathematics and I hope to help advance their prominence in the mathematical community by developing mathematics in Homotopy Type Theory. For an example of this, please see the work in my honors thesis.

I succesfully defended my honors thesis in Spring 2023, which was written under the direction of Professor Jonathan Wise. The title of the thesis is Eckmann-Hilton and The Hopf Fibration in Homotopy Type Theory. In the thesis I develop an elementary proof in the language of book HoTT that demonstrates that the Hopf fibration, the generator of $\pi_3(\mathbb{S}^2)$, can be constructed from the Eckmann-Hilton argument. I presented the results of this thesis at the Carnegie Mellon University’s Internation Confrence of Homotopy Type Theory 2023 and at KU Leuven’s Workshop on Homotopy Type Theory / Univalent Foundations. I am currently working to formally verify the results of my thesis in the agda-unimath library. For more on this, please see the following page.

agda-unimath

I am a contributor to the agda-unimath repository repository, a large-cale (over 300K lines of code) formal verification project that aims to “create an online encyclopedia of formalized mathematics containing an extensive curriculum of topics from a univalent point of view.” A full acount of my contributions can be found here. Here are some selected contributions:

• The Eckmann-Hilton Argument: I am one of the primary authors of the page on the Eckmann-Hilton argument.

• The Universal Property of the Family of Fibers of a Map: I am one of the primary authors of the page on the universal property of the family of fibers of a map

• The Suspension of a Type: The suspension of a type X is the (homotopy) pushout of the span unit <-- X --> unit. Pushouts are defined in agda-unimath by postulating a type with their universal property. I have helped to formalize some propreties of the suspension of a type, including:

  • a characterization of identifications in the type of suspension structures
  • a proof suspsensions have the universal property excpected of them
  • definitions of the unit and counit of the suspension loop space adjunction
  • the equivalence of the suspension loop space adjunction.

I am curruently working on formalizing the main results of my honors thesis using the agda-unimath library. You can read more about this project here.

Philosophy

In my junior and senior year at CU, I was president of the CU Boulder Undergraduate Philosophy Club. As president I scheduled interesting events, including faculty talks and club discussions, and worked to make the philosophy club a more inclusive enviroment by working with the Minorities and Philosophy program.

My interests in philosophy are primarily in metaphysics, philosophy of language, and the philosophy of mathematics. My favorite philosophical text is Saul Kripke’s Naming and Necessity.

Teaching and Tutoring

I am currently the lead mathematics instructor at Temple Grandin School, serving students with Asperger’s Syndrome and similar learning profiles.

I have over three years of teaching and tutoring experience, including experience with private tutoring, leading in person classes of up to 30 students, and more. I am currently working as a private tutor in the greater Boulder area, serving student both locally and online. If you or someone you know is interested in tutoring services, please don’t hesitate to reach out. You can find my email in the sidebar.