14.1 General Presentation
This section describes the inheritance mechanism of Coq. In Coq with
inheritance, we are not interested in adding any expressive power to
our theory, but only convenience. Given a term, possibly not typable,
we are interested in the problem of determining if it can be well
typed modulo insertion of appropriate coercions. We allow to write:
-
(f a) where f:(x:A)B and a:A' when A' can
be seen in some sense as a subtype of A.
- x:A when A is not a type, but can be seen in
a certain sense as a type: set, group, category etc.
- (f a) when f is not a function, but can be seen in a certain sense
as a function: bijection, functor, any structure morphism etc.