---

Step * 1 1 of Lemma equiv-path1-0


1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. equiv-path1(G;A;B;f) = (if (q=0) then (A)p else (B)p) ∈ {G.𝕀, ((q=0) ∨ (q=1)) ⊢ _}
6. Z : {G.𝕀, ((q=0) ∨ (q=1)) ⊢ _}
⊢ G ⊢ (Z)[0(𝕀)]
BY
{ SubsumeC ⌜{G, (((q=0) ∨ (q=1)))[0(𝕀)] ⊢ _}⌝⋅ }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. equiv-path1(G;A;B;f) = (if (q=0) then (A)p else (B)p) ∈ {G.𝕀, ((q=0) ∨ (q=1)) ⊢ _}
6. Z : {G.𝕀, ((q=0) ∨ (q=1)) ⊢ _}
⊢ G, (((q=0) ∨ (q=1)))[0(𝕀)] ⊢ (Z)[0(𝕀)]

2
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. equiv-path1(G;A;B;f) = (if (q=0) then (A)p else (B)p) ∈ {G.𝕀, ((q=0) ∨ (q=1)) ⊢ _}
6. Z : {G.𝕀, ((q=0) ∨ (q=1)) ⊢ _}
7. (Z)[0(𝕀)] = (Z)[0(𝕀)] ∈ {G, (((q=0) ∨ (q=1)))[0(𝕀)] ⊢ _}
⊢ {G, (((q=0) ∨ (q=1)))[0(𝕀)] ⊢ _} ⊆r {G ⊢ _}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:Equiv(A;B)\}
5.  equiv-path1(G;A;B;f)  =  (if  (q=0)  then  (A)p  else  (B)p)
6.  Z  :  \{G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  \_\}
\mvdash{}  G  \mvdash{}  (Z)[0(\mBbbI{})]


By

---

Latex:
SubsumeC  \mkleeneopen{}\{G,  (((q=0)  \mvee{}  (q=1)))[0(\mBbbI{})]  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}

---

Home Index