Step
*
1
1
1
2
of Lemma
all-quotient-dependent
1. T : Type
2. c : T ⟶ Base
3. ∀x:T. (c x ∈ T ⋂ Base)
4. ∀x:T. ((c x) = x ∈ T)
5. S : T ⟶ ℙ
6. E : t:T ⟶ (S t) ⟶ (S t) ⟶ ℙ
7. ∀t:T. EquivRel(S t;a,b.E t a b)
8. f : t:T ⟶ (x,y:S t//(E t x y))
9. f,g:∀x:T ⋂ Base. (S x)//(∀x:T ⋂ Base. (↓E x (f x) (g x)))
⊢ f,g:∀t:T. (S t)//dep-fun-equiv(T;t,x,y.↓E t x y;f;g)
BY
{ (RenameVar `g' (-1)⋅
THEN UseWitness ⌜g o c⌝⋅
THEN (D -1 THENW (Auto THEN Try ((BLemma `dep-fun-equiv-rel` THEN EAuto 1))))) }
1
1. T : Type
2. c : T ⟶ Base
3. ∀x:T. (c x ∈ T ⋂ Base)
4. ∀x:T. ((c x) = x ∈ T)
5. S : T ⟶ ℙ
6. E : t:T ⟶ (S t) ⟶ (S t) ⟶ ℙ
7. ∀t:T. EquivRel(S t;a,b.E t a b)
8. f : t:T ⟶ (x,y:S t//(E t x y))
9. g : Base
10. g1 : Base
11. g = g1 ∈ pertype(λf,g. ((f ∈ ∀x:T ⋂ Base. (S x)) ∧ (g ∈ ∀x:T ⋂ Base. (S x)) ∧ (∀x:T ⋂ Base. (↓E x (f x) (g x)))))
12. g ∈ ∀x:T ⋂ Base. (S x)
13. g1 ∈ ∀x:T ⋂ Base. (S x)
14. ∀x:T ⋂ Base. (↓E x (g x) (g1 x))
⊢ (g o c) = (g1 o c) ∈ (f,g:∀t:T. (S t)//dep-fun-equiv(T;t,x,y.↓E t x y;f;g))
Latex:
Latex:
1. T : Type
2. c : T {}\mrightarrow{} Base
3. \mforall{}x:T. (c x \mmember{} T \mcap{} Base)
4. \mforall{}x:T. ((c x) = x)
5. S : T {}\mrightarrow{} \mBbbP{}
6. E : t:T {}\mrightarrow{} (S t) {}\mrightarrow{} (S t) {}\mrightarrow{} \mBbbP{}
7. \mforall{}t:T. EquivRel(S t;a,b.E t a b)
8. f : t:T {}\mrightarrow{} (x,y:S t//(E t x y))
9. f,g:\mforall{}x:T \mcap{} Base. (S x)//(\mforall{}x:T \mcap{} Base. (\mdownarrow{}E x (f x) (g x)))
\mvdash{} f,g:\mforall{}t:T. (S t)//dep-fun-equiv(T;t,x,y.\mdownarrow{}E t x y;f;g)
By
Latex:
(RenameVar `g' (-1)\mcdot{}
THEN UseWitness \mkleeneopen{}g o c\mkleeneclose{}\mcdot{}
THEN (D -1 THENW (Auto THEN Try ((BLemma `dep-fun-equiv-rel` THEN EAuto 1)))))
Home
Index