---

Step * 1 4 1 3 2 1 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.𝕀 ⊢ _:𝔽}
10. ∀[u:{K, (phi)tau.𝕀 ⊢ _:(A)tau+}]. ∀[a0:{K ⊢ _:((A)tau+)[0(𝕀)][(phi)tau |⟶ (u)[0(𝕀)]]}].
      (comp (cA)tau+ [(phi)tau ⊢→ u] a0 ∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ (u)[1(𝕀)]]})
11. comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau ∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ ((u)tau+)[1(𝕀)]]}
12. comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau
= comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau
∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ ((u)tau+)[1(𝕀)]]}
13. x : {K ⊢ _:((A)tau+)[1(𝕀)]}
14. ((u)tau+)[1(𝕀)] = x ∈ {K, (phi)tau ⊢ _:((A)tau+)[1(𝕀)]}
⊢ x ∈ {K ⊢ _:((A)[1(𝕀)])tau}
BY
{ InferEqualTypeGen }

1
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.𝕀 ⊢ _:𝔽}
10. ∀[u:{K, (phi)tau.𝕀 ⊢ _:(A)tau+}]. ∀[a0:{K ⊢ _:((A)tau+)[0(𝕀)][(phi)tau |⟶ (u)[0(𝕀)]]}].
      (comp (cA)tau+ [(phi)tau ⊢→ u] a0 ∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ (u)[1(𝕀)]]})
11. comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau ∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ ((u)tau+)[1(𝕀)]]}
12. comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau
= comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau
∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ ((u)tau+)[1(𝕀)]]}
13. x : {K ⊢ _:((A)tau+)[1(𝕀)]}
14. ((u)tau+)[1(𝕀)] = x ∈ {K, (phi)tau ⊢ _:((A)tau+)[1(𝕀)]}
⊢ {K ⊢ _:((A)tau+)[1(𝕀)]} = {K ⊢ _:((A)[1(𝕀)])tau} ∈ 𝕌{[i | j']}

2
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.𝕀 ⊢ _:𝔽}
10. ∀[u:{K, (phi)tau.𝕀 ⊢ _:(A)tau+}]. ∀[a0:{K ⊢ _:((A)tau+)[0(𝕀)][(phi)tau |⟶ (u)[0(𝕀)]]}].
      (comp (cA)tau+ [(phi)tau ⊢→ u] a0 ∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ (u)[1(𝕀)]]})
11. comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau ∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ ((u)tau+)[1(𝕀)]]}
12. comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau
= comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau
∈ {K ⊢ _:((A)tau+)[1(𝕀)][(phi)tau |⟶ ((u)tau+)[1(𝕀)]]}
13. x : {K ⊢ _:((A)tau+)[1(𝕀)]}
14. ((u)tau+)[1(𝕀)] = x ∈ {K, (phi)tau ⊢ _:((A)tau+)[1(𝕀)]}
15. {K ⊢ _:((A)tau+)[1(𝕀)]} = {K ⊢ _:((A)[1(𝕀)])tau} ∈ 𝕌{[i | j']}
⊢ x ∈ {K ⊢ _:((A)tau+)[1(𝕀)]}

---

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{}\}
10.  \mforall{}[u:\{K,  (phi)tau.\mBbbI{}  \mvdash{}  \_:(A)tau+\}].  \mforall{}[a0:\{K  \mvdash{}  \_:((A)tau+)[0(\mBbbI{})][(phi)tau  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}].
            (comp  (cA)tau+  [(phi)tau  \mvdash{}\mrightarrow{}  u]  a0  \mmember{}  \{K  \mvdash{}  \_:((A)tau+)[1(\mBbbI{})][(phi)tau  |{}\mrightarrow{}  (u)[1(\mBbbI{})]]\})
11.  comp  (cA)tau+  [(phi)tau  \mvdash{}\mrightarrow{}  (u)tau+]  (a0)tau
        \mmember{}  \{K  \mvdash{}  \_:((A)tau+)[1(\mBbbI{})][(phi)tau  |{}\mrightarrow{}  ((u)tau+)[1(\mBbbI{})]]\}
12.  comp  (cA)tau+  [(phi)tau  \mvdash{}\mrightarrow{}  (u)tau+]  (a0)tau  =  comp  (cA)tau+  [(phi)tau  \mvdash{}\mrightarrow{}  (u)tau+]  (a0)tau
13.  x  :  \{K  \mvdash{}  \_:((A)tau+)[1(\mBbbI{})]\}
14.  ((u)tau+)[1(\mBbbI{})]  =  x
\mvdash{}  x  \mmember{}  \{K  \mvdash{}  \_:((A)[1(\mBbbI{})])tau\}


By

---

Latex:
InferEqualTypeGen

---

Home Index