FETISH: An Introduction
Here, I will give an explanation of what the FETISH Rust library crate does by utilizing two other tools that I’ve developed as part of the ecosystem: FETISH...
A Functional Embedding of Terms In a Spatial Hierarchy (FETISH)
Over the past year and a bit, I’ve been actively working on the problem of modeling the behavior of computer programs with higher-order functions from collec...
Not-So-Effective Topology: My Ill-Fated MS Thesis
While this website is largely a repository for positive things that I deem “good enough” to reach a wider audience, the attentive reader would note that in m...
Your Waifu (ZFC) is Shit-Tier: Elementary Motivation for Constructive Type Theory
In December of 2017, I gave a fairly hyperbolic talk to the CWRU math club in which I presented a basic introduction to constructive type theory, and why one...
Paper Explanations: Formalising Real Numbers in Homotopy Type Theory + Partiality, Revisited
In the summer of 2017, as part of the work I did in my master’s program, I wrote summaries on two relatively-recent papers which interested me:
Explanation of The HoTT Book: Chapter 11 Part II
The following is part two of a summary of Chapter 11 on compactness and inductive covers over the reals in Homotopy Type Theory.
Explanation of The HoTT Book: Chapter 11 Part I
The following is part one of a summary of Chapter 11 on the construction of the real numbers as a Higher Inductive Type within Homotopy Type Theory.
The Cutest and Fuzziest Computer Program
Is the universe just a simulation? How can we describe everything we see with the shortest possible description length? Is it possible to write a “God progra...