Fixed points of GADTs

Consider a basic language containing integer and boolean literals along with addition. The first approach to modeling this language could be a type like the following: »

Why HoTT matters

Equality is one of the most fundamental concepts in mathematics. But what is it? This one rule: for all x, x = x. If you are familiar »

Theories and parsing

I've had a lot of opportunity to get some reading in while spending time in the beautiful Chania. One of the books I'm reading is Logic »

Encoding unfolds

Folds are a pretty big deal. I've written a lot about them in the past. One thing I haven't covered, however, is their sister: the unfold, »

Computing domains

Recently I've been tutoring someone who's taking a pre-calculus class. They've been away from math for quite some time, so it's been an interesting challenge to »