Homotopy type theory
ریاضیاتی منطق اور کمپیوٹر سائنس میں، ہوموٹوپی ٹائپ تھیوری (ایچ او ٹی ٹی) سے مراد انٹوشنسٹک ٹائپ تھیوری کی نشوونما کی مختلف لائنیں ہیں، جو اشیاء کے طور پر اقسام کی تشریح پر مبنی ہیں جن پر (تجریدی) ہوموٹوپی تھیوری کا انٹوشن لاگو ہوتا ہے۔ اس میں، کام کی دیگر لائنوں کے علاوہ، اس طرح کے نظریات کے لیے ہوموٹوپیکل اور اعلی زمرہ کے ماڈلز کی تعمیر ؛ تجریدی ہوموٹوپی تھیوری اور اعلی زمرہ تھیوری کے لیے ٹائپ تھیوری کا منطق (یا اندرونی زبان) کے طور پر استعمال ؛ ٹائپ تھیوریٹک فاؤنڈیشن کے اندر ریاضی کی ترقی (بشمول پہلے سے موجود ریاضی اور نئی ریاضی جو ہوموٹوپیکل اقسام ممکن بناتی ہیں) ؛ اور کمپیوٹر پروف اسسٹنٹ میں ان میں سے ہر ایک کو باضابطہ بنانا شامل ہے۔ اس کام کے درمیان ایک بڑا اوورلیپ ہے جسے ہوموٹوپی ٹائپ تھیوری کہا جاتا ہے، اور غیر مساوی فاؤنڈیشنز پروجیکٹ۔ اگرچہ دونوں میں سے کسی کو بھی قطعی طور پر بیان نہیں کیا گیا ہے، اور اصطلاحات کو بعض اوقات ایک دوسرے کے متبادل کے طور پر استعمال کیا جاتا ہے، لیکن استعمال کا انتخاب بھی بعض اوقات نقطہ نظر اور زور میں فرق سے مطابقت رکھتا ہے۔ اس طرح، یہ مضمون شعبوں کے تمام محققین کے خیالات کو یکساں طور پر پیش نہیں کر سکتا۔ جب کوئی فیلڈ تیز رفتار بہاؤ میں ہو تو اس قسم کی تغیر پذیری ناگزیر ہوتی ہے۔ تاریخ گروپائڈ ماڈل ایک زمانے میں یہ خیال کہ انٹیسنشنل ٹائپ تھیوری میں ان کی شناخت کی اقسام کو گروپائڈ سمجھا جا سکتا ہے، ریاضیاتی لوک داستانیں تھیں۔ اسے پہلی بار مارٹن ہوفمین اور تھامس اسٹریچر کے 1994 کے مقالے میں الفاظ کے لحاظ سے درست بنایا گیا تھا جسے "گروپائڈ ماڈل شناخت کے ثبوت کی انفرادیت کی تردید کرتا ہے" کہا جاتا ہے، جس میں انہوں نے ظاہر کیا کہ انٹینشنل ٹائپ تھیوری کا گروپائڈز کے زمرے میں ایک ماڈل ہے۔ یہ ٹائپ تھیوری کا پہلا حقیقی "ہوموٹوپیکل" ماڈل تھا، حالانکہ صرف "1 جہتی" (سیٹوں کے زمرے میں روایتی ماڈل ہوموٹوپیکل طور پر 0 جہتی ہیں)۔ ان کے فالو اپ پیپر نے ہوموٹوپی ٹائپ تھیوری میں بعد کی کئی پیشرفتوں کی پیش گوئی کی۔ مثال کے طور پر، انہوں نے نوٹ کیا کہ گروپائڈ ماڈل ایک اصول کو مطمئن کرتا ہے جسے وہ "کائنات کی وسعت" کہتے ہیں، جو کہ کوئی اور نہیں بلکہ یکسانیت کے محور کی 1 اقسام پر پابندی ہے جسے ولادیمیر ویووڈسکی نے دس سال بعد تجویز کیا تھا۔ (1 اقسام کے لیے محوریہ وضع کرنا خاص طور پر آسان ہے، تاہم، چونکہ "مساوات" کے مربوط تصور کی ضرورت نہیں ہے۔) انہوں نے "آئسومورفزم کے ساتھ زمرہ جات کو مساوات" کے طور پر بھی بیان کیا اور قیاس کیا کہ اعلی جہتی گروپائڈز کا استعمال کرنے والے ماڈل میں، اس طرح کے زمروں کے لیے "مساوات مساوات ہے" ؛ یہ بعد میں بینیڈکٹ آرنس، کریزٹوف کاپلکن اور مائیکل شولمین نے ثابت کیا۔ ابتدائی تاریخ: ماڈل کیٹیگریز اور اعلی گروپائڈز انٹینشنل ٹائپ تھیوری کے پہلے اعلی جہتی ماڈل اسٹیو آوڈی اور ان کے طالب علم مائیکل وارن نے 2005 میں کویلن ماڈل کیٹیگریز کا استعمال کرتے ہوئے بنائے تھے۔ یہ نتائج سب سے پہلے ایف ایم سی ایس 2006 کی کانفرنس میں عوام کے سامنے پیش کیے گئے تھے جس میں وارن نے "ہوموٹوپی ماڈل آف انٹینشنل ٹائپ تھیوری" کے عنوان سے ایک تقریر کی تھی، جس نے ان کے مقالے کے پراسپیکٹس کے طور پر بھی کام کیا (مقالہ کمیٹی موجود ایوڈی، نکولا گیمبینو اور الیکس سمپسن تھے)۔ خلاصہ وارن کے مقالے پراسپیکٹس خلاصہ میں موجود ہے۔ 2006 میں اپسالا یونیورسٹی میں شناخت کی اقسام کے بارے میں ایک ورکشاپ میں انٹینشنل ٹائپ تھیوری اور فیکٹرائزیشن سسٹم کے درمیان تعلق کے بارے میں دو باتیں ہوئیں: ایک رچرڈ گارنر کی طرف سے، "فیکٹرائزیشن سسٹم فار ٹائپ تھیوری"، اور ایک مائیکل وارن کی طرف سے، "ماڈل کیٹیگریز اور انٹینشنل آئیڈینٹی ٹائپز"۔ اسٹیو آوڈی، "اعلی جہتی زمروں کا ٹائپ تھیوری"، اور تھامس اسٹریچر، "شناخت کی اقسام بمقابلہ کمزور اومیگا گروپائڈز: کچھ خیالات، کچھ مسائل" کی بات چیت میں متعلقہ خیالات پر تبادلہ خیال کیا گیا۔ اسی کانفرنس میں بینو وین ڈین برگ نے "کمزور اومیگا کیٹیگریز کی اقسام" کے عنوان سے ایک تقریر کی جہاں انہوں نے ان خیالات کا خاکہ پیش کیا جو بعد میں رچرڈ گارنر کے ساتھ مشترکہ مقالے کا موضوع بن گئے۔ اعلی جہتی ماڈلز کی تمام ابتدائی تعمیرات کو انحصار ٹائپ تھیوری کے ماڈلز کے عام ہم آہنگی کے مسئلے سے نمٹنا پڑا، اور مختلف حل تیار کیے گئے۔ اس طرح کا ایک 2009 میں ویووڈسکی نے دیا تھا، دوسرا 2010 میں وین ڈین برگ اور گارنر نے دیا تھا۔ ووووڈسکی کی تعمیر پر مبنی ایک عمومی حل بالآخر لمسڈین اور وارن نے 2014 میں دیا۔ 2007 میں پی ایس ایس ایل 86 میں اوڈی نے "ہوموٹوپی ٹائپ تھیوری" کے عنوان سے ایک تقریر کی (یہ اس اصطلاح کا پہلا عوامی استعمال تھا، جسے اوڈی نے وضع کیا تھا)۔ اوڈی اور وارن نے اپنے نتائج کا خلاصہ "شناخت کی اقسام کے ہوموٹوپی نظریاتی ماڈل" کے مقالے میں کیا، جو 2007 میں آرکسیو پری پرنٹ سرور پر پوسٹ کیا گیا تھا اور 2009 میں شائع ہوا تھا۔ ایک مزید تفصیلی ورژن 2008 میں وارن کے مقالے "ہوموٹوپی نظریاتی پہلوؤں کے تعمیری ٹائپ تھیوری" میں شائع ہوا۔ تقریبا اسی وقت، ولادیمیر ووووڈسکی آزادانہ طور پر ریاضی کی عملی رسمی شکل کے لیے زبان کی تلاش کے تناظر میں ٹائپ تھیوری کی تحقیقات کر رہے تھے۔ ستمبر 2006 میں انہوں نے ٹائپز میلنگ لسٹ میں "ہوموٹوپی لیمبڈا کیلکولس پر ایک بہت مختصر نوٹ" پوسٹ کیا، جس میں منحصر مصنوعات، جملوں اور کائناتوں کے ساتھ ٹائپ تھیوری کے خاکے اور کان کے سادہ سیٹوں میں اس قسم کے نظریہ کے ماڈل کا خاکہ پیش کیا گیا۔ اس کا آغاز یہ کہتے ہوئے ہوا کہ "ہوموٹوپی λ-کیلکولس ایک فرضی (اس وقت) قسم کا نظام ہے" اور اس کا اختتام "اس وقت جو میں نے اوپر کہا ہے وہ قیاس آرائیوں کی سطح پر ہے" کے ساتھ ہوا۔ یہاں تک کہ ہوموٹوپی زمرے میں ٹی ایس کے ماڈل کی تعریف بھی غیر معمولی ہے جو پیچیدہ ہم آہنگی کے مسائل کا حوالہ دیتی ہے جو 2009 تک حل نہیں ہوئے تھے۔ اس نوٹ میں "مساوات کی اقسام" کی ایک نحو تعریف شامل تھی جس کے بارے میں ماڈل میں پاتھ اسپیس کے ذریعے تشریح کرنے کا دعوی کیا گیا تھا، لیکن شناخت کی اقسام کے لیے پر مارٹن-لوف کے اصولوں پر غور نہیں کیا گیا۔ اس نے کائنات کو سائز کے علاوہ ہوموٹوپی طول و عرض کے ذریعے بھی مستحکم کیا، ایک ایسا خیال جسے بعد میں زیادہ تر مسترد کر دیا گیا۔ نحو کی طرف، بینو وین ڈین برگ نے 2006 میں قیاس کیا کہ شدت پسندانہ قسم کے نظریہ میں ایک قسم کی شناخت کی اقسام کے ٹاور میں مائیکل بٹانن کے "گلوبولر، الجبرائی" معنوں میں ω-زمرہ کی ساخت ہونی چاہیے، اور درحقیقت ایک ω-گروپائڈ ہونا چاہیے۔ یہ بعد میں وین ڈین برگ اور گارنر نے "ٹائپز آر ویک اومیگا گروپائڈز" (شائع شدہ 2008) کے مقالے میں آزادانہ طور پر ثابت کیا، اور پیٹر لمسڈین نے "ویک ω-کیٹیگریز فرام انٹینشنل ٹائپ تھیوری" (شائع شدہ 2009) کے مقالے میں اور اپنے 2010 کے پی ایچ ڈی تھیسس "ہائیر کیٹیگریز فرام ٹائپ تھیوریز" کے حصے کے طور پر۔ غیر مساوی محوریہ، مصنوعی ہوموٹوپی تھیوری، اور اعلی انڈکٹو اقسام غیر مساوی ریشے کا تصور ویووڈسکی نے 2006 کے اوائل میں متعارف کرایا تھا۔ تاہم، اس پراپرٹی پر مارٹن-لوف ٹائپ تھیوری کی تمام پیش کشوں کے اصرار کی وجہ سے کہ شناخت کی اقسام، خالی سیاق و سباق میں، صرف اضطراری ہو سکتی ہیں، ووووڈسکی نے 2009 تک تسلیم نہیں کیا تھا کہ ان شناخت کی اقسام کو غیر مساوی کائناتوں کے ساتھ مل کر استعمال کیا جا سکتا ہے۔ خاص طور پر، یہ خیال کہ عدم مساوات کو صرف موجودہ مارٹن-لوف ٹائپ تھیوری میں ایک محوریہ شامل کرکے متعارف کرایا جاسکتا ہے صرف 2009 میں سامنے آیا۔ نیز 2009 میں، ووووڈسکی نے کان کمپلیکس میں ٹائپ تھیوری کے ماڈل کی مزید تفصیلات پر کام کیا، اور مشاہدہ کیا کہ ٹائپ تھیوری کے زمرہ جاتی ماڈلز کے لیے ہم آہنگی کے مسائل کو حل کرنے کے لیے ایک عالمگیر کان فائبرشن کا وجود استعمال کیا جا سکتا ہے۔ انہوں نے اے کے بوسفیلڈ کے ایک خیال کا استعمال کرتے ہوئے یہ بھی ثابت کیا کہ یہ عالمگیر ریشے غیر مساوی تھے: ریشوں کے درمیان جوڑی کے لحاظ سے ہوموٹوپی مساوات کا متعلقہ ریشے بیس کے پاتھ-اسپیس ریشے کے برابر ہے۔ یکسانیت کو ایک محوری کے طور پر وضع کرنے کے لیے ویووڈسکی نے "مساوات" کی نحو طور پر تعریف کرنے کا ایک طریقہ تلاش کیا جس میں یہ اہم خاصیت تھی کہ بیان "f ایک مساوات ہے" کی نمائندگی کرنے والی قسم (فنکشن ایکسٹینشنیلٹی کے مفروضے کے تحت) (-1)-ٹرنکیٹڈ (یعنی۔ معاہدہ اگر آباد ہو)۔ اس نے انہیں ہوفمین اور اسٹریچر کی "کائنات کی وسعت" کو اعلی جہتوں تک عام کرتے ہوئے، یکسانیت کا ایک نحو بیان دینے کے قابل بنایا۔ وہ پروف اسسٹنٹ Coq میں "مصنوعی ہوموٹوپی تھیوری" کی نمایاں مقدار کو تیار کرنا شروع کرنے کے لیے مساوات اور معاہدہ کی ان تعریفوں کو استعمال کرنے کے قابل بھی تھے۔ اس نے لائبریری کی بنیاد بنائی جسے بعد میں "فاؤنڈیشنز" اور بالآخر "یونی میتھ" کہا گیا۔ مختلف دھاگوں کے اتحاد کا آغاز فروری 2010 میں کارنیگی میلن یونیورسٹی میں ایک غیر رسمی میٹنگ کے ساتھ ہوا، جہاں ویووڈسکی نے کان کمپلیکس میں اپنا ماڈل اور اپنا کوک کوڈ ایک گروپ کو پیش کیا جس میں آوڈی، وارن، لمسڈین، رابرٹ ہارپر، ڈین لیکاٹا، مائیکل شولمین اور دیگر شامل تھے۔ اس میٹنگ نے ایک ثبوت کا خاکہ پیش کیا (وارن، لمسڈین، لیکاٹا، اور شولمین کی طرف سے) کہ ہر ہوموٹوپی مساوات ایک مساوات ہے (ووووڈسکی کے اچھے مربوط معنوں میں)، جو زمرہ کے نظریہ سے متعلق مساوات کو بہتر بنانے کے خیال پر مبنی ہے۔ اس کے فورا بعد، ووووڈسکی نے ثابت کیا کہ یکسانیت کا محور فنکشن کی وسعت کو ظاہر کرتا ہے۔ اگلی اہم تقریب مارچ 2011 میں میتھمیٹیکل ریسرچ انسٹی ٹیوٹ آف اوبرولفچ میں ایک منی ورکشاپ تھی جس کا اہتمام اسٹیو آوڈی، رچرڈ گارنر، پر مارٹن-لوف، اور ولادیمیر ووڈسکی نے کیا تھا، جس کا عنوان تھا "تعمیری ٹائپ تھیوری کی ہوموٹوپی تشریح"۔ اس ورکشاپ کے لیے ایک کوک ٹیوٹوریل کے حصے کے طور پر، آندرے باؤر نے ووڈسکی کے خیالات کی بنیاد پر ایک چھوٹی سی کوک لائبریری لکھی (لیکن حقیقت میں اس کا کوئی کوڈ استعمال نہیں کیا) ؛ یہ بالآخر "ہوٹ" کوک لائبریری کے پہلے ورژن کا دانا بن گیا (مائیکل شولمین کے مؤخر الذکر کا پہلا عزم نوٹ کرتا ہے کہ "آندرے باؤر کی فائلوں پر مبنی ترقی، ولادیمیر ووڈسکی کی فائلوں سے لیے گئے بہت سے خیالات کے ساتھ")۔ اوبرولفچ میٹنگ سے سامنے آنے والی سب سے اہم چیزوں میں سے ایک اعلی انڈکٹو اقسام کا بنیادی خیال تھا، جس کی وجہ لمسڈین، شولمین، باؤر اور وارن تھے۔ شرکاء نے اہم کھلے سوالات کی ایک فہرست بھی تیار کی، جیسے کہ آیا یکسانیت محوریت کو مطمئن کرتا ہے (اب بھی کھلا ہے، اگرچہ کچھ خاص معاملات کو مثبت طور پر حل کیا گیا ہے)، کیا یکسانیت محوری میں غیر معیاری ماڈل ہیں (چونکہ شولمین نے مثبت جواب دیا ہے)، اور (نیم) آسان اقسام کی وضاحت کیسے کی جائے (اب بھی ایم ایل ٹی ٹی میں کھلی ہے، حالانکہ یہ ووڈسکی کے ہوموٹوپی ٹائپ سسٹم (ایچ ٹی ایس) میں کیا جا سکتا ہے، جو کہ دو مساوات کی اقسام کے ساتھ ایک ٹائپ تھیوری ہے۔ اوبرولفچ ورکشاپ کے فورا بعد، ہوموٹوپی ٹائپ تھیوری ویب سائٹ اور بلاگ قائم کیا گیا، اور اس موضوع کو اسی نام سے مقبول ہونا شروع ہوا۔ اس عرصے کے دوران کچھ اہم پیش رفت کا اندازہ بلاگ کی تاریخ سے حاصل کیا جا سکتا ہے۔ غیر مساوی بنیادیں "غیر مساوی بنیادیں" کے جملے پر سب کی طرف سے اتفاق کیا گیا ہے کہ اس کا ہوموٹوپی ٹائپ تھیوری سے گہرا تعلق ہے، لیکن ہر کوئی اسے اسی طرح استعمال نہیں کرتا ہے۔ یہ اصل میں ولادیمیر ویووڈسکی نے ریاضی کے لیے ایک بنیادی نظام کے اپنے وژن کا حوالہ دینے کے لیے استعمال کیا تھا جس میں بنیادی اشیاء ہوموٹوپی کی اقسام ہیں، جو ایک ٹائپ تھیوری پر مبنی ہے جو یکسانیت محوری کو مطمئن کرتی ہے، اور کمپیوٹر پروف اسسٹنٹ میں باضابطہ ہوتی ہے۔ جیسے جیسے ویووڈسکی کا کام ہوموٹوپی ٹائپ تھیوری پر کام کرنے والے دیگر محققین کی کمیونٹی کے ساتھ مربوط ہوا، "غیر مساوی فاؤنڈیشنز" کو بعض اوقات "ہوموٹوپی ٹائپ تھیوری" کے ساتھ ایک دوسرے کے ساتھ استعمال کیا جاتا تھا، اور دیگر اوقات صرف اس کے استعمال کو بنیادی نظام کے طور پر حوالہ دینے کے لیے استعمال کیا جاتا تھا (مثال کے طور پر، ماڈل-زمرہ جاتی الفاظ یا کمپیوٹیشنل میٹا تھیوری کے مطالعہ کو چھوڑ کر)۔ مثال کے طور پر، آئی اے ایس کے خصوصی سال کے موضوع کو باضابطہ طور پر "غیر مساوی بنیادوں" کے طور پر دیا گیا تھا، حالانکہ وہاں کیے گئے بہت سے کام فاؤنڈیشنز کے علاوہ سیمنٹکس اور میٹا تھیوری پر مرکوز تھے۔ آئی اے ایس پروگرام میں شرکاء کی طرف سے تیار کردہ کتاب کا عنوان "ہوموٹوپی ٹائپ تھیوری: ریاضی کی غیر مساوی بنیادیں" تھا ؛ حالانکہ یہ دونوں میں سے کسی ایک کے استعمال کا حوالہ دے سکتا ہے، کیونکہ کتاب میں صرف ایچ او ٹی ٹی کو ریاضیاتی بنیاد کے طور پر بحث کی گئی ہے۔ انسٹی ٹیوٹ فار ایڈوانسڈ اسٹڈی کے محققین نے "ریاضی کی غیر مساوی بنیادوں پر ایک خصوصی سال" کا انعقاد کیا۔ اس خاص سال نے ٹوپولوجی، کمپیوٹر سائنس، کیٹیگری تھیوری اور ریاضیاتی منطق کے محققین کو اکٹھا کیا۔ اس پروگرام کا اہتمام اسٹیو آوڈی، تھیری کوکینڈ اور ولادیمیر ووووڈسکی نے کیا تھا۔ پروگرام کے دوران پیٹر ایکزل، جو شرکاء میں سے ایک تھے، نے ایک ورکنگ گروپ کا آغاز کیا جس نے ٹائپ تھیوری کو غیر رسمی لیکن سختی سے کرنے کے طریقے کی تحقیقات کی، ایک ایسے انداز میں جو سیٹ تھیوری کرنے والے عام ریاضی دانوں کے مترادف ہے۔ ابتدائی تجربات کے بعد یہ واضح ہو گیا کہ یہ نہ صرف ممکن تھا بلکہ انتہائی فائدہ مند بھی تھا، اور یہ کہ ایک کتاب (نام نہاد ایچ او ٹی ٹی بک) لکھی جا سکتی ہے اور لکھی جانی چاہیے۔ اس کے بعد پروجیکٹ کے بہت سے دوسرے شرکاء تکنیکی مدد، تحریر، پروف ریڈنگ، اور خیالات پیش کرنے کے ساتھ اس کوشش میں شامل ہوئے۔ غیر معمولی طور پر ریاضی کے متن کے لیے، اسے باہمی تعاون سے تیار کیا گیا تھا اور گٹ ہب پر کھلے میں، کریٹیو کامنز لائسنس کے تحت جاری کیا گیا ہے جو لوگوں کو کتاب کے اپنے ورژن کو فورک کرنے کی اجازت دیتا ہے، اور یہ پرنٹ اور ڈاؤن لوڈ دونوں میں مفت میں خریدا جا سکتا ہے۔ زیادہ عام طور پر، خصوصی سال پورے موضوع کی ترقی کے لیے ایک اتپریرک تھا ؛ ایچ او ٹی ٹی بک صرف ایک تھی، حالانکہ سب سے زیادہ نظر آنے والا نتیجہ۔ خصوصی سال میں سرکاری شرکاء پیٹر ایکزل بینیڈیکٹ آرنس تھورسٹن الٹینکرچ اسٹیو آوڈی برونو بارس آندرج باؤر یویس برٹوٹ مارک بیزم تھیری کوکونڈ ایرک فنسٹر ڈینیل گریسن ہیوگو ہربلین آندرے جوئل ڈین لیکاٹا پیٹر لمسڈین آسیہ مہبوبی پر مارٹن-لوف سرگئی میلیخوف الوارو پیلیو اینڈریو پولونسکی مائیکل شولمین میتھیو سوزو بیسیٹرز بینو وین ڈین برگ ولادیمیر ووڈسکی مائیکل وارن نوم زیلبرگر اے سی ایم کمپیوٹنگ ریویوز نے اس کتاب کو "ریاضی کی کمپیوٹنگ" کے زمرے میں 2013 کی ایک قابل ذکر اشاعت کے طور پر درج کیا۔ کلیدی تصورات "اقسام کے طور پر تجاویز" ایچ او ٹی ٹی ٹائپ تھیوری کی "اقسام کے طور پر تجاویز" کی تشریح کا ایک ترمیم شدہ ورژن استعمال کرتا ہے، جس کے مطابق اقسام بھی تجاویز کی نمائندگی کر سکتی ہیں اور اصطلاحات پھر ثبوت کی نمائندگی کر سکتی ہیں۔ تاہم، ایچ او ٹی ٹی میں، معیاری "اقسام کے طور پر تجاویز" کے برعکس، ایک خاص کردار "محض تجاویز" کے ذریعے ادا کیا جاتا ہے، جو، تقریبا بولتے ہوئے، وہ اقسام ہیں جن کی زیادہ سے زیادہ ایک اصطلاح ہوتی ہے، تجویز کردہ مساوات تک۔ یہ عام اقسام کے مقابلے میں روایتی منطقی تجاویز کی طرح ہیں، اس لحاظ سے کہ وہ ثبوت سے متعلق نہیں ہیں۔ مساوات ہوموٹوپی ٹائپ تھیوری کا بنیادی تصور راستہ ہے۔ ایچ او ٹی ٹی میں، قسم نقطہ سے نقطہ تک تمام راستوں کی قسم ہے۔ (لہذا، اس بات کا ثبوت کہ ایک نقطہ ایک نقطہ کے برابر ہے، وہی چیز ہے جو نقطہ سے نقطہ تک کا راستہ ہے۔) کسی بھی نقطہ کے لیے، ایک قسم کا راستہ موجود ہے، جو مساوات کی اضطراری خاصیت سے مطابقت رکھتا ہے۔ قسم کے راستے کو الٹا کیا جا سکتا ہے، جس سے قسم کا راستہ بنتا ہے، جو مساوات کی سمیٹرک پراپرٹی سے مطابقت رکھتا ہے۔ ریسپ قسم کے دو راستے۔ مربوط کیا جا سکتا ہے، قسم کا راستہ تشکیل دے سکتا ہے ؛ یہ مساوات کی عارضی خاصیت سے مطابقت رکھتا ہے۔ سب سے اہم بات یہ ہے کہ ایک راستہ، اور کسی جائیداد کے ثبوت کو دیکھتے ہوئے، جائیداد کا ثبوت پیش کرنے کے لیے ثبوت کو راستے میں "منتقل" کیا جا سکتا ہے۔ (مساوی طور پر بیان کیا گیا ہے، کسی قسم کی شے کو کسی قسم کی شے میں تبدیل کیا جا سکتا ہے۔) یہ مساوات کی متبادل ملکیت سے مطابقت رکھتا ہے۔ یہاں، ایچ او ٹی ٹی اور کلاسیکی ریاضی کے درمیان ایک اہم فرق آتا ہے۔ کلاسیکی ریاضی میں، ایک بار جب دو اقدار کی مساوات قائم ہو جاتی ہے، اور اس کے بعد ان کے درمیان کسی فرق کی پرواہ کیے بغیر ایک دوسرے کے ساتھ استعمال کیا جا سکتا ہے۔ ہوموٹوپی ٹائپ تھیوری میں، تاہم، متعدد مختلف راستے ہو سکتے ہیں، اور کسی شے کو دو مختلف راستوں پر لے جانے سے دو مختلف نتائج برآمد ہوں گے۔ لہذا، ہوموٹوپی ٹائپ تھیوری میں، متبادل پراپرٹی کا اطلاق کرتے وقت، یہ بتانا ضروری ہے کہ کون سا راستہ استعمال کیا جا رہا ہے۔ عام طور پر، ایک "تجویز" کے متعدد مختلف ثبوت ہو سکتے ہیں۔ (مثال کے طور پر، تمام قدرتی اعداد کی قسم، جب ایک تجویز کے طور پر سمجھا جاتا ہے، تو ہر قدرتی نمبر ثبوت کے طور پر ہوتا ہے۔) یہاں تک کہ اگر کسی تجویز کا صرف ایک ثبوت ہے، تو راستوں کی جگہ کسی نہ کسی طرح سے غیر معمولی ہو سکتی ہے۔ "محض تجویز" کوئی بھی قسم ہے جو یا تو خالی ہے، یا ایک معمولی راستے کی جگہ کے ساتھ صرف ایک نقطہ پر مشتمل ہے۔ نوٹ کریں کہ لوگ اس کے لیے لکھتے ہیں، اس طرح مضمر قسم کو چھوڑ دیتے ہیں۔ آئیڈینٹیٹی فنکشن کی نشاندہی کرتے ہوئے اس کے ساتھ الجھن میں نہ پڑیں۔ مساوات کی قسم دو اقسام اور کسی کائنات سے تعلق رکھنے والوں کو مساوی ہونے کے طور پر بیان کیا جاتا ہے اگر ان کے درمیان کوئی مساوات موجود ہو۔ مساوات ایک ایسی فنکشن ہے جس میں بائیں الٹا اور دائیں الٹا دونوں ہوتے ہیں، اس معنی میں کہ مناسب طور پر منتخب ہونے کے لیے اور درج ذیل اقسام دونوں آباد ہیں: یعنی۔ یہ مساوات کی اقسام کا استعمال کرتے ہوئے "بائیں الٹا اور دائیں الٹا دونوں ہے" کے عمومی تصور کو ظاہر کرتا ہے۔ نوٹ کریں کہ اوپر دیے گئے انورٹ ایبلٹی کنڈیشنز فنکشن کی اقسام اور میں مساوات کی اقسام ہیں۔ ایک عام طور پر فنکشن ایکسٹینشنیلٹی محور کو فرض کرتا ہے، جو اس بات کو یقینی بناتا ہے کہ یہ مندرجہ ذیل اقسام کے مساوی ہیں جو ڈومین اور کوڈومین پر مساوات کا استعمال کرتے ہوئے الٹا پن کا اظہار کرتے ہیں اور: یعنی۔ سب کے لیے اور، قسم کے افعال کو ایک ساتھ اس ثبوت کے ساتھ ظاہر کیا جاتا ہے کہ وہ مساوی ہیں۔ یکسانیت محوریہ ایسے افعال کی وضاحت کرنے کے بعد جو اوپر کی طرح مساوات ہیں، کوئی یہ ظاہر کر سکتا ہے کہ مساوات کی طرف راستوں کو موڑنے کا ایک مستند طریقہ ہے۔ دوسرے لفظوں میں، اس قسم کا ایک فنکشن ہے جو اس بات کا اظہار کرتا ہے کہ مساوی اقسام، خاص طور پر، مساوی بھی ہیں۔ یکسانیت محوری بیان کرتا ہے کہ یہ فعل خود ایک مساوات ہے۔ لہذا، ہمارے پاس "دوسرے لفظوں میں، شناخت مساوات کے مساوی ہے۔ خاص طور پر، کوئی یہ کہہ سکتا ہے کہ "مساوی اقسام ایک جیسی ہیں"۔ مارٹن ہوٹزل ایسکارڈو نے دکھایا ہے کہ یکسانیت کی خاصیت مارٹن-لوف ٹائپ تھیوری (ایم ایل ٹی ٹی) سے آزاد ہے۔ ایپلی کیشنز تھیوریم ثابت کرنے والے وکلاء کا دعوی ہے کہ ایچ او ٹی ٹی ریاضیاتی ثبوتوں کو کمپیوٹر پروف اسسٹنٹ کے لیے کمپیوٹر پروگرامنگ زبان میں پہلے سے کہیں زیادہ آسانی سے ترجمہ کرنے کی اجازت دیتا ہے۔ ان کا کہنا ہے کہ یہ نقطہ نظر کمپیوٹرز کے لیے مشکل ثبوتوں کی جانچ کرنے کی صلاحیت کو بڑھاتا ہے۔ تاہم، ان دعووں کو عالمی سطح پر قبول نہیں کیا جاتا ہے اور بہت سی تحقیقی کوششیں اور پروف اسسٹنٹ ایچ او ٹی ٹی کا استعمال نہیں کرتے ہیں۔ ایچ او ٹی ٹی یکسانیت کے محور کو اپناتا ہے، جو منطقی-ریاضیاتی تجاویز کی مساوات کو ہوموٹوپی تھیوری سے متعلق کرتا ہے۔ "a = b" جیسی مساوات ایک ریاضیاتی تجویز ہے جس میں دو مختلف علامتوں کی قدر ایک جیسی ہوتی ہے۔ ہوموٹوپی ٹائپ تھیوری میں، اس کا مطلب یہ لیا جاتا ہے کہ دو شکلیں جو علامتوں کی اقدار کی نمائندگی کرتی ہیں وہ ٹپوولوجیکل طور پر مساوی ہیں۔ ای ٹی ایچ زیورخ انسٹی ٹیوٹ فار تھیوریٹیکل اسٹڈیز کے ڈائریکٹر جیووانی فیلڈر کا کہنا ہے کہ یہ مساوات کے تعلقات ہوموٹوپی تھیوری میں بہتر طریقے سے وضع کیے جا سکتے ہیں کیونکہ یہ زیادہ جامع ہے: ہوموٹوپی تھیوری نہ صرف اس بات کی وضاحت کرتی ہے کہ "a برابر b" کیوں ہے بلکہ یہ بھی بتاتا ہے کہ اسے کیسے حاصل کیا جائے۔ سیٹ تھیوری میں، اس معلومات کو اضافی طور پر بیان کرنا ہوگا، جو وکلاء کا کہنا ہے کہ ریاضیاتی تجاویز کا پروگرامنگ زبانوں میں ترجمہ زیادہ مشکل بنا دیتا ہے۔ کمپیوٹر پروگرامنگ 2015 تک، ہوموٹوپی ٹائپ تھیوری میں یکسانیت محوری کے کمپیوٹیشنل رویے کو ماڈل اور باضابطہ طور پر تجزیہ کرنے کے لیے شدید تحقیقی کام جاری تھا۔ کیوبکل ٹائپ تھیوری ہوموٹوپی ٹائپ تھیوری کو کمپیوٹیشنل مواد دینے کی ایک کوشش ہے۔ تاہم، یہ خیال کیا جاتا ہے کہ بعض اشیاء، جیسے نیم آسان اقسام، قطعی مساوات کے کچھ تصور کے حوالے کے بغیر تعمیر نہیں کی جا سکتی ہیں۔ لہذا، مختلف دو سطحی قسم کے نظریات تیار کیے گئے ہیں جو اپنی اقسام کو ریشے دار اقسام میں تقسیم کرتے ہیں، جو راستوں کا احترام کرتے ہیں، اور غیر ریشے دار اقسام، جو نہیں کرتے ہیں۔ کارٹیسیئن کیوبکل کمپیوٹیشنل ٹائپ تھیوری پہلا دو سطحی قسم کا نظریہ ہے جو ہوموٹوپی ٹائپ تھیوری کو مکمل کمپیوٹیشنل تشریح فراہم کرتا ہے۔ تعمیرات کا حساب کتاب بھی دیکھیں کری-ہاورڈ خط و کتابت انٹوشنسٹک ٹائپ تھیوری ہوموٹوپی مفروضہ غیر مساوی فاؤنڈیشنز نوٹ حوالہ جات کتابچہ (اس مضمون میں حوالہ دیا گیا گٹ ہب ورژن)۔ بطور پی ڈی ایف۔ بطور پوسٹ اسکرپٹ۔ مزید پڑھنے کے لیے ڈیوڈ کورفیلڈ (2020)، موڈل ہوموٹوپی ٹائپ تھیوری: فلسفہ کے لیے ایک نئے منطق کا امکان، آکسفورڈ یونیورسٹی پریس۔ ایگبرٹ ریجکے (2022)، ہوموٹوپی ٹائپ تھیوری کا تعارف،۔ تعارفی نصابی کتاب۔ بیرونی روابط ہوموٹوپی ٹائپ تھیوری ویکی ولادیمیر ویووڈسکی کا ویب پیج غیر متزلزل فاؤنڈیشنز ہوموٹوپی ٹائپ تھیوری اور ریاضی کی غیر متزلزل فاؤنڈیشنز پر اسٹیو آوڈی کا "کنسٹرکٹو ٹائپ تھیوری اینڈ ہوموٹوپی"-انسٹی ٹیوٹ فار ایڈوانسڈ اسٹڈی لائبریریز آف فارملائزڈ میتھمیٹکس میں اسٹیو آوڈی کا ویڈیو لیکچر (اب یونی میتھ میں مربوط ہے، جہاں مزید ترقی ہوتی ہے) ریاضی ٹائپ تھیوری کی بنیادیں ہوموٹوپی تھیوری رسمی طریقے ویڈیو کلپس پر مشتمل مضامین