---

Step * 1 1 of Lemma path-type-ext-eq


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. x : I:fset(ℕ) ⟶ a:X(I) ⟶ Path(A)(a)
6. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  ((x I a a f) = (x J f(a)) ∈ Path(A)(f(a)))
7. x @ 0(𝕀) = a ∈ {X ⊢ _:A}
8. x @ 1(𝕀) = b ∈ {X ⊢ _:A}
9. I : fset(ℕ)
10. alpha : X(I)
⊢ x I alpha ∈ {p:Path(A)(alpha)| ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha))} 
BY
{ (MemTypeCD THEN Auto THEN Try ((OnVar `p' (RepUR ``pathtype cubical-fun cubical-fun-family``) THEN Auto))) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. x : I:fset(ℕ) ⟶ a:X(I) ⟶ Path(A)(a)
6. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  ((x I a a f) = (x J f(a)) ∈ Path(A)(f(a)))
7. x @ 0(𝕀) = a ∈ {X ⊢ _:A}
8. x @ 1(𝕀) = b ∈ {X ⊢ _:A}
9. I : fset(ℕ)
10. alpha : X(I)
⊢ (x I alpha I 1 0) = a(alpha) ∈ A(alpha)

2
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. x : I:fset(ℕ) ⟶ a:X(I) ⟶ Path(A)(a)
6. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  ((x I a a f) = (x J f(a)) ∈ Path(A)(f(a)))
7. x @ 0(𝕀) = a ∈ {X ⊢ _:A}
8. x @ 1(𝕀) = b ∈ {X ⊢ _:A}
9. I : fset(ℕ)
10. alpha : X(I)
11. (x I alpha I 1 0) = a(alpha) ∈ A(alpha)
⊢ (x I alpha I 1 1) = b(alpha) ∈ A(alpha)

---

Latex:

---

Latex:

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


By

---

Latex:
(MemTypeCD
  THEN  Auto
  THEN  Try  ((OnVar  `p'  (RepUR  ``pathtype  cubical-fun  cubical-fun-family``)  THEN  Auto)))

---

Home Index