---

Step * 1 1 of Lemma composition-type-lemma3

.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. I : fset(ℕ)
7. J : fset(ℕ)
8. f : J ⟶ I
9. a : Gamma(I)
10. ∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j}
13. <(s(f(a));<new-name(J)>)> ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
14. <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
15. <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀
⊢ <(s(f(a));<new-name(J)>)> o iota
= <(s(a);<new-name(I)>)> o iota o subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(a)))
∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
BY
{ (InstLemma `csm-equal` []
   THEN BHyp -1
   THEN (((RepeatFor 2 ((FunExt THENA Auto))
           THEN (RWO "cubical-subset-I_cube" (-1) THENA Auto)
           THEN RenameVar `g' (-1)
           THEN D -1)
          THEN RepUR ``csm-comp compose context-map functor-arrow cube-context-adjoin`` 0
          THEN RepUR ``subset-iota subset-trans cc-adjoin-cube`` 0)
   ORELSE Auto
   )) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. I : fset(ℕ)
7. J : fset(ℕ)
8. f : J ⟶ I
9. a : Gamma(I)
10. ∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j}
13. <(s(f(a));<new-name(J)>)> ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
14. <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
15. <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀
16. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
      f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
17. I@0 : fset(ℕ)
18. g : I@0 ⟶ J+new-name(J)
19. (s(phi(f(a))) g) = 1
⊢ <f,new-name(I)=new-name(J) ⋅ g(s(a)), (<new-name(I)> s(a) f,new-name(I)=new-name(J) ⋅ g)> ∈ alpha:Gamma, phi(I@0)
  × 𝕀(alpha)

2
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. I : fset(ℕ)
7. J : fset(ℕ)
8. f : J ⟶ I
9. a : Gamma(I)
10. ∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j}
13. <(s(f(a));<new-name(J)>)> ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
14. <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
15. <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀
16. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
      f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
17. I1 : fset(ℕ)
18. g : I1 ⟶ J+new-name(J)
19. (s(phi(f(a))) g) = 1
⊢ <g(s(f(a))), (<new-name(J)> s(f(a)) g)>
= <f,new-name(I)=new-name(J) ⋅ g(s(a)), (<new-name(I)> s(a) f,new-name(I)=new-name(J) ⋅ g)>
∈ (alpha:Gamma, phi(I1) × 𝕀(alpha))

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
4.  \{Gamma.\mBbbI{}  \mvdash{}  \_\}  \msubseteq{}r  \{Gamma,  phi.\mBbbI{}  \mvdash{}  \_\}
5.  u  :  \{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}
6.  I  :  fset(\mBbbN{})
7.  J  :  fset(\mBbbN{})
8.  f  :  J  {}\mrightarrow{}  I
9.  a  :  Gamma(I)
10.  \mforall{}I:fset(\mBbbN{}).  \mforall{}[rho:Gamma(I)].  ((s(rho);<new-name(I)>)  \mmember{}  Gamma.\mBbbI{}(I+new-name(I)))
11.  (s(phi(a)))<f,new-name(I)=new-name(J)>  =  s(phi(f(a)))
12.  J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)>  =  J+new-name(J),s(phi(f(a)))
13.  <(s(f(a));<new-name(J)>)>  \mmember{}  J+new-name(J),s(phi(f(a)))  j{}\mrightarrow{}  Gamma,  phi.\mBbbI{}
14.  <(s(f(a));<new-name(J)>)>  o  iota  \mmember{}  J+new-name(J),s(phi(f(a)))  j{}\mrightarrow{}  Gamma,  phi.\mBbbI{}
15.  <(s(a);<new-name(I)>)>  o  iota  \mmember{}  I+new-name(I),s(phi(a))  j{}\mrightarrow{}  Gamma,  phi.\mBbbI{}
\mvdash{}  <(s(f(a));<new-name(J)>)>  o  iota
=  <(s(a);<new-name(I)>)>  o  iota  o  subset-trans(I+new-name(I);J+new-name(J);
                                                                                              f,new-name(I)=new-name(J);s(phi(a)))


By

---

Latex:
(InstLemma  `csm-equal`  []
  THEN  BHyp  -1
  THEN  (((RepeatFor  2  ((FunExt  THENA  Auto))
                  THEN  (RWO  "cubical-subset-I\_cube"  (-1)  THENA  Auto)
                  THEN  RenameVar  `g'  (-1)
                  THEN  D  -1)
                THEN  RepUR  ``csm-comp  compose  context-map  functor-arrow  cube-context-adjoin``  0
                THEN  RepUR  ``subset-iota  subset-trans  cc-adjoin-cube``  0)
  ORELSE  Auto
  ))

---

Home Index