---

Step * 2 of Lemma csm-fill_term


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
10. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
11. (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}
⊢ (fill cA [phi ⊢→ u] a0)s+ = fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}
BY
{ ((InstLemma `fill_term_wf` [⌜Delta⌝;⌜(phi)s⌝;⌜(A)s+⌝;⌜(cA)s+⌝;⌜(u)s+⌝;⌜(a0)s⌝]⋅ THENA Auto)
   THEN Symmetry
   THEN MemTypeCD) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
10. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
11. (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}
12. fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}
⊢ fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s = (fill cA [phi ⊢→ u] a0)s+ ∈ {Delta.𝕀 ⊢ _:(A)s+}

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
10. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
11. (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}
12. fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}
⊢ (u)s+ = fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
10. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
11. (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}
12. fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}
13. a : {Delta.𝕀 ⊢ _:(A)s+}
⊢ istype((u)s+ = a ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+})

---

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.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}
6.  a0  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  u[0]]\}
7.  Delta  :  CubicalSet\{j\}
8.  s  :  Delta  j{}\mrightarrow{}  Gamma
9.  Delta.\mBbbI{}  \mvdash{}  (((phi)s)p  {}\mRightarrow{}  ((phi)p)s+)
10.  (u)s+  \mmember{}  \{Delta.\mBbbI{},  ((phi)s)p  \mvdash{}  \_:(A)s+\}
11.  (a0)s  \mmember{}  \{Delta  \mvdash{}  \_:((A)s+)[0(\mBbbI{})][(phi)s  |{}\mrightarrow{}  (u)s+[0]]\}
\mvdash{}  (fill  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0)s+  =  fill  (cA)s+  [(phi)s  \mvdash{}\mrightarrow{}  (u)s+]  (a0)s


By

---

Latex:
((InstLemma  `fill\_term\_wf`  [\mkleeneopen{}Delta\mkleeneclose{};\mkleeneopen{}(phi)s\mkleeneclose{};\mkleeneopen{}(A)s+\mkleeneclose{};\mkleeneopen{}(cA)s+\mkleeneclose{};\mkleeneopen{}(u)s+\mkleeneclose{};\mkleeneopen{}(a0)s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Symmetry
  THEN  MemTypeCD)

---

Home Index