---

Step * of Lemma Kan-discrete_wf

∀[X:CubicalSet]. ∀[T:Type].  (Kan-discrete(T) ∈ {X ⊢ _(Kan)})
BY
{ (Auto THEN Unfold `Kan-discrete` 0 THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. X : CubicalSet
2. T : Type
3. I : Cname List
4. alpha : X(I)
5. J : nameset(I) List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-open-box(X;discr(T);I;alpha;J;x;i)
⊢ snd(snd(hd(bx))) ∈ discr(T)(alpha)

2
1. X : CubicalSet
2. T : Type
⊢ Kan-A-filler(X;discr(T);λI,alpha,J,x,i,bx. (snd(snd(hd(bx)))))

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

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[T:Type].    (Kan-discrete(T)  \mmember{}  \{X  \mvdash{}  \_(Kan)\})


By

---

Latex:
(Auto  THEN  Unfold  `Kan-discrete`  0  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index