Step
*
1
1
2
2
of Lemma
poset_functor_extend-face-map1
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : ℕ2
7. n : ℕ
8. ∀n:ℕn
∀[c1,c2:name-morph(I;[])].
((||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n)
⇒ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ¬(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) = [] ∈ (nameset(I) List))
12. ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n
13. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
14. I ∈ nameset(I) List
15. CnameDeq ∈ EqDecider(nameset(I))
16. ((y:=a) o c1) ∈ name-morph(I;[])
17. ((y:=a) o c2) ∈ name-morph(I;[])
⊢ (cat-comp(C) (L ((y:=a) o c1)) (L flip(((y:=a) o c1);hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]))))
(L ((y:=a) o c2))
(E hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])) ((y:=a) o c1))
poset_functor_extend(C;I;L;E;flip(((y:=a) o c1);hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])));((y:=a) o c2)))
= (cat-comp(C) (L ((y:=a) o c1)) (L ((y:=a) o flip(c1;hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])))))
(L ((y:=a) o c2))
(E hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])) ((y:=a) o c1))
poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));flip(c1;hd(filter(λx.((c1 x =z 0)
∧b (c2 x =z 1));
I-[y])));c2))
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
BY
{ ((InstLemma `filter_type` [⌜nameset(I)⌝;⌜λx.((c1 x =z 0) ∧b (c2 x =z 1))⌝;⌜I-[y]⌝]⋅
THENM (Reduce (-1) THEN GenConclTerm ⌜hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]))⌝⋅)
)
THENA (Auto THEN Unfold `nameset` 0 THEN Auto)
) }
1
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : ℕ2
7. n : ℕ
8. ∀n:ℕn
∀[c1,c2:name-morph(I;[])].
((||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n)
⇒ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ¬(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) = [] ∈ (nameset(I) List))
12. ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n
13. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
14. I ∈ nameset(I) List
15. CnameDeq ∈ EqDecider(nameset(I))
16. ((y:=a) o c1) ∈ name-morph(I;[])
17. ((y:=a) o c2) ∈ name-morph(I;[])
18. filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))} List
19. v : {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))}
20. hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])) = v ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))}
⊢ (cat-comp(C) (L ((y:=a) o c1)) (L flip(((y:=a) o c1);v)) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset_functor_extend(C;I;L;E;flip(((y:=a) o c1);v);((y:=a) o c2)))
= (cat-comp(C) (L ((y:=a) o c1)) (L ((y:=a) o flip(c1;v))) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));flip(c1;v);c2))
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
Latex:
Latex:
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) {}\mrightarrow{} cat-ob(C)
4. E : i:nameset(I) {}\mrightarrow{} c:\{c:name-morph(I;[])| (c i) = 0\} {}\mrightarrow{} (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : \mBbbN{}2
7. n : \mBbbN{}
8. \mforall{}n:\mBbbN{}n
\mforall{}[c1,c2:name-morph(I;[])].
((||filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| \mleq{} n)
{}\mRightarrow{} poset\_functor\_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset\_functor\_extend(C;I-[y];L o (\mlambda{}f.((y:=a) o f));\mlambda{}z,f. (E z ((y:=a) o f));c1;c2)
supposing \mforall{}x:nameset(I). ((c1 x) \mleq{} (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. \mneg{}(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]) = [])
12. ||filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| \mleq{} n
13. \mforall{}x:nameset(I). ((c1 x) \mleq{} (c2 x))
14. I \mmember{} nameset(I) List
15. CnameDeq \mmember{} EqDecider(nameset(I))
16. ((y:=a) o c1) \mmember{} name-morph(I;[])
17. ((y:=a) o c2) \mmember{} name-morph(I;[])
\mvdash{} (cat-comp(C) (L ((y:=a) o c1))
(L flip(((y:=a) o c1);hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]))))
(L ((y:=a) o c2))
(E hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y])) ((y:=a) o c1))
poset\_functor\_extend(C;I;L;E;flip(((y:=a) o c1);hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));
I-[y])));((y:=a) o c2)))
= (cat-comp(C) (L ((y:=a) o c1))
(L ((y:=a) o flip(c1;hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y])))))
(L ((y:=a) o c2))
(E hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y])) ((y:=a) o c1))
poset\_functor\_extend(C;I-[y];L o (\mlambda{}f.((y:=a) o f));
\mlambda{}z,f. (E z ((y:=a) o f));flip(c1;hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));
I-[y])));c2))
By
Latex:
((InstLemma `filter\_type` [\mkleeneopen{}nameset(I)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1))\mkleeneclose{};\mkleeneopen{}I-[y]\mkleeneclose{}]\mcdot{}
THENM (Reduce (-1) THEN GenConclTerm \mkleeneopen{}hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]))\mkleeneclose{}\mcdot{})
)
THENA (Auto THEN Unfold `nameset` 0 THEN Auto)
)
Home
Index