---

Step * 1 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)
= case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
⊢ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B)) ⊆r Gamma ⊢ Compositon(B)
BY
{ (RWO  "4" 0 THENA Auto) }

1
.....antecedent..... 
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)
= case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
⊢ Gamma, (phi ∧ psi) ⊢ A = B

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)
= case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
⊢ Gamma, (0(𝔽) ∨ psi) ⊢ Compositon((if 0(𝔽) then A else B)) ⊆r Gamma ⊢ Compositon(B)

---

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)  =  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)
\mvdash{}  Gamma,  (phi  \mvee{}  psi)  \mvdash{}  Compositon((if  phi  then  A  else  B))  \msubseteq{}r  Gamma  \mvdash{}  Compositon(B)


By

---

Latex:
(RWO    "4"  0  THENA  Auto)

---

Home Index