---

Step * of Lemma csm-equiv-path1

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(A;B)}]. ∀[H:j⊢]. ∀[s:H j⟶ G].
  ((equiv-path1(G;A;B;f))s+ = equiv-path1(H;(A)s;(B)s;(f)s) ∈ {H.𝕀 ⊢ _})
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 `equiv-path1` 0
   THEN (InstLemma `csm-glue-type` [⌜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))⌝;⌜H.𝕀⌝;⌜s+⌝]⋅
         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
11. (Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then (A)p else (B)p);equiv-fun(cubical-equiv-by-cases(G;B;f)))] (B)p)s+
= H.𝕀 ⊢ Glue [(((q=0) ∨ (q=1)))s+ ⊢→ (((if (q=0) then (A)p else (B)p))
                                       s+;(equiv-fun(cubical-equiv-by-cases(G;B;f)))s+)] ((B)p)s+
∈ {H.𝕀 ⊢ _}
⊢ (Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then (A)p else (B)p);equiv-fun(cubical-equiv-by-cases(G;B;f)))] (B)p)s+
= H.𝕀 ⊢ Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then ((A)s)p else ((B)s)
                                                               p);equiv-fun(cubical-equiv-by-cases(H;(B)s;(f)s)))] ((B)
                                                                                                                     s)p
∈ {H.𝕀 ⊢ _}

---

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].
    ((equiv-path1(G;A;B;f))s+  =  equiv-path1(H;(A)s;(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  `equiv-path1`  0
  THEN  (InstLemma  `csm-glue-type`  [\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{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}s+\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index