---

Step * 1 of Lemma equiv-path2-1

.....assertion..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. cA : G +⊢ Compositon(A)
6. cB : G +⊢ Compositon(B)
7. G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)
⊢ case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p)
  ∈ G.𝕀, ((q=0) ∨ (q=1)) +⊢ Compositon((if (q=0) then (A)p else (B)p))
BY
{ ((GenConcl ⌜q = i ∈ {G.𝕀 ⊢ _:𝕀}⌝⋅ THENA Auto)
   THEN (Assert G.𝕀, (i=0) ⊢ (A)p BY
               (SubsumeC ⌜{G.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN (Assert G.𝕀, (i=1) ⊢ (B)p BY
               (SubsumeC ⌜{G.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN BLemma `case-type-comp-disjoint`
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:Equiv(A;B)\}
5.  cA  :  G  +\mvdash{}  Compositon(A)
6.  cB  :  G  +\mvdash{}  Compositon(B)
7.  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  (if  (q=0)  then  (A)p  else  (B)p)
\mvdash{}  case-type-comp(G.\mBbbI{};  (q=0);  (q=1);  (A)p;  (B)p;  (cA)p;  (cB)p)
    \mmember{}  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  +\mvdash{}  Compositon((if  (q=0)  then  (A)p  else  (B)p))


By

---

Latex:
((GenConcl  \mkleeneopen{}q  =  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  G.\mBbbI{},  (i=0)  \mvdash{}  (A)p  BY
                          (SubsumeC  \mkleeneopen{}\{G.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  G.\mBbbI{},  (i=1)  \mvdash{}  (B)p  BY
                          (SubsumeC  \mkleeneopen{}\{G.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  BLemma  `case-type-comp-disjoint`
  THEN  Auto)

---

Home Index