---

Step * of Lemma equiv-path1-constraint

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(A;B)}].
  G.𝕀, ((q=0) ∨ (q=1)) ⊢ equiv-path1(G;A;B;f) = (if (q=0) then (A)p else (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 (InstLemma `glue-type-constraint` [⌜G.𝕀⌝;⌜(B)p⌝;⌜((q=0) ∨ (q=1))⌝;⌜(if (q=0) then (A)p else (B)p)⌝;
         ⌜equiv-fun(cubical-equiv-by-cases(G;B;f))⌝]⋅
         THENA Auto
         )
   THEN Fold `equiv-path1` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(A;B)\}].
    G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  equiv-path1(G;A;B;f)  =  (if  (q=0)  then  (A)p  else  (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  (InstLemma  `glue-type-constraint`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}((q=0)  \mvee{}  (q=1))\mkleeneclose{};
              \mkleeneopen{}(if  (q=0)  then  (A)p  else  (B)p)\mkleeneclose{};\mkleeneopen{}equiv-fun(cubical-equiv-by-cases(G;B;f))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `equiv-path1`  (-1)
  THEN  Trivial)

---

Home Index