理论中产品类型消除器的推导

Question

在Hott Book中，第1.5节（产品类型），以便为产品类型定义Eliminator，它假设 $ G：A \ Lightarrow B \ lightarrow C $的函数然后继续定义消除器规则，说我们可以定义一个函数 $ f：a \ times b \ lightarrow c $ 对于任何此类g通过：

$ 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 （x））。$$ 为此，我们使用 $ 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）\等于$ 和 $ \ mathsf {pr} _2（a，b）\ Equiv b $ 。因此，以上类型减少到<跨度类=“math-container”> $$ \ pi _ {（a：a）} \ pi _ {（b：b）}（a，b）=（a，b），$ $ 可以通过反射性证明。

我们得出的结论是，<跨度类=“math-container”> $ a \ times b $ 的每个元素都可以是用一对识别，即它自己的投影。 $ \ sigma _ {（x：a）} b（x）$ 相同。