Bản mẫu:Chuyên ngành

Trong logic toán và khoa học máy tính, lý thuyết hình thái đồng luân (tiếng Anh: homotopy type theory, HoTT /hɒt/) đề cập đến các dòng phát triển khác nhau của lý thuyết hình thái trực giác, dựa trên việc diễn giải các hình thái như là các đối tượng mà lý thuyết đồng luân trừu tượng có thể áp dụng được.

Ngày xửa ngày xưa, trong cộng đồng toán học lan truyền ý tưởng rằng các hình thái trong lý thuyết hình thái tăng cường cùng với các hình thái đẳng thức của chúng có thể được coi là các groupoid. Ý tưởng này được chính xác hóa lần đầu tiên vào năm 1998 bởi Martin Hofmann và Thomas Strerich trong bài báo "The groupoid interpretation of type theory", trong đó họ cho thấy rằng lý thuyết hình thái tăng cường có một mô hình trong phạm trù các nhóm.^[1] Đây là mô hình đồng luân đầu tiên của lý thuyết hình thái, mặc dù chỉ là "1 chiều" (các mô hình truyền thống trong phạm trù tập hợp là "0 chiều đồng luân").

Các mô hình cao chiều đầu tiên của lý thuyết hình thái tăng cường được xây dựng bởi Steve Awodey và sinh viên Michael Warren vào năm 2005 bằng cách sử dụng các phạm trù mô hình Quillen. Những kết quả này lần đầu tiên được trình bày trước công chúng tại hội nghị FMCS 2006 ^[2] trong đó Warren đã có một bài nói với tiêu đề "Homotopy models of intensional type theory", cũng đóng vai trò là bản cáo bạch luận án tiến sỹ của ông (hội đồng luận án là Awodey, Nicola Gambino và Alex Simpson). Một bản tóm tắt được lưu trong bản tóm tắt luận án của Warren.

Lý thuyết hình thái tăng cường	Lý thuyết đồng luân
các hình thái ${\displaystyle A}$	các không gian ${\displaystyle A}$
các đối tượng ${\displaystyle a}$	các điểm ${\displaystyle a}$
${\displaystyle a:A}$	${\displaystyle a\in A}$
hình thái phụ thuộc ${\displaystyle x:A\ \vdash \ B(x)\ }$	thành thớ ${\displaystyle B\to A}$
hình thái đẳng thức ${\displaystyle \mathrm {Id} _{A}(a,b)}$	không gian đường dẫn
${\displaystyle p:\mathrm {Id} _{A}(a,b)}$	đường ${\displaystyle p:a\to b}$
${\displaystyle \alpha :\mathrm {Id} _{\mathrm {Id} _{A}(a,b)}(p,q)}$	đồng luân ${\displaystyle \alpha :p\Rightarrow q}$

HoTT sử dụng một phiên bản sửa đổi của diễn giải " mệnh đề là hình thái " của lý thuyết hình thái (diễn giải mà theo đó một hình thái là một mệnh đề và một đối tượng là một chứng minh của mệnh đề). Trong HoTT, không giống như trong diễn giải "mệnh đề là hình thái" tiêu chuẩn, "các mệnh đề đơn thuần" đóng một vai trò đặc biệt: đó là các hình thái có nhiều nhất một đối tượng, xê xích một đẳng thức mệnh đề.

Khái niệm cơ bản của lý thuyết hình thái đồng luân là đường dẫn. Trong HoTT, hình thái ${\displaystyle a=b}$ là hình thái của tất cả các đường dẫn từ điểm ${\displaystyle a}$ đến điểm ${\displaystyle b}$. (Do đó, một chứng minh cho thấy một điểm ${\displaystyle a}$ bằng một điểm ${\displaystyle b}$ cũng là một đường dẫn từ điểm ${\displaystyle a}$ đến điểm ${\displaystyle b}$.) Với mọi điểm ${\displaystyle a}$, tồn tại một đường dẫn với hình thái ${\displaystyle a=a}$, tương ứng với tính chất phản xạ của đẳng thức. Một đường dẫn với hình thái ${\displaystyle a=b}$ có thể được nghịch đảo, tạo thành một đường dẫn với hình thái ${\displaystyle b=a}$, tương ứng với tính chất đối xứng của đẳng thức. Hai đường dẫn với các hình thái ${\displaystyle a=b}$ và.${\displaystyle b=c}$ có thể được nối, tạo thành một đường dẫn với hình thái ${\displaystyle a=c}$; điều này tương ứng với tính chất bắc cầu của đẳng thức.

Sau đây, ta sẽ dùng đường thay cho đường dẫn và loại thay cho hình thái.

