Step * 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. {Gamma ⊢ _}
7. cB Gamma ⊢ Compositon(B)
8. {Gamma, phi ⊢ _}
9. cA Gamma, phi ⊢ Compositon(A)
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(B)
⊢ case-type-comp(Gamma; phi; psi; A; B; cA; cB) cB ∈ Gamma ⊢ Compositon(B)
BY
(((BLemma `composition-structure-equal` THENM Intros) THENA Auto)
   THEN Symmetry
   THEN (CubicalTermEqual THENA Auto)
   THEN RepUR ``case-type-comp case-term`` 0
   THEN Assert ⌜(∀ (phi)sigma)(a) 0 ∈ Point(face_lattice(I))⌝⋅}

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

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


By


Latex:
(((BLemma  `composition-structure-equal`  THENM  Intros)  THENA  Auto)
  THEN  Symmetry
  THEN  (CubicalTermEqual  THENA  Auto)
  THEN  RepUR  ``case-type-comp  case-term``  0
  THEN  Assert  \mkleeneopen{}(\mforall{}  (phi)sigma)(a)  =  0\mkleeneclose{}\mcdot{})




Home Index