---

Step * 2 1 of Lemma case-type-comp-true-false

.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. Gamma ⊢ (psi ⇒ 0(𝔽))
5. Gamma ⊢ (1(𝔽) ⇒ phi)
6. A : {Gamma ⊢ _}
7. cA : Gamma ⊢ Compositon(A)
8. B : {Gamma, psi ⊢ _}
9. cB : Gamma, psi ⊢ Compositon(B)
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(A)
11. H : CubicalSet{j}
12. sigma : H.𝕀 j⟶ Gamma
13. p1 : {H ⊢ _:𝔽}
14. u : {H, p1.𝕀 ⊢ _:(A)sigma}
15. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][p1 |⟶ (u)[0(𝕀)]]}
16. I : fset(ℕ)
17. a : H(I)
⊢ (∀ (phi)sigma)(a) = 1 ∈ Point(face_lattice(I))
BY
{ ((InstLemma `csm-face-term-implies` [⌜Gamma⌝;⌜1(𝔽)⌝;⌜phi⌝;⌜H.𝕀⌝;⌜sigma⌝]⋅ THENA Auto)
   THEN (RWO "csm-face-1" (-1) THENA Auto)
   THEN RepUR ``face-forall cubical-term-at`` 0) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. Gamma ⊢ (psi ⇒ 0(𝔽))
5. Gamma ⊢ (1(𝔽) ⇒ phi)
6. A : {Gamma ⊢ _}
7. cA : Gamma ⊢ Compositon(A)
8. B : {Gamma, psi ⊢ _}
9. cB : Gamma, psi ⊢ Compositon(B)
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(A)
11. H : CubicalSet{j}
12. sigma : H.𝕀 j⟶ Gamma
13. p1 : {H ⊢ _:𝔽}
14. u : {H, p1.𝕀 ⊢ _:(A)sigma}
15. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][p1 |⟶ (u)[0(𝕀)]]}
16. I : fset(ℕ)
17. a : H(I)
18. H.𝕀 ⊢ (1(𝔽) ⇒ (phi)sigma)
⊢ (∀new-name(I).(phi)sigma I+new-name(I) (s(a);<new-name(I)>)) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  Gamma  \mvdash{}  (psi  {}\mRightarrow{}  0(\mBbbF{}))
5.  Gamma  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  phi)
6.  A  :  \{Gamma  \mvdash{}  \_\}
7.  cA  :  Gamma  \mvdash{}  Compositon(A)
8.  B  :  \{Gamma,  psi  \mvdash{}  \_\}
9.  cB  :  Gamma,  psi  \mvdash{}  Compositon(B)
10.  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)  \mmember{}  Gamma  \mvdash{}  Compositon(A)
11.  H  :  CubicalSet\{j\}
12.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Gamma
13.  p1  :  \{H  \mvdash{}  \_:\mBbbF{}\}
14.  u  :  \{H,  p1.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
15.  a0  :  \{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][p1  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
16.  I  :  fset(\mBbbN{})
17.  a  :  H(I)
\mvdash{}  (\mforall{}  (phi)sigma)(a)  =  1


By

---

Latex:
((InstLemma  `csm-face-term-implies`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}1(\mBbbF{})\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}sigma\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "csm-face-1"  (-1)  THENA  Auto)
  THEN  RepUR  ``face-forall  cubical-term-at``  0)

---

Home Index