---

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


1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. I : fset(ℕ)
4. I1 : fset(ℕ)
5. a1 : I1 ⟶ I+new-name(I)
6. v : H(I)
7. (phi(s(v)))<a1> = phi(a1(s(v))) ∈ 𝔽(a1(s(v)))
⊢ phi(a1(s(v))) ∈ 𝔽(a1)
BY
{ InferEqualTypeGen }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. I : fset(ℕ)
4. I1 : fset(ℕ)
5. a1 : I1 ⟶ I+new-name(I)
6. v : H(I)
7. (phi(s(v)))<a1> = phi(a1(s(v))) ∈ 𝔽(a1(s(v)))
⊢ 𝔽(a1(s(v))) = 𝔽(a1) ∈ Type

2
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. I : fset(ℕ)
4. I1 : fset(ℕ)
5. a1 : I1 ⟶ I+new-name(I)
6. v : H(I)
7. (phi(s(v)))<a1> = phi(a1(s(v))) ∈ 𝔽(a1(s(v)))
8. 𝔽(a1(s(v))) = 𝔽(a1) ∈ Type
⊢ phi(a1(s(v))) ∈ 𝔽(a1(s(v)))

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
3.  I  :  fset(\mBbbN{})
4.  I1  :  fset(\mBbbN{})
5.  a1  :  I1  {}\mrightarrow{}  I+new-name(I)
6.  v  :  H(I)
7.  (phi(s(v)))<a1>  =  phi(a1(s(v)))
\mvdash{}  phi(a1(s(v)))  \mmember{}  \mBbbF{}(a1)


By

---

Latex:
InferEqualTypeGen

---

Home Index