Subtyping by folding an inductive relation into a coinductive one

Abstract

In this paper we show that a prototypical subtype relation that can neither be defined as a least fixed point nor as a greatest fixed point can nevertheless be defined in a dependently typed language with inductive and coinductive types. The definition proceeds alike a fold in functional programming, although a rather unusual one: that is not applied to any starting object. There has been a related construction of bisimilarity in Coq by Nakata and Uustalu recently, however, our case is not concerned with bisimilarity but a weaker notion of similarity that corresponds to recursive subtyping and has it’s own interesting problems.