---

Step * 1 of Lemma comp_term-subset


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(𝕀)]}
BY
{ ((Subst' ((u)1(Gamma)+)[1(𝕀)] ~ (u)[1(𝕀)] -1 THENA (CsmUnfolding THEN Auto))
   THEN (Subst' ((A)1(Gamma)+)[1(𝕀)] ~ (A)[1(𝕀)] -1 THENA (CsmUnfolding THEN 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(𝕀)][(phi)1(Gamma) |⟶ (u)[1(𝕀)]]}
⊢ comp cA [phi ⊢→ u] a0 = comp cA [phi ⊢→ u] a0 ∈ {Gamma, psi ⊢ _:(A)[1(𝕀)]}

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  ((u)1(Gamma)+)[1(\mBbbI{})]  \msim{}  (u)[1(\mBbbI{})]  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (Subst'  ((A)1(Gamma)+)[1(\mBbbI{})]  \msim{}  (A)[1(\mBbbI{})]  -1  THENA  (CsmUnfolding  THEN  Auto))
  )

---

Home Index