Step
*
1
of Lemma
equipollent-function-product
1. A : Type
2. B : Type
3. C : Type
4. a1 : C ⟶ (A × B)@i
5. a2 : C ⟶ (A × B)@i
6. <λx.(fst((a1 x))), λx.(snd((a1 x)))> = <λx.(fst((a2 x))), λx.(snd((a2 x)))> ∈ (C ⟶ A × (C ⟶ B))@i
⊢ a1 = a2 ∈ (C ⟶ (A × B))
BY
{ ((Ext THEN Auto)
THEN (SplitPair (-2) THENA Auto)
THEN (ApFunToHypEquands `Z' ⌜Z x⌝ ⌜A⌝ (-2)⋅ THENA Auto)
THEN Reduce (-1)
THEN (ApFunToHypEquands `Z' ⌜Z x⌝ ⌜B⌝ (-2)⋅ THENA Auto)
THEN Reduce (-1)) }
1
1. A : Type
2. B : Type
3. C : Type
4. a1 : C ⟶ (A × B)@i
5. a2 : C ⟶ (A × B)@i
6. x : C
7. (λx.(fst((a1 x)))) = (λx.(fst((a2 x)))) ∈ (C ⟶ A)
8. (λx.(snd((a1 x)))) = (λx.(snd((a2 x)))) ∈ (C ⟶ B)
9. (fst((a1 x))) = (fst((a2 x))) ∈ A
10. (snd((a1 x))) = (snd((a2 x))) ∈ B
⊢ (a1 x) = (a2 x) ∈ (A × B)
Latex:
Latex:
1. A : Type
2. B : Type
3. C : Type
4. a1 : C {}\mrightarrow{} (A \mtimes{} B)@i
5. a2 : C {}\mrightarrow{} (A \mtimes{} B)@i
6. <\mlambda{}x.(fst((a1 x))), \mlambda{}x.(snd((a1 x)))> = <\mlambda{}x.(fst((a2 x))), \mlambda{}x.(snd((a2 x)))>@i
\mvdash{} a1 = a2
By
Latex:
((Ext THEN Auto)
THEN (SplitPair (-2) THENA Auto)
THEN (ApFunToHypEquands `Z' \mkleeneopen{}Z x\mkleeneclose{} \mkleeneopen{}A\mkleeneclose{} (-2)\mcdot{} THENA Auto)
THEN Reduce (-1)
THEN (ApFunToHypEquands `Z' \mkleeneopen{}Z x\mkleeneclose{} \mkleeneopen{}B\mkleeneclose{} (-2)\mcdot{} THENA Auto)
THEN Reduce (-1))
Home
Index