The paper aims at a formalization of analogy reasoning. An analogical intuitionistic type theory (AITT) is proposed. AITT is developed from Martin-Löf's intuitionistic type theory MITT and from the analogical calculus \(LK_A\) [the authors, Theor. Comput. Sci. 113, 211-230 (1993; Zbl 0784.68083)]. Martin-Löf's intuitionistic type theory is presented in section 2. In section 3, fundamentals of the AITT-analogy theory are given. Analogy between types is defined as follows. Let \(A\) and \(B\) be types (sets). Further, let us consider mappings \(f\) and \(g\), such that \(f : A \to B\), \(g : B \to A\), the equivalence relations \(\sim_f\), \(\sim_g\), and mappings \([f] : A/ \sim_f \to B/ \sim_g\), \([g] : B/ \sim_g \to A/ \sim_f\).