---

Step * 3 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)))))
⊢ uniform-Kan-A-filler(X;discr(T);λI,alpha,J,x,i,bx. (snd(snd(hd(bx)))))
BY
{ (D 0 THEN Reduce 0 THEN Auto THEN RepUR ``A-open-box-image`` 0 THEN RepeatFor 2 (DVar `bx') THEN Reduce 0) }

1
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. A-adjacent-compatible(X;discr(T);I;alpha;[])
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈[]. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
  ∧ (∃f∈[]. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
  ∧ (∀f∈[].¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈[].(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈[].  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
⊢ (snd(snd(hd([]))) alpha f) = (snd(snd(hd([])))) ∈ discr(T)(f(alpha))

2
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))

---

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)))))
\mvdash{}  uniform-Kan-A-filler(X;discr(T);\mlambda{}I,alpha,J,x,i,bx.  (snd(snd(hd(bx)))))


By

---

Latex:
(D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``A-open-box-image``  0
  THEN  RepeatFor  2  (DVar  `bx')
  THEN  Reduce  0)

---

Home Index