[codethief]

I'm not quite following. According to the OP and the docs you linked, a subtype is defined by a base type and a predicate. In other words: You can view it as a subset of the set of elements of the base type. That's pretty much the standard definition of a subtype.

Object-oriented programming languages are not that different: The types induced by classes can easily be viewed as sets: A child class is a specialized version of its parent's class, hence a subtype/subset thereof if you define all the sets by declaring `instanceof` to be their predicate function.

[nickpsecurity]

B. Meyer made an attempt to formulate many concepts in programming using simple, set theory. It might help in discussions like this. I say might since I'm not mathematically-inclined enough to know for sure.

https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-pro...

[SkiFire13]

> You can view it as a subset of the set of elements of the base type.

Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa. They are not a subset of the other, hence why it's improper to consider one a subtype of the other.

[codethief]

> Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa.

Emphasis on "technically". The embedding is trivial. The Lean docs linked by the GP suggest to put those technicalities aside:

> Even though they are pairs syntactically, Subtype should really be thought of as elements of the base type with associated proof obligations.

[gugagore]

Right, though the embedding is trivial, the conceptual distinction is not. In Lean, a subtype is a refinement that restricts by proof. In OOP, a subclass augments or overrides behavior. It's composition versus inheritance. The trivial embedding masks a fundamental shift in what "subtype" means.