---

Step * of Lemma constant-Kan-type_wf

∀[X:KanCubicalSet]. ∀[Gamma:CubicalSet].  (constant-Kan-type(X) ∈ {Gamma ⊢ _(Kan)})
BY
{ (Auto THEN RepeatFor 2 (D 1) THEN MemTypeCD THEN Try (Unfold `constant-Kan-type` 0) THEN All Reduce THEN Auto) }

1
1. X1 : CubicalSet
2. X2 : I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X1;I;J;x;i) ⟶ X1(I)
3. Kan-filler(X1;X2)
4. uniform-Kan-filler(X1;X2)
5. Gamma : CubicalSet
⊢ Kan-A-filler(Gamma;(X1);λI,alpha. (X2 I))

2
1. X1 : CubicalSet
2. X2 : I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X1;I;J;x;i) ⟶ X1(I)
3. Kan-filler(X1;X2)
4. uniform-Kan-filler(X1;X2)
5. Gamma : CubicalSet
6. Kan-A-filler(Gamma;(X1);λI,alpha. (X2 I))
⊢ uniform-Kan-A-filler(Gamma;(X1);λI,alpha. (X2 I))

---

Latex:

---

Latex:
\mforall{}[X:KanCubicalSet].  \mforall{}[Gamma:CubicalSet].    (constant-Kan-type(X)  \mmember{}  \{Gamma  \mvdash{}  \_(Kan)\})


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  1)
  THEN  MemTypeCD
  THEN  Try  (Unfold  `constant-Kan-type`  0)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index