اشتقاق نوع المنتج المزيل في نظرية النوع

Question

في كتاب Hott، القسم 1.5 (أنواع المنتج) من أجل تحديد المزيل لنوع المنتج، يفترض وظيفة من النوع $ g: a \ charnarrow b \ charnarrow c $ ثم يستمر في تحديد قاعدة المزيل، قائلا أننا نستطيع تحديد وظيفة $ f: a \ times b \ charnarrow c $ لأي مثل بواسطة:

$ f ((a، b)): \ equiv g (a) (b) $ .

ثم ينص على أنه

لاحظ أنه في نظرية التعيين، سنبرر التعريف أعلاه $ f $ بواسطة حقيقة أن كل عنصر من $ a \ times b $ هو زوج أمر، بحيث يكفي تحديد $ F $ على مثل هذه الأزواج. على النقيض من ذلك، فإن النظرية من النوع عكس الوضع: نفترض أن وظيفة على $ a \ times b $ محددة جيدا بمجرد تحديد قيمها على أزواج، و من هذا، سنكون قادرين على أثبت أن كل عنصر من عنصر $ a \ times b $ هو زوج.

هل توضح بمزيد من التفصيل ما تحاول الفقرة أعلاه؟

Answer 1

ما هو المقصود هنا، هو أنه يمكنك إنشاء تحديد الهوية $ x= (\ mathsf {pr} _1 (x)، \ mathsf {pr} _2 (x)) $ لأي $ x: a \ times b $ . بمعنى آخر، يمكنك إظهار $$ \ pi _ {(x: a \ times b)} x= (\ mathsf {pr} _1 (x)، \ mathsf {pr} _2 (س)). $$ من أجل القيام بذلك، نستخدم مبدأ التعريفي من $ a \ times b $ . من خلال مبدأ التعريفي الذي يكفي لإظهار أن $$ \ PI _ {(a: a)} \ pi _ {(b: b)} (a، b)= (\ mathsf {pr } _1 (a، b)، \ mathsf {pr} _2 (a، b)). $ الآن فقط تلاحظ ببساطة أنه من خلال تعريف خرائط الإسقاط، هناك المساواة في القضايا $ \ mathsf {pr} _1 (a، b) \ equiang a $ و $ \ mathsf {pr} _2 (a، b) \ equiV b $ . لذلك، يقلل النوع أعلاه إلى $$ \ PI _ {(a: a)} \ pi _ {(b: b)} (a، b)= (a، b)، $ $ والتي يمكن أن تثبت عن الانعكاس.

نستنتج أن كل عنصر من عنصر $ a \ times b $ يمكن تحديد مع زوج، وهما زوج من التوقعات الخاصة به وبعد وينطبق الشيء نفسه بالنسبة ل $ \ sigma _ {(x: a)} b (x) $ .