Step
*
1
1
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))
⊢ 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)))
BY
{ (((Assert I ∈ nameset(I) List BY
(Unfold `nameset` 0 THEN Auto))
THEN (Assert CnameDeq ∈ EqDecider(nameset(I)) BY
(Unfold `nameset` 0 THEN Auto))
)
THEN (Assert ((y:=a) o c1) ∈ name-morph(I;[]) BY
(Auto THEN SubsumeC ⌜name-morph([y / I];I)⌝⋅ THEN Auto))
THEN (Assert ((y:=a) o c2) ∈ name-morph(I;[]) BY
(Auto THEN SubsumeC ⌜name-morph([y / I];I)⌝⋅ THEN Auto))
THEN RecUnfold `poset_functor_extend` 0
THEN Subst' filter(λx.((((y:=a) o c1) x =z 0) ∧b (((y:=a) o c2) x =z 1));I)
~ filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) 0) }
1
.....equality.....
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;[])
⊢ filter(λx.((((y:=a) o c1) x =z 0) ∧b (((y:=a) o c2) x =z 1));I) ~ filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])
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)|| ≤ 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)))
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))
\mvdash{} 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)
By
Latex:
(((Assert I \mmember{} nameset(I) List BY
(Unfold `nameset` 0 THEN Auto))
THEN (Assert CnameDeq \mmember{} EqDecider(nameset(I)) BY
(Unfold `nameset` 0 THEN Auto))
)
THEN (Assert ((y:=a) o c1) \mmember{} name-morph(I;[]) BY
(Auto THEN SubsumeC \mkleeneopen{}name-morph([y / I];I)\mkleeneclose{}\mcdot{} THEN Auto))
THEN (Assert ((y:=a) o c2) \mmember{} name-morph(I;[]) BY
(Auto THEN SubsumeC \mkleeneopen{}name-morph([y / I];I)\mkleeneclose{}\mcdot{} THEN Auto))
THEN RecUnfold `poset\_functor\_extend` 0
THEN Subst' filter(\mlambda{}x.((((y:=a) o c1) x =\msubz{} 0) \mwedge{}\msubb{} (((y:=a) o c2) x =\msubz{} 1));I)
\msim{} filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]) 0)
Home
Index