---

Step * of Lemma term-to-path_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}].  ∀a:{X.𝕀 ⊢ _:(A)p}. (<>(a) ∈ {X ⊢ _:(Path_A (a)[0(𝕀)] (a)[1(𝕀)])})
BY
{ (Intros
   THEN RepUR ``term-to-path path-type`` 0
   THEN (BLemma `cubical-subset-term` THEN Auto)
   THEN Try ((OnVar `p' (RepUR ``pathtype cubical-fun cubical-fun-family``) THEN Auto))) }

1
.....wf..... 
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X.𝕀 ⊢ _:(A)p}
⊢ (λa) ∈ {X ⊢ _:Path(A)}

2
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X.𝕀 ⊢ _:(A)p}
4. I : fset(ℕ)
5. alpha : X(I)
⊢ ((λa)(alpha) I 1 0) = (a)[0(𝕀)](alpha) ∈ A(alpha)

3
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X.𝕀 ⊢ _:(A)p}
4. I : fset(ℕ)
5. alpha : X(I)
6. ((λa)(alpha) I 1 0) = (a)[0(𝕀)](alpha) ∈ A(alpha)
⊢ ((λa)(alpha) I 1 1) = (a)[1(𝕀)](alpha) ∈ A(alpha)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].    \mforall{}a:\{X.\mBbbI{}  \mvdash{}  \_:(A)p\}.  (<>(a)  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  (a)[0(\mBbbI{})]  (a)[1(\mBbbI{})])\})


By

---

Latex:
(Intros
  THEN  RepUR  ``term-to-path  path-type``  0
  THEN  (BLemma  `cubical-subset-term`  THEN  Auto)
  THEN  Try  ((OnVar  `p'  (RepUR  ``pathtype  cubical-fun  cubical-fun-family``)  THEN  Auto)))

---

Home Index