Analogical Type Theory

This paper proposes an analogical type system based on MITT. First, we talk about intuitive meaning of analogy. On the basis of intuitions, a set of rules is introduced and justified to deal with analogy. Analogies on types as well as terms are introduced in our system. By an analogy between types, we mean a pair of mappings satisfying coherent conditions on those types. Terms with analogous types are analogical if their focus points meet with each other related to an analogy of the types. Analogical theorem proving and term derivation methods are also illustrated as examples of applications of our system.