---

Step * 1 1 of Lemma cubical-path-app-1


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. t : I:fset(ℕ)
⟶ a@0:X(I)
⟶ {p:Path(A) | ∀I,alpha. ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha))}(a@0)
6. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a@0:X(I).
     ((t I a@0 a@0 f)
     = (t J f(a@0))
     ∈ {p:Path(A) | ∀I,alpha. ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha))}(f(a@0)))
7. I : fset(ℕ)
8. a1 : X(I)
⊢ (t I a1 I 1 1) = (b I a1) ∈ A(a1)
BY
{ ((GenConclTerm ⌜t I a1⌝⋅ THENM (RepUR ``cubical-type-at cubical-subset cubical-term-at`` -2 THEN D -2 THEN Auto))
   THENA (Auto THEN OnVar `p' (RepUR ``pathtype cubical-fun cubical-fun-family``) THEN Auto)
   ) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  t  :  I:fset(\mBbbN{})
{}\mrightarrow{}  a@0:X(I)
{}\mrightarrow{}  \{p:Path(A)  |  \mforall{}I,alpha.  ((p  I  1  0)  =  a(alpha))  \mwedge{}  ((p  I  1  1)  =  b(alpha))\}(a@0)
6.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a@0:X(I).    ((t  I  a@0  a@0  f)  =  (t  J  f(a@0)))
7.  I  :  fset(\mBbbN{})
8.  a1  :  X(I)
\mvdash{}  (t  I  a1  I  1  1)  =  (b  I  a1)


By

---

Latex:
((GenConclTerm  \mkleeneopen{}t  I  a1\mkleeneclose{}\mcdot{}
  THENM  (RepUR  ``cubical-type-at  cubical-subset  cubical-term-at``  -2  THEN  D  -2  THEN  Auto)
  )
  THENA  (Auto  THEN  OnVar  `p'  (RepUR  ``pathtype  cubical-fun  cubical-fun-family``)  THEN  Auto)
  )

---

Home Index