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)-বিচ্ছিন্ন (অর্থাৎ। বসবাসযোগ্য হলে চুক্তিবদ্ধ)। এটি তাকে একতার একটি বাক্যবিন্যাসমূলক বিবৃতি দিতে সক্ষম করে, হফম্যান এবং স্ট্রেইচারের "মহাবিশ্ব সম্প্রসারণ" কে উচ্চতর মাত্রায় সাধারণীকরণ করে। তিনি প্রুফ অ্যাসিস্ট্যান্ট কোক-এ উল্লেখযোগ্য পরিমাণে "সিন্থেটিক হোমোটপি তত্ত্ব" বিকাশ শুরু করতে সমতুল্যতা এবং চুক্তির এই সংজ্ঞাগুলি ব্যবহার করতে সক্ষম হয়েছিলেন; এটি গ্রন্থাগারের ভিত্তি গঠন করেছিল যা পরে "ফাউন্ডেশন" এবং অবশেষে "ইউনিম্যাথ" নামে পরিচিত হয়েছিল। 2010 সালের ফেব্রুয়ারিতে কার্নেগি মেলন বিশ্ববিদ্যালয়ে একটি অনানুষ্ঠানিক বৈঠকের মাধ্যমে বিভিন্ন সূত্রগুলির একীকরণ শুরু হয়, যেখানে ভোভডস্কি কান কমপ্লেক্সে তাঁর মডেল এবং আওডি, ওয়ারেন, লামসডাইন, রবার্ট হার্পার, ড্যান লিকাটা, মাইকেল শুলম্যান এবং অন্যান্যদের সহ একটি দলের কাছে তাঁর কোক কোড উপস্থাপন করেছিলেন। এই বৈঠকটি একটি প্রমাণের রূপরেখা তৈরি করেছিল (ওয়ারেন, লামসডাইন, লিকাটা এবং শুলম্যান দ্বারা) যে প্রতিটি সমস্থানিক সমতুল্যতা একটি সমতুল্য (ভোভোডস্কির ভাল সুসঙ্গত অর্থে), যা সমতুল্যতার সাথে সংলগ্ন সমতুল্যতার উন্নতির বিভাগ তত্ত্বের ধারণার উপর ভিত্তি করে। এর পরপরই, ভোয়েভডস্কি প্রমাণ করেছিলেন যে অভিন্ন স্বতঃসিদ্ধ সূত্রটি কার্যকারিতার সম্প্রসারণকে বোঝায়। পরবর্তী গুরুত্বপূর্ণ অনুষ্ঠানটি ছিল 2011 সালের মার্চ মাসে ওবারওয়ালফ্যাকের ম্যাথমেটিকাল রিসার্চ ইনস্টিটিউটে স্টিভ আওডি, রিচার্ড গার্নার, পার মার্টিন-লোফ এবং ভ্লাদিমির ভোভডস্কি দ্বারা আয়োজিত একটি মিনি-ওয়ার্কশপ, যার শিরোনাম ছিল "গঠনমূলক প্রকার তত্ত্বের হোমোটপি ব্যাখ্যা"। এই কর্মশালার জন্য একটি কোক টিউটোরিয়ালের অংশ হিসাবে, আন্দ্রেজ বাউয়ার ভোয়েভডস্কির ধারণার উপর ভিত্তি করে একটি ছোট কোক লাইব্রেরি লিখেছিলেন (তবে প্রকৃতপক্ষে তাঁর কোনও কোড ব্যবহার না করে); এটি শেষ পর্যন্ত "হোটিটি" কোক লাইব্রেরির প্রথম সংস্করণের কার্নেলে পরিণত হয়েছিল (মাইকেল শুলম্যানের পরেরটির প্রথম কমিট নোট করে "আন্দ্রেজ বাউয়ারের ফাইলের উপর ভিত্তি করে উন্নয়ন, ভ্লাদিমির ভোয়েভডস্কির ফাইল থেকে নেওয়া অনেক ধারণা সহ")। লামসডাইন, শুলম্যান, বাউয়ার এবং ওয়ারেনের কারণে ওবারওয়ালফ্যাকের সভা থেকে বেরিয়ে আসা সবচেয়ে গুরুত্বপূর্ণ বিষয়গুলির মধ্যে একটি ছিল উচ্চতর ইন্ডাক্টিভ প্রকারের মৌলিক ধারণা। অংশগ্রহণকারীরা গুরুত্বপূর্ণ উন্মুক্ত প্রশ্নের একটি তালিকাও তৈরি করেছিলেন, যেমন অভিন্নতা স্বতঃসিদ্ধটি ক্যানোনিকতাকে সন্তুষ্ট করে কিনা (এখনও খোলা, যদিও কিছু বিশেষ ক্ষেত্রে ইতিবাচকভাবে সমাধান করা হয়েছে), অভিন্নতা স্বতঃসিদ্ধটির অ-মানক মডেল রয়েছে কিনা (যেহেতু শুলম্যান দ্বারা ইতিবাচক উত্তর দেওয়া হয়েছে), এবং কীভাবে (আধা) সরল প্রকারগুলি সংজ্ঞায়িত করা যায় (এখনও এমএলটিটি-তে খোলা, যদিও এটি ভোভোডস্কির হোমোটপি টাইপ সিস্টেম (এইচটিএস)-এ করা যেতে পারে, যা দুটি সমতার ধরণের একটি টাইপ তত্ত্ব)। ওবারওয়ালফ্যাক কর্মশালার পরপরই, হোমোটপি টাইপ থিওরি ওয়েবসাইট এবং ব্লগ প্রতিষ্ঠিত হয় এবং সেই নামে বিষয়টি জনপ্রিয় হতে শুরু করে। এই সময়ের মধ্যে কিছু গুরুত্বপূর্ণ অগ্রগতির ধারণা ব্লগের ইতিহাস থেকে পাওয়া যেতে পারে। অভিন্ন ভিত্তি "অভিন্ন ভিত্তি" বাক্যাংশটি হোমোটপি টাইপ তত্ত্বের সাথে ঘনিষ্ঠভাবে সম্পর্কিত বলে সকলেই একমত, তবে সবাই এটিকে একইভাবে ব্যবহার করে না। এটি মূলত ভ্লাদিমির ভোয়েভডস্কি গণিতের জন্য একটি মৌলিক ব্যবস্থার তাঁর দৃষ্টিভঙ্গিকে বোঝাতে ব্যবহার করেছিলেন যেখানে মৌলিক বস্তুগুলি সমস্থানিক প্রকার, যা § অভিন্নতা স্বতঃসিদ্ধিকে সন্তুষ্ট করে এমন একটি প্রকার তত্ত্বের উপর ভিত্তি করে এবং একটি কম্পিউটার প্রুফ অ্যাসিস্ট্যান্ট-এ আনুষ্ঠানিক করা হয়। ভোভোডস্কির কাজটি হোমোটপি টাইপ তত্ত্বের উপর কাজ করা অন্যান্য গবেষকদের সম্প্রদায়ের সাথে একীভূত হওয়ার সাথে সাথে, "অভিন্ন ভিত্তি" কখনও কখনও "হোমোটপি টাইপ তত্ত্বের" সাথে বিনিময়যোগ্যভাবে ব্যবহৃত হত এবং অন্যান্য সময় শুধুমাত্র একটি ভিত্তি ব্যবস্থা হিসাবে এর ব্যবহারকে বোঝাতে ব্যবহৃত হত (উদাহরণস্বরূপ, মডেল-বিভাগগত শব্দার্থবিজ্ঞান বা গণনামূলক মেটাথেরির অধ্যয়ন বাদে)। উদাহরণস্বরূপ, আইএএস বিশেষ বছরের বিষয়টিকে আনুষ্ঠানিকভাবে "অভিন্ন ভিত্তি" হিসাবে দেওয়া হয়েছিল, যদিও সেখানে করা অনেক কাজ ভিত্তি ছাড়াও শব্দার্থবিজ্ঞান এবং মেটাথেরির উপর দৃষ্টি নিবদ্ধ করে। আইএএস প্রোগ্রামে অংশগ্রহণকারীদের দ্বারা উত্পাদিত বইটির শিরোনাম ছিল "হোমোটপি টাইপ থিওরিঃ গণিতের অবিচ্ছেদ্য ভিত্তি"; যদিও এটি উভয় ব্যবহারের উল্লেখ করতে পারে, কারণ বইটি শুধুমাত্র এইচওটিটি-কে গাণিতিক ভিত্তি হিসাবে আলোচনা করে। ইনস্টিটিউট ফর অ্যাডভান্সড স্টাডির গবেষকরা "গণিতের অভিন্ন ভিত্তির উপর একটি বিশেষ বছর" অনুষ্ঠিত করেছেন। বিশেষ বছরটি টপোলজি, কম্পিউটার বিজ্ঞান, বিভাগ তত্ত্ব এবং গাণিতিক যুক্তির গবেষকদের একত্রিত করে। স্টিভ আওডি, থিয়েরি কোকুয়ান্ড এবং ভ্লাদিমির ভোয়েভডস্কি এই অনুষ্ঠানের আয়োজন করেছিলেন। প্রোগ্রাম চলাকালীন পিটার অ্যাজেল, যিনি অংশগ্রহণকারীদের মধ্যে একজন ছিলেন, একটি ওয়ার্কিং গ্রুপের সূচনা করেছিলেন যা টাইপ তত্ত্বটি অনানুষ্ঠানিকভাবে কিন্তু কঠোরভাবে কীভাবে করা যায় তা তদন্ত করেছিল, এমন একটি শৈলীতে যা সাধারণ গণিতবিদদের সেট তত্ত্বের অনুরূপ। প্রাথমিক পরীক্ষার পরে এটি স্পষ্ট হয়ে ওঠে যে এটি কেবল সম্ভবই নয়, অত্যন্ত উপকারী এবং একটি বই (তথাকথিত এইচওটিটি বই) লেখা যেতে পারে এবং করা উচিত। প্রকল্পের অন্যান্য অনেক অংশগ্রহণকারী তখন প্রযুক্তিগত সহায়তা, লেখা, প্রুফ রিডিং এবং ধারণার প্রস্তাব দিয়ে এই প্রচেষ্টায় যোগ দেন। গণিতের পাঠ্যের জন্য অস্বাভাবিকভাবে, এটি সহযোগিতামূলকভাবে এবং গিটহাব-এ উন্মুক্তভাবে তৈরি করা হয়েছিল, এটি ক্রিয়েটিভ কমন্স লাইসেন্সের অধীনে প্রকাশিত হয়েছে যা লোকেদের বইয়ের নিজস্ব সংস্করণটি কাঁটাচামচ করার অনুমতি দেয় এবং এটি মুদ্রণ এবং ডাউনলোড উভয় ক্ষেত্রেই বিনামূল্যে ক্রয়যোগ্য। আরও সাধারণভাবে, বিশেষ বছরটি পুরো বিষয়টির বিকাশের জন্য একটি অনুঘটক ছিল; এইচওটিটি বইটি কেবল একটি ছিল, যদিও সবচেয়ে দৃশ্যমান, ফলাফল। বিশেষ বছরে সরকারী অংশগ্রহণকারীরা পিটার অ্যাজেল বেনেডিক্ট আহরেনস থর্স্টেন আলটেনকির্চ স্টিভ আওডি ব্রুনো বারাস আন্দ্রেজ বাউয়ার ইভস বার্টোট মার্ক বেজেম থিয়েরি কোকুয়ান্ড এরিক ফিনস্টার ড্যানিয়েল গ্রেসন হুগো হার্বেলিন আন্দ্রে জোয়েল ড্যান লিকাটা পিটার লামসডাইন আসিয়া মাহবুবি পার মার্টিন-লোফ সের্গেই মেলিখভ আলভারো পেলায়ো অ্যান্ড্রু পোলনস্কি মাইকেল শুলম্যান ম্যাথিউ সোজেউ স্পিটার্স বেনো ভ্যান ডেন বার্গ ভ্লাদিমির ভোয়েভোডস্কি মাইকেল ওয়ারেন নোম জেইলবার্গার এসিএম কম্পিউটিং রিভিউ বইটিকে "কম্পিউটিংয়ের গণিত" বিভাগে 2013 সালের একটি উল্লেখযোগ্য প্রকাশনা হিসাবে তালিকাভুক্ত করেছে। মূল ধারণাগুলি "প্রকার হিসাবে প্রস্তাব" এইচওটিটি প্রকার তত্ত্বের "প্রকার হিসাবে প্রস্তাব" ব্যাখ্যার একটি পরিবর্তিত সংস্করণ ব্যবহার করে, যা অনুসারে প্রকারগুলি প্রস্তাবও উপস্থাপন করতে পারে এবং পদগুলি তখন প্রমাণ উপস্থাপন করতে পারে। তবে, এইচ. ও. টি. টি-তে, প্রমিত "প্রকার হিসাবে প্রস্তাব"-এর বিপরীতে, 'নিছক প্রস্তাব' দ্বারা একটি বিশেষ ভূমিকা পালন করা হয়, যা মোটামুটিভাবে বলতে গেলে, প্রস্তাবমূলক সমতা পর্যন্ত সর্বাধিক একটি শব্দ রয়েছে। এগুলি সাধারণ প্রকারের তুলনায় প্রচলিত যৌক্তিক প্রস্তাবের মতো, কারণ এগুলি প্রমাণ-অপ্রাসঙ্গিক। সমতা হোমোটপি টাইপ তত্ত্বের মৌলিক ধারণা হল পথ। এইচওটিটি-তে, প্রকারটি হল বিন্দু থেকে বিন্দু পর্যন্ত সমস্ত পথের প্রকার। (অতএব, একটি বিন্দু যে একটি বিন্দুর সমান তার প্রমাণ বিন্দু থেকে বিন্দু পর্যন্ত পথের সমান।) যে কোনও বিন্দুর জন্য, সমতার প্রতিফলিত বৈশিষ্ট্যের সাথে সামঞ্জস্যপূর্ণ ধরনের একটি পথ রয়েছে। সমতার প্রতিসম বৈশিষ্ট্যের সাথে সামঞ্জস্য রেখে একটি প্রকারের পথ গঠন করে একটি প্রকারের পথকে উল্টানো যেতে পারে। রেসপ টাইপের দুটি পথ। সংহত করা যেতে পারে, প্রকারের একটি পথ গঠন করে; এটি সমতার ক্ষণস্থায়ী বৈশিষ্ট্যের সাথে মিলে যায়। সবচেয়ে গুরুত্বপূর্ণ বিষয় হল, একটি পথ এবং কিছু সম্পত্তির প্রমাণ দেওয়া হলে, সম্পত্তির প্রমাণ দেওয়ার জন্য প্রমাণটি পথে "পরিবহন" করা যেতে পারে। (সমতুল্যভাবে বলা যায়, একটি ধরনের বস্তুকে একটি ধরনের বস্তুতে পরিণত করা যেতে পারে।) এটি সমতার প্রতিস্থাপন সম্পত্তির সাথে মিলে যায়। এখানে, এইচওটিটি এবং শাস্ত্রীয় গণিতের মধ্যে একটি গুরুত্বপূর্ণ পার্থক্য রয়েছে। ধ্রুপদী গণিতে, একবার দুটি মানের সমতা প্রতিষ্ঠিত হয়েছে এবং তারপরে তাদের মধ্যে কোনও পার্থক্য বিবেচনা না করে বিনিময়যোগ্যভাবে ব্যবহার করা যেতে পারে। হোমোটপি টাইপ তত্ত্বে, তবে, একাধিক ভিন্ন পথ থাকতে পারে এবং দুটি ভিন্ন পথ ধরে একটি বস্তুর পরিবহন দুটি ভিন্ন ফলাফল দেবে। অতএব, হোমোটপি টাইপ তত্ত্বে, প্রতিস্থাপন বৈশিষ্ট্য প্রয়োগ করার সময়, কোন পথটি ব্যবহার করা হচ্ছে তা উল্লেখ করা প্রয়োজন। সাধারণভাবে, একটি "প্রস্তাব"-এর একাধিক ভিন্ন প্রমাণ থাকতে পারে। (উদাহরণস্বরূপ, সমস্ত স্বাভাবিক সংখ্যার ধরন, যখন একটি প্রস্তাব হিসাবে বিবেচিত হয়, তখন প্রমাণ হিসাবে প্রতিটি প্রাকৃতিক সংখ্যা থাকে।) এমনকি যদি কোনও প্রস্তাবের একটি মাত্র প্রমাণ থাকে, তবে পথের স্থান কোনও না কোনওভাবে তুচ্ছ হতে পারে। একটি "নিছক প্রস্তাব" হল এমন কোনও প্রকার যা হয় খালি, অথবা একটি তুচ্ছ পথের স্থান সহ শুধুমাত্র একটি বিন্দু ধারণ করে। লক্ষ্য করুন যে লোকেরা এর জন্য লেখে, যার ফলে অন্তর্নিহিত প্রকারটি রয়ে যায়। আইডেন্টিটি ফাংশনকে নির্দেশ করে এটিকে বিভ্রান্ত করবেন না। দুই ধরনের এবং কোনো মহাবিশ্বের অন্তর্গতকে সমতুল্য হিসাবে সংজ্ঞায়িত করা হয় যদি তাদের মধ্যে সমতুল্যতা বিদ্যমান থাকে। সমতুল্যতা এমন একটি ফাংশন যার বাম বিপরীত এবং ডান বিপরীত উভয়ই রয়েছে, এই অর্থে যে উপযুক্তভাবে নির্বাচিত হওয়ার জন্য এবং নিম্নলিখিত প্রকারগুলি উভয়ই বসবাস করেঃ এটি সমতার ধরন ব্যবহার করে "বাম বিপরীত এবং ডান বিপরীত উভয়ই রয়েছে"-এর একটি সাধারণ ধারণা প্রকাশ করে। লক্ষ্য করুন যে উপরের ইনভার্টিবিলিটি শর্তগুলি ফাংশনের ধরণ এবং-এ সমতার প্রকার। একটি সাধারণভাবে ফাংশন এক্সটেনশনালিটি স্বতঃসিদ্ধ অনুমান করে, যা নিশ্চিত করে যে এগুলি নিম্নলিখিত প্রকারের সমতুল্য যা ডোমেন এবং কোডোমেইনের সমতা ব্যবহার করে বিপরীততা প্রকাশ করেঃ সকলের জন্য এবং, প্রকারের ফাংশনগুলি একটি প্রমাণ সহ যে তারা সমতুল্য দ্বারা চিহ্নিত করা হয়। অভিন্নতা স্বতঃসিদ্ধ উপরে বর্ণিত সমতুল্য ফাংশনগুলি সংজ্ঞায়িত করা থাকলে, কেউ দেখাতে পারে যে সমতুল্যতার দিকে পথ ঘুরিয়ে দেওয়ার একটি প্রামাণিক উপায় রয়েছে। অন্য কথায়, এই ধরনের একটি ফাংশন রয়েছে যা প্রকাশ করে যে যে প্রকারগুলি সমান, সেগুলিও বিশেষভাবে সমতুল্য। অভিন্ন স্বতঃসিদ্ধ বলে যে এই ফাংশন নিজেই একটি সমতুল্য। অতএব, আমাদের আছে "অন্য কথায়, পরিচয় সমতুল্য। বিশেষ করে, কেউ বলতে পারে যে 'সমতুল্য প্রকারগুলি অভিন্ন'। মার্টিন হটজেল এসকার্ডো দেখিয়েছেন যে, অভিন্নতার বৈশিষ্ট্য মার্টিন-লোফ টাইপ থিওরি (এমএলটিটি) থেকে স্বাধীন। অ্যাপ্লিকেশন তত্ত্ব প্রমাণকারী উকিলরা দাবি করেন যে এইচওটিটি গাণিতিক প্রমাণগুলিকে কম্পিউটার প্রুফ অ্যাসিস্ট্যান্টদের জন্য কম্পিউটার প্রোগ্রামিং ভাষায় অনুবাদ করার অনুমতি দেয় যা আগের তুলনায় অনেক সহজ। তারা যুক্তি দেয় যে এই পদ্ধতিটি কম্পিউটারের পক্ষে কঠিন প্রমাণগুলি পরীক্ষা করার সম্ভাবনা বাড়ায়। যাইহোক, এই দাবিগুলি সর্বজনীনভাবে গৃহীত হয় না এবং অনেক গবেষণা প্রচেষ্টা এবং প্রমাণ সহকারীরা এইচওটিটি ব্যবহার করে না। এইচওটিটি অভিন্ন স্বতঃসিদ্ধ গ্রহণ করে, যা যৌক্তিক-গাণিতিক প্রস্তাবের সমতার সাথে সমস্থানিক তত্ত্বের সম্পর্কযুক্ত। "a = b"-এর মতো একটি সমীকরণ হল একটি গাণিতিক প্রস্তাব যেখানে দুটি ভিন্ন প্রতীকের একই মান থাকে। হোমোটপি টাইপ তত্ত্বে, এর অর্থ ধরা হয় যে দুটি আকৃতি যা প্রতীকগুলির মানকে উপস্থাপন করে তা টপোলজিক্যালি সমতুল্য। ই. টি. এইচ জুরিখ ইনস্টিটিউট ফর থিওরিটিক্যাল স্টাডিজের পরিচালক জিওভান্নি ফেল্ডার যুক্তি দেখান যে, এই সমতুল্য সম্পর্কগুলি হোমোটপি তত্ত্বে আরও ভালভাবে প্রণয়ন করা যেতে পারে কারণ এটি আরও বিস্তৃতঃ হোমোটপি তত্ত্ব কেবল "এ সমান বি" কেন নয়, এটি কীভাবে বের করা যায় তাও ব্যাখ্যা করে। সেট তত্ত্বে, এই তথ্যকে অতিরিক্তভাবে সংজ্ঞায়িত করতে হবে, যা, সমর্থকদের যুক্তি, প্রোগ্রামিং ভাষায় গাণিতিক প্রস্তাবগুলির অনুবাদকে আরও কঠিন করে তোলে। 2015 সাল পর্যন্ত, হোমোটপি টাইপ তত্ত্বে অভিন্ন স্বতঃসিদ্ধের গণনামূলক আচরণের মডেল এবং আনুষ্ঠানিকভাবে বিশ্লেষণ করার জন্য তীব্র গবেষণা কাজ চলছে। কিউবিক্যাল টাইপ তত্ত্ব হল হোমোটপি টাইপ তত্ত্বকে গণনামূলক বিষয়বস্তু দেওয়ার একটি প্রচেষ্টা। যাইহোক, এটি বিশ্বাস করা হয় যে নির্দিষ্ট কিছু বস্তু, যেমন আধা-সরল প্রকার, সঠিক সমতার কিছু ধারণার উল্লেখ ছাড়া নির্মাণ করা যায় না। অতএব, বিভিন্ন দ্বি-স্তরের তত্ত্ব তৈরি করা হয়েছে যা তাদের প্রকারগুলিকে তন্তুযুক্ত প্রকারগুলিতে বিভক্ত করে, যা পথকে সম্মান করে এবং অ-তন্তুযুক্ত প্রকার, যা করে না। কার্টেসিয়ান কিউবিকাল গণনামূলক প্রকার তত্ত্ব হল প্রথম দ্বি-স্তরের প্রকার তত্ত্ব যা হোমোটপি প্রকার তত্ত্বকে একটি সম্পূর্ণ গণনামূলক ব্যাখ্যা দেয়। এছাড়াও দেখুন ক্যালকুলাস অফ কনস্ট্রাকশনস কারি-হাওয়ার্ড করেসপন্ডেন্স ইন্টুইশনিস্ট টাইপ থিওরি হোমোটোপি হাইপোথিসিস ইউনিভ্যালেন্ট ফাউন্ডেশনস নোটস রেফারেন্স বিব্লিওগ্রাফি (এই নিবন্ধে উদ্ধৃত গিটহাব সংস্করণ)। পিডিএফ হিসেবে। পোস্টস্ক্রিপ্ট হিসাবে। ডেভিড করফিল্ড (2020), মডেল হোমোটোপি টাইপ থিওরিঃ দ্য প্রসপেক্ট অফ এ নিউ লজিক ফর ফিলোসফি, অক্সফোর্ড ইউনিভার্সিটি প্রেস। এগবার্ট রিজকে (2022), হোমোটোপি টাইপ তত্ত্বের ভূমিকা। প্রারম্ভিক পাঠ্যপুস্তক। বহিরাগত লিঙ্ক হোমোটোপি টাইপ থিওরি উইকি ভ্লাদিমির ভোয়েভোডস্কির ওয়েবপেজ অন দ্য ইউনিভ্যালেন্ট ফাউন্ডেশনস হোমোটোপি টাইপ থিওরি অ্যান্ড দ্য ইউনিভ্যালেন্ট ফাউন্ডেশনস অফ ম্যাথমেটিক্স স্টিভ আওডের "কনস্ট্রাকটিভ টাইপ থিওরি অ্যান্ড হোমোটোপি"-ইনস্টিটিউট ফর অ্যাডভান্সড স্টাডি লাইব্রেরি অফ ফর্মালাইজড ম্যাথমেটিক্সে স্টিভ আওডের ভিডিও বক্তৃতা (এখন ইউনিম্যাথের সাথে একীভূত, যেখানে আরও উন্নয়ন ঘটে) গণিতের ভিত্তি টাইপ তত্ত্ব হোমোটোপি ফর্মাল পদ্ধতি ফর্মাল পদ্ধতি ভিডিও ক্লিপযুক্ত নিবন্ধ