---

Step * 2 1 of Lemma equiv-path1-1


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWW  "csm-case-type  csm-face-zero"  0  THENA  Auto)
  THEN  (Subst'  (q)[1(\mBbbI{})]  \msim{}  1(\mBbbI{})  0  THENA  (CsmUnfolding  THEN  Auto))
  )

---

Home Index