---

Step * 1 2 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. 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)))} 
BY
{ (EqTypeCD 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. J : fset(ℕ)
11. f : J ⟶ I
12. a@0 : X(I)
⊢ ((x I a@0 a@0 f) J 1 0) = a(f(a@0)) ∈ A(f(a@0))

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)
13. ((x I a@0 a@0 f) J 1 0) = a(f(a@0)) ∈ A(f(a@0))
⊢ ((x I a@0 a@0 f) J 1 1) = b(f(a@0)) ∈ A(f(a@0))

---

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.  J  :  fset(\mBbbN{})
11.  f  :  J  {}\mrightarrow{}  I
12.  a@0  :  X(I)
\mvdash{}  (x  I  a@0  a@0  f)  =  (x  J  f(a@0))


By

---

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

---

Home Index