---

Step * of Lemma comp_term-subset

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)]. ∀[u:{Gamma, phi.𝕀 ⊢ _:A}].
∀[a0:{Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}]. ∀[psi:{Gamma ⊢ _:𝔽}].
  (comp cA [phi ⊢→ u] a0 = comp cA [phi ⊢→ u] a0 ∈ {Gamma, psi ⊢ _:(A)[1(𝕀)]})
BY
{ (InstLemma `csm-comp_term` []
   THEN RepeatFor 6 (ParallelLast')
   THEN Intro
   THEN (InstHyp [⌜Gamma, psi⌝;⌜1(Gamma)⌝] (-2)⋅ THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
7. ∀[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(𝕀)]]})
8. psi : {Gamma ⊢ _:𝔽}
9. (comp cA [phi ⊢→ u] a0)1(Gamma)
= comp (cA)1(Gamma)+ [(phi)1(Gamma) ⊢→ (u)1(Gamma)+] (a0)1(Gamma)
∈ {Gamma, psi ⊢ _:((A)1(Gamma)+)[1(𝕀)][(phi)1(Gamma) |⟶ ((u)1(Gamma)+)[1(𝕀)]]}
⊢ comp cA [phi ⊢→ u] a0 = comp cA [phi ⊢→ u] a0 ∈ {Gamma, psi ⊢ _:(A)[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{}[psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    (comp  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0  =  comp  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0)


By

---

Latex:
(InstLemma  `csm-comp\_term`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Intro
  THEN  (InstHyp  [\mkleeneopen{}Gamma,  psi\mkleeneclose{};\mkleeneopen{}1(Gamma)\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto))

---

Home Index