---

Step * 1 1 of Lemma case-type-comp-true-false


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. Gamma ⊢ (psi ⇒ 0(𝔽))
5. Gamma ⊢ (1(𝔽) ⇒ phi)
6. A : {Gamma ⊢ _}
7. cA : Gamma ⊢ Compositon(A)
8. B : {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 A else B))
BY
{ ((Assert Gamma, phi ⊢ A BY
          (SubsumeC  ⌜{Gamma ⊢ _}⌝⋅ THEN Auto))
   THEN (Assert cA ∈ Gamma, phi ⊢ Compositon(A) BY
               (SubsumeC ⌜Gamma ⊢ Compositon(A)⌝⋅ THEN Auto))
   THEN (Assert Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽)) BY
               (RepeatFor 2 (ParallelOp 4) THEN RepeatFor 2 (ParallelLast) THEN RWO  "face-and-eq-1" (-1) 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. Gamma ⊢ (psi ⇒ 0(𝔽))
5. Gamma ⊢ (1(𝔽) ⇒ phi)
6. A : {Gamma ⊢ _}
7. cA : Gamma ⊢ Compositon(A)
8. B : {Gamma, psi ⊢ _}
9. cB : Gamma, psi ⊢ Compositon(B)
10. Gamma, phi ⊢ A
11. cA ∈ Gamma, phi ⊢ Compositon(A)
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.  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,  (phi  \mvee{}  psi)  \mvdash{}  Compositon((if  phi  then  A  else  B))


By

---

Latex:
((Assert  Gamma,  phi  \mvdash{}  A  BY
                (SubsumeC    \mkleeneopen{}\{Gamma  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  cA  \mmember{}  Gamma,  phi  \mvdash{}  Compositon(A)  BY
                          (SubsumeC  \mkleeneopen{}Gamma  \mvdash{}  Compositon(A)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))  BY
                          (RepeatFor  2  (ParallelOp  4)
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  RWO    "face-and-eq-1"  (-1)
                            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