This post is a bit different, as it’s somewhat more of a curiosity I recently noticed. It’s a theorem of that every type of of algebraic structure has a *free* algebra, similar to the notion of a free group, free module and so on. How about without choice? It turns out that the theory

has considerable consistency strength. It consistency-wise implies and is consistency-wise implied by a proper class of strongly compacts.