Step
*
1
1
2
of Lemma
poset_functor_extend-face-map
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. ∀[c1,c2:name-morph(I;[])].
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))
8. c1 : name-morph(I-[y];[])
9. c2 : name-morph(I-[y];[])
10. ∀x:nameset(I-[y]). ((c1 x) ≤ (c2 x))
11. poset_functor_extend(C;I;L;E;((y:=a) o ((y:=a) o c1));((y:=a) o ((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));((y:=a) o c1);((y:=a) o c2))
∈ (cat-arrow(C) (L ((y:=a) o ((y:=a) o c1))) (L ((y:=a) o ((y:=a) o c2))))
⊢ 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
{ (NthHypEq (-1) THEN EqCD THEN Try (TrueCD)) }
1
.....subterm..... T:t
1:n
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. ∀[c1,c2:name-morph(I;[])].
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))
8. c1 : name-morph(I-[y];[])
9. c2 : name-morph(I-[y];[])
10. ∀x:nameset(I-[y]). ((c1 x) ≤ (c2 x))
11. poset_functor_extend(C;I;L;E;((y:=a) o ((y:=a) o c1));((y:=a) o ((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));((y:=a) o c1);((y:=a) o c2))
∈ (cat-arrow(C) (L ((y:=a) o ((y:=a) o c1))) (L ((y:=a) o ((y:=a) o c2))))
⊢ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
= (cat-arrow(C) (L ((y:=a) o ((y:=a) o c1))) (L ((y:=a) o ((y:=a) o c2))))
∈ Type
2
.....subterm..... T:t
2:n
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. ∀[c1,c2:name-morph(I;[])].
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))
8. c1 : name-morph(I-[y];[])
9. c2 : name-morph(I-[y];[])
10. ∀x:nameset(I-[y]). ((c1 x) ≤ (c2 x))
11. poset_functor_extend(C;I;L;E;((y:=a) o ((y:=a) o c1));((y:=a) o ((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));((y:=a) o c1);((y:=a) o c2))
∈ (cat-arrow(C) (L ((y:=a) o ((y:=a) o c1))) (L ((y:=a) o ((y:=a) o c2))))
⊢ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I;L;E;((y:=a) o ((y:=a) o c1));((y:=a) o ((y:=a) o c2)))
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
3
.....subterm..... T:t
3:n
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. ∀[c1,c2:name-morph(I;[])].
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))
8. c1 : name-morph(I-[y];[])
9. c2 : name-morph(I-[y];[])
10. ∀x:nameset(I-[y]). ((c1 x) ≤ (c2 x))
11. poset_functor_extend(C;I;L;E;((y:=a) o ((y:=a) o c1));((y:=a) o ((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));((y:=a) o c1);((y:=a) o c2))
∈ (cat-arrow(C) (L ((y:=a) o ((y:=a) o c1))) (L ((y:=a) o ((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)
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));((y:=a) o c1);((y:=a) o 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. \mforall{}[c1,c2:name-morph(I;[])].
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))
8. c1 : name-morph(I-[y];[])
9. c2 : name-morph(I-[y];[])
10. \mforall{}x:nameset(I-[y]). ((c1 x) \mleq{} (c2 x))
11. poset\_functor\_extend(C;I;L;E;((y:=a) o ((y:=a) o c1));((y:=a) o ((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));((y:=a) o c1);((y:=a) o c2))
\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:
(NthHypEq (-1) THEN EqCD THEN Try (TrueCD))
Home
Index