Type theories with canonical objects like Martin Lof 's Type Theory or Luo's
UTT have increasingly gained popularity in the last decades due to their usage
in proof assistants, formal semantics of natural language and formalization
of mathematics. The main purpose of this work is to explore a new way
of introducing coercive subtyping in such type theories which facilitates the
representation of some practical notions of subtyping.
Introducing subtyping in dependent type theories is not straightforward
when the preservation of properties like canonicity and subject reduction is also
desired. Previous research already showed how such properties are affected
by the usual notion of subsumptive subtyping and offered an alternative in
the form of coercive subtyping introduced by enriching the system with a
set of coercive subtyping judgements. Here I introduce a new way of adding
coercive subtyping to type theory, specifically by annotating certain functions
in assumptions, arguing that this is more handy to represent practical cases.
This system is also closer to the programming model of proof assistants like
Coq where coercions are annotated as such at the assumption level.
Assumptions in Type Theory are represented as either contexts, which
are sequences of membership entries for variables that bear abstraction and
substitution or signatures, which are sequences of memberships entries for
constants for which abstraction and substitution are not available. I shall use
signatures as an environment for subtyping assumptions. I will prove that
the system thus obtained is well behaved, in that it is only abbreviational to
the original system, by considering its relation with the previous version of
coercive subtyping which was already proved to be well behaved.
To demonstrate the ability of the system to argue about practical situations,
I will present three case studies. The first one studies the relationship
between a subsumptive subtyping system and coercive subtyping. The second
case study discusses how Russell-style universe inclusions, as found in Homotopy Type Theory, can be understood as coercions in a system with Tarski
style hierarchy. And the last discussion is the need to treat injectivity as an
assumption as well in order to capture faithfully some notions of subtyping
which are based on or generalize inclusion.