Introduction to two ways of defining real numbers: Dedekind cuts and Cauchy sequences, and discussion of their equivalence

This article explains the concepts of Büchi automata, ω-regular languages and ω-regular expressions, and the conversion algorithms between Büchi automata and ω-regular expressions.

This article explains the concept of pushdown automata.

This article is about set quotients.

This article is about image factorizations.

This article is about propositional truncations.

An outline for HoTT. Focus on easy to understand.

This article is about function extensionality.

This article is about Propositions, sets, and the higher truncation levels.

After a year, I'm finally take a course about HoTT formally in a classroom. This article is about the fundamental theorem of identity types.