Step
*
1
1
2
3
1
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-[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 o (λf.((y:=a) o f))) c1) ((L o (λf.((y:=a) o f))) c2))
BY
{ (EqCD THEN Try (QuickAuto)) }
1
.....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))))
⊢ (L o (λf.((y:=a) o f))) = (L o (λf.((y:=a) o f))) ∈ (name-morph(I-[y];[]) ⟶ cat-ob(C))
2
.....subterm..... T:t
4: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))))
⊢ (λz,f. (E z ((y:=a) o f)))
= (λz,f. (E z ((y:=a) o f)))
∈ (i:nameset(I-[y])
⟶ c:{c:name-morph(I-[y];[])| (c i) = 0 ∈ ℕ2}
⟶ (cat-arrow(C) ((L o (λf.((y:=a) o f))) c) ((L o (λf.((y:=a) o f))) flip(c;i))))
3
.....subterm..... T:t
5: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))))
⊢ c1 = ((y:=a) o c1) ∈ name-morph(I-[y];[])
4
.....subterm..... T:t
6: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))))
⊢ c2 = ((y:=a) o c2) ∈ name-morph(I-[y];[])
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-[y];L o (\mlambda{}f.((y:=a) o f));\mlambda{}z,f. (E z ((y:=a) o f));c1;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))
By
Latex:
(EqCD THEN Try (QuickAuto))
Home
Index