---

Step * of Lemma term-A-face_wf

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[i:ℕ2].
  (term-A-face(a;I;alpha;i) ∈ A-face(X;A;[fresh-cname(I) / I];iota(fresh-cname(I))(alpha)))
BY
{ (Auto THEN RepUR ``term-A-face A-face`` 0 THEN Auto) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. I : Cname List
5. alpha : X(I)
6. i : ℕ2
⊢ alpha = (iota(fresh-cname(I)) o (fresh-cname(I):=i))(alpha) ∈ X(I)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[i:\mBbbN{}2].
    (term-A-face(a;I;alpha;i)  \mmember{}  A-face(X;A;[fresh-cname(I)  /  I];iota(fresh-cname(I))(alpha)))


By

---

Latex:
(Auto  THEN  RepUR  ``term-A-face  A-face``  0  THEN  Auto)

---

Home Index