---

Step * of Lemma composition-in-subset

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G ⊢ Compositon(A)]. ∀[H1,H2:j⊢].
  ∀[sigma:H1.𝕀 j⟶ G]. ∀[phi:{H1 ⊢ _:𝔽}]. ∀[u:{H1, phi.𝕀 ⊢ _:(A)sigma}].
  ∀[a0:{H1 ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    ((cA H1 sigma phi u a0) = (cA H2 sigma phi u a0) ∈ {H2 ⊢ _:((A)sigma)[1(𝕀)]}) 
  supposing sub_cubical_set{j:l}(H2; H1)
BY
{ (Intros
   THEN OnVar `cA' (\h. ((D h THEN (D h+1 With ⌜H1⌝  THENA Auto))
                         THEN (InstHyp [⌜H2⌝;⌜1(H2)⌝;⌜sigma⌝;⌜phi⌝;⌜u⌝;⌜a0⌝] (-1)⋅ THENA Auto)
                         ))⋅
   THEN (EqTypeHD (-1) THENA Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : composition-function{j:l,i:l}(G;A)
4. H1 : CubicalSet{j}
5. H2 : CubicalSet{j}
6. sub_cubical_set{j:l}(H2; H1)
7. sigma : H1.𝕀 j⟶ G
8. phi : {H1 ⊢ _:𝔽}
9. u : {H1, phi.𝕀 ⊢ _:(A)sigma}
10. a0 : {H1 ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
11. ∀K:j⊢. ∀tau:K j⟶ H1. ∀sigma:H1.𝕀 j⟶ G. ∀phi:{H1 ⊢ _:𝔽}. ∀u:{H1, phi.𝕀 ⊢ _:(A)sigma}.
    ∀a0:{H1 ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
      ((cA H1 sigma phi u a0)tau
      = (cA K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
      ∈ {K ⊢ _:(((A)sigma)[1(𝕀)])tau[(phi)tau |⟶ ((u)[1(𝕀)])tau]})
12. (cA H1 sigma phi u a0)1(H2)
= (cA H2 sigma o 1(H2)+ (phi)1(H2) (u)1(H2)+ (a0)1(H2))
∈ {H2 ⊢ _:(((A)sigma)[1(𝕀)])1(H2)}
13. ((u)[1(𝕀)])1(H2) = (cA H1 sigma phi u a0)1(H2) ∈ {H2, (phi)1(H2) ⊢ _:(((A)sigma)[1(𝕀)])1(H2)}
⊢ (cA H1 sigma phi u a0) = (cA H2 sigma phi u a0) ∈ {H2 ⊢ _:((A)sigma)[1(𝕀)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  \mvdash{}  Compositon(A)].  \mforall{}[H1,H2:j\mvdash{}].
    \mforall{}[sigma:H1.\mBbbI{}  j{}\mrightarrow{}  G].  \mforall{}[phi:\{H1  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[u:\{H1,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}].
    \mforall{}[a0:\{H1  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}].
        ((cA  H1  sigma  phi  u  a0)  =  (cA  H2  sigma  phi  u  a0)) 
    supposing  sub\_cubical\_set\{j:l\}(H2;  H1)


By

---

Latex:
(Intros
  THEN  OnVar  `cA'  (\mbackslash{}h.  ((D  h  THEN  (D  h+1  With  \mkleeneopen{}H1\mkleeneclose{}    THENA  Auto))
                                              THEN  (InstHyp  [\mkleeneopen{}H2\mkleeneclose{};\mkleeneopen{}1(H2)\mkleeneclose{};\mkleeneopen{}sigma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}a0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                                              ))\mcdot{}
  THEN  (EqTypeHD  (-1)  THENA  Auto))

---

Home Index