在數理邏輯和計算機科學中，同構類型理論（HoTT/h?t/）是指直觀類型理論的各種發展路線，其基礎是將類型解釋為（抽象的）同構理論的直覺所適用的對象。這包括為這種類型理論構建同構和高分類模型；將類型理論作為抽象同構理論和高分類理論的邏輯（或內部語言）；在類型理論的基礎上發展數學（包括以前存在的數學和同構類型使之成為可能的新數學）；以及在計算機證明助手中對上述每一項進行形式化。被稱為同構類型理論的工作與單價基礎項目之間存在著很大的重疊。雖然兩者都沒有精確的劃分，而且這些術語有時可以互換使用，但用法的選擇有時也與觀點和重點的不同相對應。因此，本文可能并不完全代表這些領域所有研究者的觀點。當一個領域處于快速變化之中時，這種差異性是不可避免的。

前史：群組模型曾幾何時，廣義類型理論中的類型及其身份類型可以被視為群組的想法是數學界的民間傳說。1998年，MartinHofmann和ThomasStreicher發表了一篇名為《類型理論的類群解釋》的論文，首次在語義上明確了這一觀點，他們在論文中表明，廣義類型理論在類群中有一個模型。這是類型理論的xxx個真正的同構模型，盡管只是一維的（集合類別中的傳統模型是同構的0維）。他們的論文也預示了后來同構類型理論的若干發展。例如，他們指出類群模型滿足一個他們稱之為宇宙擴展性的規則，這不是別的，而是弗拉基米爾-沃耶沃茨基十年后提出的對1-類型的限制。(然而，1-類型的公理在表述上明顯更簡單，因為不需要一個連貫的等價概念）。他們還將同構的范疇定義為平等，并猜想在一個使用高維群的模型中，對于這樣的范疇，人們會有平等性；這后來被BenediktAhrens,KrzysztofKapulkin和MichaelShulman證明。早期歷史：模型類別和高分組2005年，SteveAwodey和他的學生MichaelWarren用Quillen模型類別構建了擴展類型理論的xxx個高維模型。

所有早期的高維模型的構造都必須處理依附類型理論模型的典型的一致性問題，并且開發了各種解決方案。大約在同一時間，VladimirVoevodsky在尋找數學實用形式化語言的背景下獨立研究類型理論。2006年9月，他在Types郵件列表中發表了一篇關于同構λ微積分的簡短說明，其中勾勒出一個具有依存積、和與宇宙的類型理論的輪廓，以及這個類型理論的一個模型.