---

Step * 1 of Lemma composition-in-subset


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(𝕀)]}
BY
{ (Thin (-1)
   THEN (Subst' (((A)sigma)[1(𝕀)])1(H2) ~ ((A)sigma)[1(𝕀)] -1 THENA (CsmUnfolding THEN Auto))
   THEN NthHypEqGen (-1)
   THEN EqCDA) }

1
.....subterm..... T:t
2:n
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(𝕀)]}
⊢ (cA H1 sigma phi u a0) = (cA H1 sigma phi u a0)1(H2) ∈ {H2 ⊢ _:((A)sigma)[1(𝕀)]}

2
.....subterm..... T:t
3:n
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(𝕀)]}
⊢ (cA H2 sigma phi u a0) = (cA H2 sigma o 1(H2)+ (phi)1(H2) (u)1(H2)+ (a0)1(H2)) ∈ {H2 ⊢ _:((A)sigma)[1(𝕀)]}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
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.\mBbbI{}  j{}\mrightarrow{}  G
8.  phi  :  \{H1  \mvdash{}  \_:\mBbbF{}\}
9.  u  :  \{H1,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
10.  a0  :  \{H1  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
11.  \mforall{}K:j\mvdash{}.  \mforall{}tau:K  j{}\mrightarrow{}  H1.  \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)tau  =  (cA  K  sigma  o  tau+  (phi)tau  (u)tau+  (a0)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))
13.  ((u)[1(\mBbbI{})])1(H2)  =  (cA  H1  sigma  phi  u  a0)1(H2)
\mvdash{}  (cA  H1  sigma  phi  u  a0)  =  (cA  H2  sigma  phi  u  a0)


By

---

Latex:
(Thin  (-1)
  THEN  (Subst'  (((A)sigma)[1(\mBbbI{})])1(H2)  \msim{}  ((A)sigma)[1(\mBbbI{})]  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  NthHypEqGen  (-1)
  THEN  EqCDA)

---

Home Index