---

Step * of Lemma csm-cubical-equiv-by-cases

No Annotations
∀G:j⊢. ∀A,B:{G ⊢ _}. ∀f:{G ⊢ _:Equiv(A;B)}. ∀H:j⊢. ∀s:H j⟶ G.
  ((cubical-equiv-by-cases(G;B;f))s+
  = cubical-equiv-by-cases(H;(B)s;(f)s)
  ∈ {H.𝕀, ((q=0) ∨ (q=1)) ⊢ _:Equiv((if (q=0) then ((A)s)p else ((B)s)p);((B)s)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 (Assert ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((A)s)p BY
               ((D 0 THENA Auto) THEN SubsumeC ⌜{H.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN (Assert ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((B)s)p BY
               ((D 0 THENA Auto) THEN SubsumeC ⌜{H.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN Unfold `cubical-equiv-by-cases` 0
   THEN (RWO "csm-case-term" 0 THENA Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p
8. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p
9. ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((A)s)p
10. ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((B)s)p
⊢ (((f)p)s+ ∨ (IdEquiv(G.𝕀, (q=1);(B)p))s+)
= (((f)s)p ∨ IdEquiv(H.𝕀, (q=1);((B)s)p))
∈ {H.𝕀, ((q=0) ∨ (q=1)) ⊢ _:Equiv((if (q=0) then ((A)s)p else ((B)s)p);((B)s)p)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}G:j\mvdash{}.  \mforall{}A,B:\{G  \mvdash{}  \_\}.  \mforall{}f:\{G  \mvdash{}  \_:Equiv(A;B)\}.  \mforall{}H:j\mvdash{}.  \mforall{}s:H  j{}\mrightarrow{}  G.
    ((cubical-equiv-by-cases(G;B;f))s+  =  cubical-equiv-by-cases(H;(B)s;(f)s))


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  (Assert  \mforall{}phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  H.\mBbbI{},  phi  \mvdash{}  ((A)s)p  BY
                          ((D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}\{H.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  H.\mBbbI{},  phi  \mvdash{}  ((B)s)p  BY
                          ((D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}\{H.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Unfold  `cubical-equiv-by-cases`  0
  THEN  (RWO  "csm-case-term"  0  THENA  Auto))

---

Home Index