Step
*
1
1
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)|| ≤ n
12. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
13. I ∈ nameset(I) List
14. CnameDeq ∈ EqDecider(nameset(I))
15. ((y:=a) o c1) ∈ name-morph(I;[])
16. ((y:=a) o c2) ∈ name-morph(I;[])
⊢ eval d = filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) in
if null(d)
then cat-id(C) (L ((y:=a) o c1))
else cat-comp(C) (L ((y:=a) o c1)) (L flip(((y:=a) o c1);hd(d))) (L ((y:=a) o c2)) (E hd(d) ((y:=a) o c1))
poset_functor_extend(C;I;L;E;flip(((y:=a) o c1);hd(d));((y:=a) o c2))
fi
= eval d = filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) in
if null(d)
then cat-id(C) ((L o (λf.((y:=a) o f))) c1)
else cat-comp(C) ((L o (λf.((y:=a) o f))) c1) ((L o (λf.((y:=a) o f))) flip(c1;hd(d))) ((L o (λf.((y:=a) o f))) c2)
((λz,f. (E z ((y:=a) o f))) hd(d) 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(d));c2)
fi
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
BY
{ ((CallByValueReduce 0 THENA Auto) THEN (BoolCase ⌜null(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]))⌝⋅ THENA 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)|| ≤ n
12. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
13. I ∈ nameset(I) List
14. CnameDeq ∈ EqDecider(nameset(I))
15. ((y:=a) o c1) ∈ name-morph(I;[])
16. ((y:=a) o c2) ∈ name-morph(I;[])
17. filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) = [] ∈ (nameset(I) List)
⊢ (cat-id(C) (L ((y:=a) o c1))) = (cat-id(C) (L ((y:=a) o c1))) ∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
2
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)))
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. ||filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| \mleq{} n
12. \mforall{}x:nameset(I). ((c1 x) \mleq{} (c2 x))
13. I \mmember{} nameset(I) List
14. CnameDeq \mmember{} EqDecider(nameset(I))
15. ((y:=a) o c1) \mmember{} name-morph(I;[])
16. ((y:=a) o c2) \mmember{} name-morph(I;[])
\mvdash{} eval d = filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]) in
if null(d)
then cat-id(C) (L ((y:=a) o c1))
else cat-comp(C) (L ((y:=a) o c1)) (L flip(((y:=a) o c1);hd(d))) (L ((y:=a) o c2))
(E hd(d) ((y:=a) o c1))
poset\_functor\_extend(C;I;L;E;flip(((y:=a) o c1);hd(d));((y:=a) o c2))
fi
= eval d = filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]) in
if null(d)
then cat-id(C) ((L o (\mlambda{}f.((y:=a) o f))) c1)
else cat-comp(C) ((L o (\mlambda{}f.((y:=a) o f))) c1) ((L o (\mlambda{}f.((y:=a) o f))) flip(c1;hd(d)))
((L o (\mlambda{}f.((y:=a) o f))) c2)
((\mlambda{}z,f. (E z ((y:=a) o f))) hd(d) 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(d));c2\000C)
fi
By
Latex:
((CallByValueReduce 0 THENA Auto)
THEN (BoolCase \mkleeneopen{}null(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]))\mkleeneclose{}\mcdot{} THENA Auto)
)
Home
Index