---

Step * of Lemma equiv-path1-0

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(A;B)}].  ((equiv-path1(G;A;B;f))[0(𝕀)] = A ∈ {G ⊢ _})
BY
{ (InstLemma `equiv-path1-constraint` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Unfold `same-cubical-type` -1
   THEN ApFunToHypEquands `Z' ⌜(Z)[0(𝕀)]⌝ ⌜{G ⊢ _}⌝ (-1)⋅) }

1
.....fun wf..... 
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)) ⊢ _}
⊢ (Z)[0(𝕀)] = (Z)[0(𝕀)] ∈ {G ⊢ _}

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. (equiv-path1(G;A;B;f))[0(𝕀)] = ((if (q=0) then (A)p else (B)p))[0(𝕀)] ∈ {G ⊢ _}
⊢ (equiv-path1(G;A;B;f))[0(𝕀)] = A ∈ {G ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(A;B)\}].    ((equiv-path1(G;A;B;f))[0(\mBbbI{})]  =  A)


By

---

Latex:
(InstLemma  `equiv-path1-constraint`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Unfold  `same-cubical-type`  -1
  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}(Z)[0(\mBbbI{})]\mkleeneclose{}  \mkleeneopen{}\{G  \mvdash{}  \_\}\mkleeneclose{}  (-1)\mcdot{})

---

Home Index