---

Step * 1 1 of Lemma unit-pathtype


1. G : CubicalSet{j}
2. a : I:fset(ℕ) ⟶ a:G(I) ⟶ Path(1)(a)
3. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a@0:G(I).  ((a I a@0 a@0 f) = (a J f(a@0)) ∈ Path(1)(f(a@0)))
4. b : I:fset(ℕ) ⟶ a:G(I) ⟶ Path(1)(a)
5. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:G(I).  ((b I a a f) = (b J f(a)) ∈ Path(1)(f(a)))
6. I : fset(ℕ)
7. a1 : G(I)
⊢ (a I a1) = (b I a1) ∈ Path(1)(a1)
BY
{ All (RepUR ``pathtype cubical-fun cubical-fun-family``) }

1
1. G : CubicalSet{j}
2. a : I:fset(ℕ)
⟶ a:G(I)
⟶ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:𝕀(f(a)) ⟶ 1(f(a))| 
    ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:𝕀(f(a)).  ((w J f u f(a) g) = (w K f ⋅ g (u f(a) g)) ∈ 1(g(f(a))))} 
3. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a@0:G(I).
     ((λK,g. (a I a@0 K f ⋅ g))
     = (a J f(a@0))
     ∈ {w:J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ J ⟶ u:𝕀(f@0(f(a@0))) ⟶ 1(f@0(f(a@0)))| 
        ∀J@0,K:fset(ℕ). ∀f@0:J@0 ⟶ J. ∀g:K ⟶ J@0. ∀u:𝕀(f@0(f(a@0))).
          ((w J@0 f@0 u f@0(f(a@0)) g) = (w K f@0 ⋅ g (u f@0(f(a@0)) g)) ∈ 1(g(f@0(f(a@0)))))} )
4. b : I:fset(ℕ)
⟶ a:G(I)
⟶ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:𝕀(f(a)) ⟶ 1(f(a))| 
    ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:𝕀(f(a)).  ((w J f u f(a) g) = (w K f ⋅ g (u f(a) g)) ∈ 1(g(f(a))))} 
5. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:G(I).
     ((λK,g. (b I a K f ⋅ g))
     = (b J f(a))
     ∈ {w:J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ J ⟶ u:𝕀(f@0(f(a))) ⟶ 1(f@0(f(a)))| 
        ∀J@0,K:fset(ℕ). ∀f@0:J@0 ⟶ J. ∀g:K ⟶ J@0. ∀u:𝕀(f@0(f(a))).
          ((w J@0 f@0 u f@0(f(a)) g) = (w K f@0 ⋅ g (u f@0(f(a)) g)) ∈ 1(g(f@0(f(a)))))} )
6. I : fset(ℕ)
7. a1 : G(I)
⊢ (a I a1)
= (b I a1)
∈ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:𝕀(f(a1)) ⟶ 1(f(a1))| 
   ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:𝕀(f(a1)).  ((w J f u f(a1) g) = (w K f ⋅ g (u f(a1) g)) ∈ 1(g(f(a1))))} 

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  a  :  I:fset(\mBbbN{})  {}\mrightarrow{}  a:G(I)  {}\mrightarrow{}  Path(1)(a)
3.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a@0:G(I).    ((a  I  a@0  a@0  f)  =  (a  J  f(a@0)))
4.  b  :  I:fset(\mBbbN{})  {}\mrightarrow{}  a:G(I)  {}\mrightarrow{}  Path(1)(a)
5.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:G(I).    ((b  I  a  a  f)  =  (b  J  f(a)))
6.  I  :  fset(\mBbbN{})
7.  a1  :  G(I)
\mvdash{}  (a  I  a1)  =  (b  I  a1)


By

---

Latex:
All  (RepUR  ``pathtype  cubical-fun  cubical-fun-family``)

---

Home Index