---

Step * 1 2 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)
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(A)
BY
{ ((Assert (if phi then A else B) = A ∈ {Gamma ⊢ _} BY
          (SubsumeC ⌜{Gamma, phi ⊢ _}⌝⋅
           THENL [(Fold `same-cubical-type` 0 THEN UsingVars [`psi'] (BLemma  `case-type-same1`) THEN Auto)
                 ; ((BLemma `subset-cubical-type` THENA Auto) THEN BLemma `face-1-implies-subset` THEN Auto)]
          ))
   THEN (Assert Gamma, (phi ∨ psi) ⊢ Compositon(A) ⊆r Gamma ⊢ Compositon(A) BY
               (Assert ⌜sub_cubical_set{j:l}(Gamma; Gamma, (phi ∨ psi))⌝⋅
                THEN Auto
                THEN BLemma `face-1-implies-subset`
                THEN Auto
                THEN RepeatFor 2 (ParallelOp 5)
                THEN RepeatFor 2 (ParallelLast)
                THEN RWO  "face-or-eq-1" 0
                THEN Auto))
   THEN HypSubst' (-2) 0
   THEN Auto) }

---

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)
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(A)


By

---

Latex:
((Assert  (if  phi  then  A  else  B)  =  A  BY
                (SubsumeC  \mkleeneopen{}\{Gamma,  phi  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
                  THENL  [(Fold  `same-cubical-type`  0
                                  THEN  UsingVars  [`psi']  (BLemma    `case-type-same1`)
                                  THEN  Auto)
                              ;  ((BLemma  `subset-cubical-type`  THENA  Auto)
                                    THEN  BLemma  `face-1-implies-subset`
                                    THEN  Auto)]
                ))
  THEN  (Assert  Gamma,  (phi  \mvee{}  psi)  \mvdash{}  Compositon(A)  \msubseteq{}r  Gamma  \mvdash{}  Compositon(A)  BY
                          (Assert  \mkleeneopen{}sub\_cubical\_set\{j:l\}(Gamma;  Gamma,  (phi  \mvee{}  psi))\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  BLemma  `face-1-implies-subset`
                            THEN  Auto
                            THEN  RepeatFor  2  (ParallelOp  5)
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  RWO    "face-or-eq-1"  0
                            THEN  Auto))
  THEN  HypSubst'  (-2)  0
  THEN  Auto)

---

Home Index