Subtyping for f-bounded quantifiers and equirecursive types

<em>Equirecursive types</em> consider a recursive type to be equal to its unrolling and have no explicit term-level coercions to change a term's type from the former to the latter or vice versa. This equality makes deciding type equality and subtyping more difficult than the other approach--<em>isorecursive types</em>, in which the types are not equal, but isomorphic, witnessed by explicit term-level coercions. Previous work has built intuition, rules, and polynomial-time decision procedures for equirecursive types for first-order type systems. Some work has been done for type systems with parametric polymorphism, but that work is incomplete (see below). This chapter will give an intuitive theory of equirecursive types for second-order type systems, sound and complete rules, and a decision procedure for subtyping.