---

Step * 1 of Lemma composition-term-uniformity


1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : H.𝕀 ⊢ CompOp(A)
9. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
⊢ (comp cA [phi ⊢→ u] a0)tau = comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau ∈ {K ⊢ _:((A)[1(𝕀)])tau}
BY
{ BLemma `cubical-term-equal2` }

1
.....wf..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : H.𝕀 ⊢ CompOp(A)
9. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
⊢ K j⊢

2
.....wf..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : H.𝕀 ⊢ CompOp(A)
9. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
⊢ K ⊢ ((A)[1(𝕀)])tau

3
.....wf..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : H.𝕀 ⊢ CompOp(A)
9. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
⊢ (comp cA [phi ⊢→ u] a0)tau ∈ {K ⊢ _:((A)[1(𝕀)])tau}

4
.....wf..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : H.𝕀 ⊢ CompOp(A)
9. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
⊢ comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau ∈ {K ⊢ _:((A)[1(𝕀)])tau}

5
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : H.𝕀 ⊢ CompOp(A)
9. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
⊢ ∀I:fset(ℕ). ∀a:K(I).
    (((comp cA [phi ⊢→ u] a0)tau I a) = (comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau I a) ∈ ((A)[1(𝕀)])tau(a))

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  H
4.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
5.  A  :  \{H.\mBbbI{}  \mvdash{}  \_\}
6.  u  :  \{H,  phi.\mBbbI{}  \mvdash{}  \_:A\}
7.  a0  :  \{H  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
8.  cA  :  H.\mBbbI{}  \mvdash{}  CompOp(A)
9.  ((phi)p)tau+  \mmember{}  \{K.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  (comp  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0)tau  =  comp  (cA)tau+  [(phi)tau  \mvdash{}\mrightarrow{}  (u)tau+]  (a0)tau


By

---

Latex:
BLemma  `cubical-term-equal2`

---

Home Index