---

Step * 2 of Lemma case-type-comp-partition


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽))
9. Gamma ⊢ (1(𝔽) ⇒ (phi ∨ psi))
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
11. 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
BY
{ (Unfold `same-cubical-type` 0 THEN SubsumeC ⌜{Gamma, 0(𝔽) ⊢ _}⌝⋅ THEN Try (Fold `same-cubical-type` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  A  :  \{Gamma,  phi  \mvdash{}  \_\}
5.  B  :  \{Gamma,  psi  \mvdash{}  \_\}
6.  cA  :  Gamma,  phi  \mvdash{}  Compositon(A)
7.  cB  :  Gamma,  psi  \mvdash{}  Compositon(B)
8.  Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))
9.  Gamma  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (phi  \mvee{}  psi))
10.  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)
        \mmember{}  Gamma,  (phi  \mvee{}  psi)  \mvdash{}  Compositon((if  phi  then  A  else  B))
11.  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)  =  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)
\mvdash{}  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  A  =  B


By

---

Latex:
(Unfold  `same-cubical-type`  0
  THEN  SubsumeC  \mkleeneopen{}\{Gamma,  0(\mBbbF{})  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
  THEN  Try  (Fold  `same-cubical-type`  0)
  THEN  Auto)

---

Home Index