---

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


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
5. Gamma ⊢ (1(𝔽) ⇒ psi)
6. B : {Gamma ⊢ _}
7. cB : Gamma ⊢ Compositon(B)
8. A : {Gamma, phi ⊢ _}
9. cA : Gamma, phi ⊢ Compositon(A)
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(B)
11. H : CubicalSet{j}
12. sigma : H.𝕀 j⟶ Gamma
13. p1 : {H ⊢ _:𝔽}
14. u : {H, p1.𝕀 ⊢ _:(B)sigma}
15. a0 : {H ⊢ _:((B)sigma)[0(𝕀)][p1 |⟶ (u)[0(𝕀)]]}
16. I : fset(ℕ)
17. a : H(I)
18. (∀ (phi)sigma)(a) = 0 ∈ Point(face_lattice(I))
⊢ (cB H sigma p1 u a0 I a)
= if ((∀ (phi)sigma)(a)==1) then cA H, (∀ (phi)sigma) sigma p1 u a0(a) else cB H, (∀ (psi)sigma) sigma p1 u a0(a) fi 
∈ ((B)sigma)[1(𝕀)](a)
BY
{ ((Subst' ((∀ (phi)sigma)(a)==1) ~ ff 0 THENA (BoolCase ⌜((∀ (phi)sigma)(a)==1)⌝⋅ THEN Auto)) THENM Reduce 0) }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  ((\mforall{}  (phi)sigma)(a)==1)  \msim{}  ff  0  THENA  (BoolCase  \mkleeneopen{}((\mforall{}  (phi)sigma)(a)==1)\mkleeneclose{}\mcdot{}  THEN  Auto))
THENM  Reduce  0
)

---

Home Index