---

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

.....subterm..... T:t
1:n
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. x : {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = a ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = b ∈ {X ⊢ _:A})} 
⊢ x ∈ {X ⊢ _:(Path_A a b)}
BY
{ (RepeatFor 2 (D -1)
   THEN DVar `x'
   THEN (MemTypeCD THENW Auto)
   THEN RepUR ``path-type cubical-subset`` 0
   THEN ((RepeatFor 2 ((FunExt THENA Auto)) THEN RenameVar `alpha' (-1)) ORELSE 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 ∈ {p:Path(A)(alpha)| ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(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. J : fset(ℕ)
11. f : J ⟶ I
12. a@0 : X(I)
⊢ (x I a@0 a@0 f)
= (x J f(a@0))
∈ {p:Path(A)(f(a@0))| ((p J 1 0) = a(f(a@0)) ∈ A(f(a@0))) ∧ ((p J 1 1) = b(f(a@0)) ∈ A(f(a@0)))} 

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  x  :  \{t:\{X  \mvdash{}  \_:Path(A)\}|  (t  @  0(\mBbbI{})  =  a)  \mwedge{}  (t  @  1(\mBbbI{})  =  b)\} 
\mvdash{}  x  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  a  b)\}


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  DVar  `x'
  THEN  (MemTypeCD  THENW  Auto)
  THEN  RepUR  ``path-type  cubical-subset``  0
  THEN  ((RepeatFor  2  ((FunExt  THENA  Auto))  THEN  RenameVar  `alpha'  (-1))  ORELSE  Auto))

---

Home Index