---

Step * of Lemma cubical-equiv-by-cases_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(A;B)}].
  (cubical-equiv-by-cases(G;B;f) ∈ {G.𝕀, ((q=0) ∨ (q=1)) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)})
BY
{ (Intros
   THEN (Assert ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p BY
               ((D 0 THENA Auto) THEN SubsumeC ⌜{G.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN (Assert ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p BY
               ((D 0 THENA Auto) THEN SubsumeC ⌜{G.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN Unfold `cubical-equiv-by-cases` 0
   THEN MemCD
   THEN Try (QuickAuto)) }

1
.....subterm..... T:t
3:n
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p
6. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p
⊢ IdEquiv(G.𝕀, (q=1);(B)p) ∈ {G.𝕀, (q=1) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)}

2
.....subterm..... T:t
2:n
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p
6. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p
⊢ (f)p ∈ {G.𝕀, (q=0) ⊢ _:Equiv((if (q=0) then (A)p else (B)p);(B)p)[(q=1) |⟶ IdEquiv(G.𝕀, (q=1);(B)p)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(A;B)\}].
    (cubical-equiv-by-cases(G;B;f)
      \mmember{}  \{G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  \_:Equiv((if  (q=0)  then  (A)p  else  (B)p);(B)p)\})


By

---

Latex:
(Intros
  THEN  (Assert  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (A)p  BY
                          ((D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}\{G.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (B)p  BY
                          ((D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}\{G.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Unfold  `cubical-equiv-by-cases`  0
  THEN  MemCD
  THEN  Try  (QuickAuto))

---

Home Index