Quan trọng nhất, cho trước một đường ${\displaystyle p:a=b}$ và một chứng minh cho thuộc tính ${\displaystyle P(a)}$, chứng minh đó có thể được chuyển dịch dọc theo đường ${\displaystyle p}$ để cho ta một chứng minh của thuộc tính ${\displaystyle P(b)}$. (Nói một cách tương đương, một đối tượng loại ${\displaystyle P(a)}$ có thể được biến thành một đối tượng loại ${\displaystyle P(b)}$.) Điều này tương ứng với tính chất thay thế của đẳng thức. Ở đây, một sự khác biệt quan trọng giữa HoTT và toán học cổ điển xuất hiện. Trong toán học cổ điển, một khi đẳng thức giữa hai giá trị ${\displaystyle a}$ và ${\displaystyle b}$ đã được thành lập, ${\displaystyle a}$ và ${\displaystyle b}$ có thể được sử dụng thay thế cho nhau và sau đó không còn bất kỳ sự phân biệt nào giữa chúng. Tuy nhiên, trong lý thuyết hình thái đồng luân, có thể có nhiều đường khác nhau cùng có hình thái ${\displaystyle a=b}$, và chuyển dịch một đối tượng dọc theo hai đường khác nhau sẽ mang lại hai kết quả khác nhau (tức là ta có hai chứng minh khác nhau cho thuộc tính ${\displaystyle P(b)}$). Do đó, trong lý thuyết hình thái đồng luân, khi áp dụng thuộc tính thay thế, cần phải nêu đường dẫn nào đang được sử dụng.

Nói chung, một "mệnh đề" có thể có nhiều chứng minh khác nhau. (Ví dụ, hình thái tất cả các số tự nhiên, khi được coi là một mệnh đề, có một chứng minh tương ứng với mỗi số tự nhiên.) Ngay cả khi một mệnh đề chỉ có một chứng minh ${\displaystyle a}$, không gian các đường dẫn loại ${\displaystyle a=a}$ có thể không tầm thường theo một cách nào đó. Một "mệnh đề đơn thuần" là bất kỳ hình thái nào hoặc là rỗng, hoặc là chỉ chứa một điểm với không gian đường dẫn tầm thường..

Lưu ý rằng ta viết ${\displaystyle a=b}$ cho ${\displaystyle Id_{A}(a,b)}$, do đó ngầm hiểu có một hình thái ${\displaystyle A}$ cho các đối tượng ${\displaystyle a,b}$. Đừng nhầm lẫn với ${\displaystyle id_{A}:A\to A}$, biểu thị hàm đồng nhất trên ${\displaystyle A}$.

Hai hình thái ${\displaystyle A}$ và ${\displaystyle B}$ thuộc một vũ trụ ${\displaystyle U}$ được định nghĩa là tương đương nếu tồn tại sự tương đương giữa chúng. Một sự tương đương là một hàm

${\displaystyle f:A\to B}$

có cả nghịch đảo trái và nghịch đảo phải, theo nghĩa với việc lựa chọn ${\displaystyle g}$ và ${\displaystyle h}$ phù hợp, các hình thái sau đây đều là inhabited:

${\displaystyle Id_{B\rightarrow B}(f\circ g,id_{B}),}$

${\displaystyle Id_{A\rightarrow A}(h\circ f,id_{A}).}$

tức là

${\displaystyle f\circ g=_{B\rightarrow B}id_{B},}$

${\displaystyle h\circ f=_{A\rightarrow A}id_{A}.}$

HoTT cho phép các chứng minh toán học được dịch sang ngôn ngữ lập trình máy tính dễ dàng hơn nhiều so với trước đây. Cách tiếp cận này cung cấp tiềm năng cho máy tính để kiểm tra các chứng minh khó.^[3]

• Phép tính xây dựng
• Tương ứng Curry-Howard
• Lý thuyết hình thái trực giác
• Giả thuyết đồng luân
• Univalent foundations

• The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ: Institute for Advanced Study.
• Awodey, S.; Warren, M. A. (January 2009). "Homotopy Theoretic Models of Identity Types". Mathematical Proceedings of the Cambridge Philosophical Society. 146 (1): 45–55. arXiv:0709.0248
• Awodey, Steve (2012). "Type Theory and Homotopy" (PDF). In Dybjer, P.; Lindström, Sten; Palmgren, Erik; et al. (eds.). Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science. Springer. pp. 183–201.
• Awodey, Steve (2014). "Structuralism, Invariance, and Univalence". Philosophia Mathematica. 22 (1): 1–11.
• Hofmann, Martin; Streicher, Thomas (1998). "The groupoid interpretation of type theory". In Sambin, G.; Smith, J.M. (eds.). Twenty Five Years of Constructive Type Theory. Clarendon Press. pp. 83–112.
• Rijke, Egbert (2012), Homotopy Type Theory (PDF) (Master's).
• Voevodsky, Vladimir (2006), A Very Short Note on Homotopy Lambda Calculus
• Voevodsky, Vladimir (2010), The Equivalence Axiom and Univalent Models of Type Theory, arXiv:1402.5556
• Warren, Michael A. (2008). Homotopy Theoretic Aspects of Constructive Type Theory

• David Corfield (2020), Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy, Oxford University Press.

• Homotopy Type Theory
• Homotopy type theory in nLab
• Homotopy type theory wiki
• Vladimir Voevodsky's webpage on the Univalent Foundations
• Homotopy Type Theory and the Univalent Foundations of Mathematics by Steve Awodey
• "Constructive Type Theory and Homotopy" – Video lecture by Steve Awodey at the Institute for Advanced Study
• #hott connect Homotopy Type Theory IRC channel