---

Step * 1 5 1 1 1 1 2 2 1 1 1 2 1 2 1 2 1 1 1 1 1 1 1 1 of Lemma composition-term-uniformity

.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. u : {Gamma, phi.𝕀 ⊢ _:A}
5. a0 : {Gamma ⊢ _:(A)[0(𝕀)]}
6. (u)[0(𝕀)] = a0 ∈ {Gamma, phi ⊢ _:(A)[0(𝕀)]}
7. I : fset(ℕ)
8. J : fset(ℕ)
9. rho : Gamma(I)
10. f : J ⟶ I
11. (phi(rho) f) = 1
12. A(f((new-name(I)0)((s(rho);<new-name(I)>)))) = A(f((rho;0))) ∈ Type
13. A(f((rho;0))) = A((f(rho);0)) ∈ Type
14. (a0(rho) (new-name(I)0)((s(rho);<new-name(I)>)) f) = (a0(rho) (rho;0) f) ∈ A((f(rho);0))
15. (a0(rho) (rho;0) f) = a0(f(rho)) ∈ A((f(rho);0))
⊢ (u)[0(𝕀)] = a0 ∈ {Gamma, phi ⊢ _:((A)[0(𝕀)])iota}
BY
{ (NthHypSq 6 THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
4.  u  :  \{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}
5.  a0  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}
6.  (u)[0(\mBbbI{})]  =  a0
7.  I  :  fset(\mBbbN{})
8.  J  :  fset(\mBbbN{})
9.  rho  :  Gamma(I)
10.  f  :  J  {}\mrightarrow{}  I
11.  (phi(rho)  f)  =  1
12.  A(f((new-name(I)0)((s(rho);<new-name(I)>))))  =  A(f((rho;0)))
13.  A(f((rho;0)))  =  A((f(rho);0))
14.  (a0(rho)  (new-name(I)0)((s(rho);<new-name(I)>))  f)  =  (a0(rho)  (rho;0)  f)
15.  (a0(rho)  (rho;0)  f)  =  a0(f(rho))
\mvdash{}  (u)[0(\mBbbI{})]  =  a0


By

---

Latex:
(NthHypSq  6  THEN  CsmUnfolding  THEN  Auto)

---

Home Index