---

Step * of Lemma term-to-path-equal

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[u,v:{X ⊢ _:A}].
  ∀a:{X.𝕀 ⊢ _:(A)p}
    (∀[b:{X.𝕀 ⊢ _:(A)p}]. X ⊢ <>(a) = X ⊢ <>(b) ∈ {X ⊢ _:(Path_A u v)} supposing a = b ∈ {X.𝕀 ⊢ _:(A)p}) supposing 
       (X ⊢ (a)[0(𝕀)]=u:A and 
       X ⊢ (a)[1(𝕀)]=v:A)
BY
{ (InstLemma `term-to-path-wf` [] THEN RepeatFor 7 (ParallelLast')) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. u : {X ⊢ _:A}
4. v : {X ⊢ _:A}
5. a : {X.𝕀 ⊢ _:(A)p}
6. X ⊢ (a)[1(𝕀)]=v:A
7. X ⊢ (a)[0(𝕀)]=u:A
8. <>(a) ∈ {X ⊢ _:(Path_A u v)}
⊢ ∀[b:{X.𝕀 ⊢ _:(A)p}]. X ⊢ <>(a) = X ⊢ <>(b) ∈ {X ⊢ _:(Path_A u v)} supposing a = b ∈ {X.𝕀 ⊢ _:(A)p}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[u,v:\{X  \mvdash{}  \_:A\}].
    \mforall{}a:\{X.\mBbbI{}  \mvdash{}  \_:(A)p\}
        (\mforall{}[b:\{X.\mBbbI{}  \mvdash{}  \_:(A)p\}].  X  \mvdash{}  <>(a)  =  X  \mvdash{}  <>(b)  supposing  a  =  b)  supposing 
              (X  \mvdash{}  (a)[0(\mBbbI{})]=u:A  and 
              X  \mvdash{}  (a)[1(\mBbbI{})]=v:A)


By

---

Latex:
(InstLemma  `term-to-path-wf`  []  THEN  RepeatFor  7  (ParallelLast'))

---

Home Index