---

Step * of Lemma Kan_id_filler_uniform

∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀a,b:{X ⊢ _:Kan-type(A)}.
  uniform-Kan-A-filler(X;(Id_Kan-type(A) a b);Kan_id_filler(X;A;a;b))
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. a : {X ⊢ _:Kan-type(A)}
4. b : {X ⊢ _:Kan-type(A)}
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. bx : A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
11. K : Cname List
12. f : name-morph(I;K)
13. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
14. ↑isname(f x)
⊢ (Kan_id_filler(X;A;a;b) I alpha J x i bx alpha f)
= (Kan_id_filler(X;A;a;b) K f(alpha) map(f;J) (f x) i A-open-box-image(X;(Id_Kan-type(A) a b);I;K;f;alpha;bx))
∈ (Id_Kan-type(A) a b)(f(alpha))

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_(Kan)\}.  \mforall{}a,b:\{X  \mvdash{}  \_:Kan-type(A)\}.
    uniform-Kan-A-filler(X;(Id\_Kan-type(A)  a  b);Kan\_id\_filler(X;A;a;b))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index