[TYPES] Types theories with first-class definitional extensions

[Jacques Carette]

I am looking for literature on (higher-order, potentially dependent) 
type theories where a context (telescope) can contain not just 
declarations, but also definitions.

Of course, from a semantic point of view, this is entirely unnecessary, 
as such definitions can simply be expanded away. However, from a 
categorical standpoint (amongst others), things are not so trivial: what 
is the proper meaning of morphisms (substitutions) in such a case?

The motivation comes from the remark that the category of contexts for a 
type theory is the opposite category of that of theory presentations 
(aka algebraic theories, algebraic specifications, etc).  By applying 
the 'little theories' approach, it is really the theory morphisms that 
carry the most interesting information.  And that, in practice, one uses 
"conservative extensions" of theories all the time.

Some concrete examples:
- in Agda, in a parametric record definition, one can also define 
generic functions which 'depend' on the fields of the record;
- in Haskell, in a typeclass definition, one can define default 
implementations;
- in Scala, in a trait, one can similarly define default implementations.
These 3 things are essentially the same idea, of a conservative 
extension of a theory.

The problem arises when one wants to build theory morphisms (which would 
be typeclass-to-typeclass functions in Haskell, or trait-to-trait 
functions in Scala, neither of which are available AFAIK): what to do 
with the definitions?  Again, from a semantic point-of-view, there is no 
intrinsic difficulty, and multiple different designs are equivalent.  
The question only really becomes interesting when considering the 
pragmatics.  Some designs lead to huge combinatorial explosions of 
definitions once your theory library gets into the 100s of theories, 
never mind the 1000s, which is what a realistic library of 
mathematics+CS needs.

This is not entirely straightforward.  For example, the old theorem 
prover IMPS actually has 4 different ways to handle the transport of 
definitional extension along theory morphisms.

I have tried to look into the literature for related work, but I have 
not been successful.  Thus this query.

Jacques