---

Step * 1 of Lemma csm-comp_term

.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. Gamma.𝕀 j⊢
5. cA : composition-function{j:l,i:l}(Gamma.𝕀;A)
6. u : {Gamma, phi.𝕀 ⊢ _:A}
7. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. Delta : CubicalSet{j}
9. s : Delta j⟶ Gamma
10. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
11. ∀a0:{Gamma ⊢ _:((A)1(Gamma.𝕀))[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
      ((cA Gamma 1(Gamma.𝕀) phi u a0)s
      = (cA Delta 1(Gamma.𝕀) o s+ (phi)s (u)s+ (a0)s)
      ∈ {Delta ⊢ _:(((A)1(Gamma.𝕀))[1(𝕀)])s[(phi)s |⟶ ((u)[1(𝕀)])s]})
⊢ a0 ∈ {Gamma ⊢ _:((A)1(Gamma.𝕀))[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
BY
{ (InferEqualType THEN Try (Trivial) THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. Gamma.𝕀 j⊢
5. cA : composition-function{j:l,i:l}(Gamma.𝕀;A)
6. u : {Gamma, phi.𝕀 ⊢ _:A}
7. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. Delta : CubicalSet{j}
9. s : Delta j⟶ Gamma
10. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
11. ∀a0:{Gamma ⊢ _:((A)1(Gamma.𝕀))[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
      ((cA Gamma 1(Gamma.𝕀) phi u a0)s
      = (cA Delta 1(Gamma.𝕀) o s+ (phi)s (u)s+ (a0)s)
      ∈ {Delta ⊢ _:(((A)1(Gamma.𝕀))[1(𝕀)])s[(phi)s |⟶ ((u)[1(𝕀)])s]})
⊢ (A)[0(𝕀)] = ((A)1(Gamma.𝕀))[0(𝕀)] ∈ cubical-type{[j' | i']:l}(Gamma)

2
.....subterm..... T:t
4:n
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. Gamma.𝕀 j⊢
5. cA : composition-function{j:l,i:l}(Gamma.𝕀;A)
6. u : {Gamma, phi.𝕀 ⊢ _:A}
7. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. Delta : CubicalSet{j}
9. s : Delta j⟶ Gamma
10. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
11. ∀a0:{Gamma ⊢ _:((A)1(Gamma.𝕀))[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
      ((cA Gamma 1(Gamma.𝕀) phi u a0)s
      = (cA Delta 1(Gamma.𝕀) o s+ (phi)s (u)s+ (a0)s)
      ∈ {Delta ⊢ _:(((A)1(Gamma.𝕀))[1(𝕀)])s[(phi)s |⟶ ((u)[1(𝕀)])s]})
⊢ (u)[0(𝕀)] = (u)[0(𝕀)] ∈ {Gamma, phi ⊢ _:(A)[0(𝕀)]}

---

Latex:

---

Latex:
.....wf..... 
1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
4.  Gamma.\mBbbI{}  j\mvdash{}
5.  cA  :  composition-function\{j:l,i:l\}(Gamma.\mBbbI{};A)
6.  u  :  \{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}
7.  a0  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
8.  Delta  :  CubicalSet\{j\}
9.  s  :  Delta  j{}\mrightarrow{}  Gamma
10.  \{Gamma.\mBbbI{}  \mvdash{}  \_\}  \msubseteq{}r  \{Gamma,  phi.\mBbbI{}  \mvdash{}  \_\}
11.  \mforall{}a0:\{Gamma  \mvdash{}  \_:((A)1(Gamma.\mBbbI{}))[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
            ((cA  Gamma  1(Gamma.\mBbbI{})  phi  u  a0)s  =  (cA  Delta  1(Gamma.\mBbbI{})  o  s+  (phi)s  (u)s+  (a0)s))
\mvdash{}  a0  \mmember{}  \{Gamma  \mvdash{}  \_:((A)1(Gamma.\mBbbI{}))[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}


By

---

Latex:
(InferEqualType  THEN  Try  (Trivial)  THEN  EqCDA)

---

Home Index