Step * 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. {Gamma ⊢ _}
7. cA Gamma ⊢ Compositon(A)
8. {Gamma, psi ⊢ _}
9. cB Gamma, psi ⊢ Compositon(B)
⊢ case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon(A)
BY
DoSubsume }

1
1. Gamma CubicalSet{j}
2. phi {Gamma ⊢ _:𝔽}
3. psi {Gamma ⊢ _:𝔽}
4. Gamma ⊢ (psi  0(𝔽))
5. Gamma ⊢ (1(𝔽 phi)
6. {Gamma ⊢ _}
7. cA Gamma ⊢ Compositon(A)
8. {Gamma, psi ⊢ _}
9. cB Gamma, psi ⊢ Compositon(B)
⊢ case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then else B))

2
1. Gamma CubicalSet{j}
2. phi {Gamma ⊢ _:𝔽}
3. psi {Gamma ⊢ _:𝔽}
4. Gamma ⊢ (psi  0(𝔽))
5. Gamma ⊢ (1(𝔽 phi)
6. {Gamma ⊢ _}
7. cA Gamma ⊢ Compositon(A)
8. {Gamma, psi ⊢ _}
9. cB Gamma, psi ⊢ Compositon(B)
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then else B))
⊢ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then else B)) ⊆Gamma ⊢ Compositon(A)


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)
\mvdash{}  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)  \mmember{}  Gamma  \mvdash{}  Compositon(A)


By


Latex:
DoSubsume




Home Index