ในทฤษฎีประเภทซึ่งเป็นสาขาหนึ่งของคณิตศาสตร์ประเภทเอกลักษณ์แสดงถึงแนวคิดของความเท่าเทียมกันเรียกอีกอย่างว่าความเท่าเทียมกันเชิงประพจน์เพื่อแยกความแตกต่างจาก "ความเท่าเทียมกันเชิงตัดสิน" ความเท่าเทียมกันในทฤษฎีประเภทเป็นหัวข้อที่ซับซ้อนและเป็นหัวข้อของการวิจัย เช่น สาขาทฤษฎีประเภทโฮโมโทปี^{[ 1 ]}

ประเภทเอกลักษณ์เป็นหนึ่งใน 2 แนวคิดที่แตกต่างกันของความเท่าเทียมกันในทฤษฎีประเภท^{[ 2 ]} แนวคิดพื้นฐานกว่าคือ "ความเท่าเทียมกันเชิงตัดสิน" ซึ่งเป็นการ ตัดสิน

เอกลักษณ์ประเภทนี้สามารถทำได้มากกว่าความเท่าเทียมกันเชิงตัดสิน มันสามารถใช้เพื่อแสดง "สำหรับทุก" ซึ่งเป็นไปไม่ได้ที่จะแสดงด้วยความเท่าเทียมกันเชิงตัดสิน สิ่งนี้ทำได้โดยการใช้ตัวกำจัด (หรือ "ตัววนซ้ำ") ของจำนวนธรรมชาติที่เรียกว่า "R" ${\displaystyle x,x+1=1+x}$

ฟังก์ชัน "R" ช่วยให้เรากำหนดฟังก์ชันใหม่บนจำนวนธรรมชาติได้ ฟังก์ชันใหม่ "P" นั้นถูกกำหนดให้เป็น "(λ x:nat . x+1 = 1+x)" อาร์กิวเมนต์อื่นๆ ทำหน้าที่เหมือนส่วนต่างๆ ของการพิสูจน์แบบอุปนัย อาร์กิวเมนต์ "PZ : P 0" กลายเป็นกรณีพื้นฐาน "0+1 = 1+0" ซึ่งก็คือประโยค "refl nat 1" อาร์กิวเมนต์ "PS : P n → P (S n)" กลายเป็นกรณีอุปนัย โดยพื้นฐานแล้ว นี่หมายความว่าเมื่อ "x+1 = 1+x" ถูกแทนที่ด้วยค่ามาตรฐาน นิพจน์นั้นจะเหมือนกับ "refl nat (x+1)"

ประเภทเอกลักษณ์มีความซับซ้อนและเป็นหัวข้อการวิจัยในทฤษฎีประเภท แม้ว่าทุกเวอร์ชันจะเห็นพ้องต้องกันในเรื่องตัวสร้าง "refl" แต่คุณสมบัติและฟังก์ชันการกำจัดของแต่ละเวอร์ชันนั้นแตกต่างกันอย่างมาก

สำหรับเวอร์ชัน "ส่วนขยาย" ประเภทเอกลักษณ์ใดๆ ก็สามารถแปลงเป็นความเท่าเทียมกันเชิงตัดสินได้ เวอร์ชันการคำนวณเรียกว่า "สัจพจน์ K" ซึ่งคิดค้นโดย Thomas Streicher ^{[ 3 ]} สิ่งเหล่านี้ไม่ได้รับความนิยมมากนักในปัจจุบัน

Martin Hofmann และ Thomas Streicher ปฏิเสธความคิดที่ว่าทฤษฎีประเภทต้องการให้เทอมทั้งหมดของประเภทเอกลักษณ์เหมือนกัน^{[ 4 ]}

สาขาการวิจัยที่เป็นที่นิยมเกี่ยวกับประเภทเอกลักษณ์ ได้แก่ทฤษฎีประเภทโฮโมโทปี^{[ 5 ]}และทฤษฎี ประเภทลูกบาศก์