Step
*
of Lemma
equipollent-product-sum
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:a:A ⟶ B[a] ⟶ Type]. x:A ⟶ (y:B[x] × C[x;y]) ~ f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])
BY
{ (Auto
THEN (With ⌜λF.<λx.(fst((F x))), λx.(snd((F x)))>⌝ (D 0)⋅ THENA Auto)
THEN D 0
THEN RepUR ``inject surject`` 0
THEN Auto) }
1
1. A : Type
2. B : A ⟶ Type
3. C : a:A ⟶ B[a] ⟶ Type
4. a1 : x:A ⟶ (y:B[x] × C[x;y])
5. a2 : x:A ⟶ (y:B[x] × C[x;y])
6. <λx.(fst((a1 x))), λx.(snd((a1 x)))> = <λx.(fst((a2 x))), λx.(snd((a2 x)))> ∈ (f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x]))
⊢ a1 = a2 ∈ (x:A ⟶ (y:B[x] × C[x;y]))
2
1. [A] : Type
2. [B] : A ⟶ Type
3. [C] : a:A ⟶ B[a] ⟶ Type
4. b : f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])
⊢ ∃a:x:A ⟶ (y:B[x] × C[x;y]). (<λx.(fst((a x))), λx.(snd((a x)))> = b ∈ (f:a:A ⟶ B[a] × (x:A ⟶ C[x;f x])))
Latex:
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[C:a:A {}\mrightarrow{} B[a] {}\mrightarrow{} Type].
x:A {}\mrightarrow{} (y:B[x] \mtimes{} C[x;y]) \msim{} f:a:A {}\mrightarrow{} B[a] \mtimes{} (x:A {}\mrightarrow{} C[x;f x])
By
Latex:
(Auto
THEN (With \mkleeneopen{}\mlambda{}F.<\mlambda{}x.(fst((F x))), \mlambda{}x.(snd((F x)))>\mkleeneclose{} (D 0)\mcdot{} THENA Auto)
THEN D 0
THEN RepUR ``inject surject`` 0
THEN Auto)
Home
Index