---

Step * of Lemma csm-comp_term

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)]. ∀[u:{Gamma, phi.𝕀 ⊢ _:A}].
∀[a0:{Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ Gamma].
  ((comp cA [phi ⊢→ u] a0)s = comp (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta ⊢ _:((A)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]})
BY
{ ((RepeatFor 3 (Intro) THEN (Assert Gamma.𝕀 j⊢ BY Auto) THEN Intros)
   THEN ((InstLemma `context-subset-adjoin-subtype` [⌜Gamma⌝;⌜𝕀⌝;⌜phi⌝]⋅ THENA Auto)
         THEN OnVar `cA' (\h. (D h
                               THEN (D h+1 With ⌜Gamma⌝  THENA Auto)
                               THEN (Assert u ∈ {Gamma, phi.𝕀 ⊢ _:(A)1(Gamma.𝕀)} BY
                                           (InferEqualType
                                            THEN Try (Trivial)
                                            THEN EqCDA
                                            THEN SubsumeC ⌜{Gamma.𝕀 ⊢ _}⌝⋅
                                            THEN Auto))
                               THEN (InstHyp [⌜Delta⌝;⌜s⌝;⌜1(Gamma.𝕀)⌝;⌜phi⌝;⌜u⌝] (-2)⋅ THENA Auto)
                               THEN RepeatFor 2 (Thin (-2))) )⋅
         )
   THEN Unfold `comp_term` 0
   THEN InstHyp [⌜a0⌝] (-1)⋅) }

1
.....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(𝕀)]]}

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]}
⊢ (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(𝕀)]]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  Compositon(A)].
\mforall{}[u:\{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}].  \mforall{}[a0:\{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}].  \mforall{}[Delta:j\mvdash{}].
\mforall{}[s:Delta  j{}\mrightarrow{}  Gamma].
    ((comp  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0)s  =  comp  (cA)s+  [(phi)s  \mvdash{}\mrightarrow{}  (u)s+]  (a0)s)


By

---

Latex:
((RepeatFor  3  (Intro)  THEN  (Assert  Gamma.\mBbbI{}  j\mvdash{}  BY  Auto)  THEN  Intros)
  THEN  ((InstLemma  `context-subset-adjoin-subtype`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  OnVar  `cA'  (\mbackslash{}h.  (D  h
                                                          THEN  (D  h+1  With  \mkleeneopen{}Gamma\mkleeneclose{}    THENA  Auto)
                                                          THEN  (Assert  u  \mmember{}  \{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:(A)1(Gamma.\mBbbI{})\}  BY
                                                                                  (InferEqualType
                                                                                    THEN  Try  (Trivial)
                                                                                    THEN  EqCDA
                                                                                    THEN  SubsumeC  \mkleeneopen{}\{Gamma.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
                                                                                    THEN  Auto))
                                                          THEN  (InstHyp  [\mkleeneopen{}Delta\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}1(Gamma.\mBbbI{})\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                                                          THEN  RepeatFor  2  (Thin  (-2)))  )\mcdot{}
              )
  THEN  Unfold  `comp\_term`  0
  THEN  InstHyp  [\mkleeneopen{}a0\mkleeneclose{}]  (-1)\mcdot{})

---

Home Index