249mainindex.xmlPatrick NicodemusHello, and welcome to my personal website.I am a research mathematician interested in applied topology, category theory, homological algebra, type theory and formal verification.At the moment, I primarily work on applied topology, in the Cámara Lab at the University of Pennsylvania. Specifically, I apply the Gromov-Wasserstein distance to the study of cell morphology. I also maintain CAJAL, a Python package for the analysis of cell morphology.This website is under construction. Over the course of the next few weeks, I intend to start blogging here and uploading content, ideally, both my about my mathematics research, and potentially some literate formal verification using the Rocq theorem prover.Some things you might find interesting: Some nice looking Rocq proofs: Webpage aesthetics, i.e. basic use of LaTeX and Coqdoc. Brief walkthrough of Rocq's dependent pattern matching, illustrated via natural number arithmetic. No use of tactics. Walkthrough continued, this time focusing on basic properties of equality. No use of tactics. Some practice with Elpi, a logic programming language which Enrico Tassi and others have been developing as a tactic language for the Rocq theorem prover.