---

Step * 2 of Lemma csm-comp_term


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]})
12. (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]}
⊢ (cA Gamma 1(Gamma.𝕀) phi u a0)s
= ((cA)s+ Delta 1(Delta.𝕀) (phi)s (u)s+ (a0)s)
∈ {Delta ⊢ _:((A)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]}
BY
{ (((Assert Gamma, phi.𝕀 j⊢ BY Auto) THEN (Assert Delta, (phi)s.𝕀 j⊢ BY Auto))
   THEN (Assert (u)s+ ∈ {Delta, (phi)s.𝕀 ⊢ _:(A)s+} BY
               Auto)
   THEN (Assert (u)s+ ∈ {Delta, (phi)s.𝕀 ⊢ _:(A)1(Gamma.𝕀) o s+} BY
               (InferEqualType THEN Auto))
   THEN NthHypEqGen (-5)
   THEN Assert ⌜{Delta ⊢ _:((A)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]}
                = {Delta ⊢ _:(((A)1(Gamma.𝕀))[1(𝕀)])s[(phi)s |⟶ ((u)[1(𝕀)])s]}
                ∈ 𝕌{[i | j']}⌝⋅) }

1
.....assertion..... 
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]})
12. (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]}
13. Gamma, phi.𝕀 j⊢
14. Delta, (phi)s.𝕀 j⊢
15. (u)s+ ∈ {Delta, (phi)s.𝕀 ⊢ _:(A)s+}
16. (u)s+ ∈ {Delta, (phi)s.𝕀 ⊢ _:(A)1(Gamma.𝕀) o s+}
⊢ {Delta ⊢ _:((A)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]}
= {Delta ⊢ _:(((A)1(Gamma.𝕀))[1(𝕀)])s[(phi)s |⟶ ((u)[1(𝕀)])s]}
∈ 𝕌{[i | j']}

2
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]})
12. (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]}
13. Gamma, phi.𝕀 j⊢
14. Delta, (phi)s.𝕀 j⊢
15. (u)s+ ∈ {Delta, (phi)s.𝕀 ⊢ _:(A)s+}
16. (u)s+ ∈ {Delta, (phi)s.𝕀 ⊢ _:(A)1(Gamma.𝕀) o s+}
17. {Delta ⊢ _:((A)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]}
= {Delta ⊢ _:(((A)1(Gamma.𝕀))[1(𝕀)])s[(phi)s |⟶ ((u)[1(𝕀)])s]}
∈ 𝕌{[i | j']}
⊢ ((cA Gamma 1(Gamma.𝕀) phi u a0)s
= ((cA)s+ Delta 1(Delta.𝕀) (phi)s (u)s+ (a0)s)
∈ {Delta ⊢ _:((A)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]})
= ((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]})
∈ ℙ{[j' | i]}

---

Latex:

---

Latex:

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))
12.  (cA  Gamma  1(Gamma.\mBbbI{})  phi  u  a0)s  =  (cA  Delta  1(Gamma.\mBbbI{})  o  s+  (phi)s  (u)s+  (a0)s)
\mvdash{}  (cA  Gamma  1(Gamma.\mBbbI{})  phi  u  a0)s  =  ((cA)s+  Delta  1(Delta.\mBbbI{})  (phi)s  (u)s+  (a0)s)


By

---

Latex:
(((Assert  Gamma,  phi.\mBbbI{}  j\mvdash{}  BY  Auto)  THEN  (Assert  Delta,  (phi)s.\mBbbI{}  j\mvdash{}  BY  Auto))
  THEN  (Assert  (u)s+  \mmember{}  \{Delta,  (phi)s.\mBbbI{}  \mvdash{}  \_:(A)s+\}  BY
                          Auto)
  THEN  (Assert  (u)s+  \mmember{}  \{Delta,  (phi)s.\mBbbI{}  \mvdash{}  \_:(A)1(Gamma.\mBbbI{})  o  s+\}  BY
                          (InferEqualType  THEN  Auto))
  THEN  NthHypEqGen  (-5)
  THEN  Assert  \mkleeneopen{}\{Delta  \mvdash{}  \_:((A)s+)[1(\mBbbI{})][(phi)s  |{}\mrightarrow{}  ((u)s+)[1(\mBbbI{})]]\}
                            =  \{Delta  \mvdash{}  \_:(((A)1(Gamma.\mBbbI{}))[1(\mBbbI{})])s[(phi)s  |{}\mrightarrow{}  ((u)[1(\mBbbI{})])s]\}\mkleeneclose{}\mcdot{})

---

Home Index