---

Step * 2 1 of Lemma equiv-path1-0


1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
⊢ A = ((if (q=0) then (A)p else (B)p))[0(𝕀)] ∈ {G ⊢ _}
BY
{ ((RWW "csm-case-type csm-face-zero" 0 THENA Auto) THEN SubsumeC  ⌜{G, ((q)[0(𝕀)]=0) ⊢ _}⌝⋅) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
⊢ A = (if ((q)[0(𝕀)]=0) then ((A)p)[0(𝕀)] else ((B)p)[0(𝕀)]) ∈ {G, ((q)[0(𝕀)]=0) ⊢ _}

2
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. A = (if ((q)[0(𝕀)]=0) then ((A)p)[0(𝕀)] else ((B)p)[0(𝕀)]) ∈ {G, ((q)[0(𝕀)]=0) ⊢ _}
⊢ {G, ((q)[0(𝕀)]=0) ⊢ _} ⊆r {G ⊢ _}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
\mvdash{}  A  =  ((if  (q=0)  then  (A)p  else  (B)p))[0(\mBbbI{})]


By

---

Latex:
((RWW  "csm-case-type  csm-face-zero"  0  THENA  Auto)  THEN  SubsumeC    \mkleeneopen{}\{G,  ((q)[0(\mBbbI{})]=0)  \mvdash{}  \_\}\mkleeneclose{}\mcdot{})

---

Home Index