Step
*
3
2
of Lemma
Kan-discrete_wf
1. X : CubicalSet
2. T : Type
3. Kan-A-filler(X;discr(T);λI,alpha,J,x,i,bx. (snd(snd(hd(bx)))))
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. u : A-face(X;discr(T);I;alpha)
10. v : A-face(X;discr(T);I;alpha) List
11. A-adjacent-compatible(X;discr(T);I;alpha;[u / v])
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2. (∃f∈[u / v]. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈[u / v]. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈[u / v].¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈[u / v].(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈[u / v]. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
12. K : Cname List
13. f : name-morph(I;K)
14. ∀i:nameset(I). ((i ∈ J)
⇒ (↑isname(f i)))
15. ↑isname(f x)
⊢ (snd(snd(u)) alpha f) = (snd(snd(A-face-image(X;discr(T);I;K;f;alpha;u)))) ∈ discr(T)(f(alpha))
BY
{ ((DVar `u' THEN DVar `u1')
THEN RepUR ``A-face-image cubical-type-ap-morph discrete-cubical-type cubical-type-at`` 0
THEN All (RepUR ``discrete-cubical-type cubical-type-at``)
THEN Auto) }
Latex:
Latex:
1. X : CubicalSet
2. T : Type
3. Kan-A-filler(X;discr(T);\mlambda{}I,alpha,J,x,i,bx. (snd(snd(hd(bx)))))
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : \mBbbN{}2
9. u : A-face(X;discr(T);I;alpha)
10. v : A-face(X;discr(T);I;alpha) List
11. A-adjacent-compatible(X;discr(T);I;alpha;[u / v])
\mwedge{} (\mneg{}(x \mmember{} J))
\mwedge{} l\_subset(Cname;J;I)
\mwedge{} ((\mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}[u / v]. A-face-name(f) = <y, c>))
\mwedge{} (\mexists{}f\mmember{}[u / v]. A-face-name(f) = <x, i>)
\mwedge{} (\mforall{}f\mmember{}[u / v].\mneg{}(A-face-name(f) = <x, 1 - i>)))
\mwedge{} (\mforall{}f\mmember{}[u / v].(fst(f) \mmember{} [x / J]))
\mwedge{} (\mforall{}f1,f2\mmember{}[u / v]. \mneg{}(A-face-name(f1) = A-face-name(f2)))
12. K : Cname List
13. f : name-morph(I;K)
14. \mforall{}i:nameset(I). ((i \mmember{} J) {}\mRightarrow{} (\muparrow{}isname(f i)))
15. \muparrow{}isname(f x)
\mvdash{} (snd(snd(u)) alpha f) = (snd(snd(A-face-image(X;discr(T);I;K;f;alpha;u))))
By
Latex:
((DVar `u' THEN DVar `u1')
THEN RepUR ``A-face-image cubical-type-ap-morph discrete-cubical-type cubical-type-at`` 0
THEN All (RepUR ``discrete-cubical-type cubical-type-at``)
THEN Auto)
Home
Index