---

Step * 1 1 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)
⊢ case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
BY
{ ((Assert Gamma, psi ⊢ B BY
          (SubsumeC  ⌜{Gamma ⊢ _}⌝⋅ THEN Auto))
   THEN (Assert cB ∈ Gamma, psi ⊢ Compositon(B) BY
               (SubsumeC ⌜Gamma ⊢ Compositon(B)⌝⋅ THEN Auto))
   THEN (Assert Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽)) BY
               (RWO  "4" 0 THEN Auto))
   THEN (Assert Gamma, (phi ∧ psi) ⊢ A = B BY
               (UnfoldTopAb 0
                THEN SubsumeC ⌜{Gamma, 0(𝔽) ⊢ _}⌝⋅
                THEN Try ((BLemma `empty-context-subset-lemma6` THEN Auto))
                THEN (BLemma `subset-cubical-type` THENA Auto)
                THEN BLemma `face-term-implies-subset`
                THEN Auto))) }

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. Gamma, psi ⊢ B
11. cB ∈ Gamma, psi ⊢ Compositon(B)
12. Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽))
13. Gamma, (phi ∧ psi) ⊢ A = B
⊢ case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else 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)
\mvdash{}  case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)
    \mmember{}  Gamma,  (phi  \mvee{}  psi)  \mvdash{}  Compositon((if  phi  then  A  else  B))


By

---

Latex:
((Assert  Gamma,  psi  \mvdash{}  B  BY
                (SubsumeC    \mkleeneopen{}\{Gamma  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  cB  \mmember{}  Gamma,  psi  \mvdash{}  Compositon(B)  BY
                          (SubsumeC  \mkleeneopen{}Gamma  \mvdash{}  Compositon(B)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))  BY
                          (RWO    "4"  0  THEN  Auto))
  THEN  (Assert  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  A  =  B  BY
                          (UnfoldTopAb  0
                            THEN  SubsumeC  \mkleeneopen{}\{Gamma,  0(\mBbbF{})  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
                            THEN  Try  ((BLemma  `empty-context-subset-lemma6`  THEN  Auto))
                            THEN  (BLemma  `subset-cubical-type`  THENA  Auto)
                            THEN  BLemma  `face-term-implies-subset`
                            THEN  Auto)))

---

Home Index