---

Step * of Lemma cubical-term-equal2

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[u,z:{X ⊢ _:A}].
  u = z ∈ {X ⊢ _:A} supposing ∀I:Cname List. ∀a:X(I).  ((u I a) = (z I a) ∈ ((fst(A)) I a))
BY
{ RepeatFor 3 (Intro) }

1
1. [X] : CubicalSet
2. [A] : {X ⊢ _}
3. [u] : {X ⊢ _:A}
⊢ ∀[z:{X ⊢ _:A}]. u = z ∈ {X ⊢ _:A} supposing ∀I:Cname List. ∀a:X(I).  ((u I a) = (z I a) ∈ ((fst(A)) I a))

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[u,z:\{X  \mvdash{}  \_:A\}].
    u  =  z  supposing  \mforall{}I:Cname  List.  \mforall{}a:X(I).    ((u  I  a)  =  (z  I  a))


By

---

Latex:
RepeatFor  3  (Intro)

---

Home Index