Step
*
of Lemma
map-path_wf
No Annotations
∀[G:j⊢]. ∀[S,T:{G ⊢ _}]. ∀[f:{G ⊢ _:(S ⟶ T)}]. ∀[a,b:{G ⊢ _:S}]. ∀[pth:{G ⊢ _:(Path_S a b)}].
(map-path(G;f;pth) ∈ {G ⊢ _:(Path_T app(f; a) app(f; b))})
BY
{ ((Auto
THEN (Assert {G.𝕀 ⊢ _:((S ⟶ T))p} = {G.𝕀 ⊢ _:((S)p ⟶ (T)p)} ∈ 𝕌{[i' | j']} BY
(EqCDA THEN Auto))
THEN (Assert (f)p ∈ {G.𝕀 ⊢ _:((S)p ⟶ (T)p)} BY
((Assert (f)p ∈ {G.𝕀 ⊢ _:((S ⟶ T))p} BY Auto) THEN InferEqualTypeUp THEN Eq)))
THEN Unfold `map-path` 0
THEN (InstLemma `term-to-path_wf` [⌜G⌝;⌜T⌝;⌜app((f)p; path-eta(pth))⌝]⋅ THENA Auto)
THEN InferEqualType
THEN Auto
THEN EqCDA
THEN (RWO "csm-cubical-app" 0 THENA Auto)
THEN Symmetry
THEN EqCDA
THEN RWW "path-eta-0 path-eta-1" 0
THEN Auto
THEN Symmetry
THEN Fold `cubical-path-app` 0
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[G:j\mvdash{}]. \mforall{}[S,T:\{G \mvdash{} \_\}]. \mforall{}[f:\{G \mvdash{} \_:(S {}\mrightarrow{} T)\}]. \mforall{}[a,b:\{G \mvdash{} \_:S\}]. \mforall{}[pth:\{G \mvdash{} \_:(Path\_S a b)\}].
(map-path(G;f;pth) \mmember{} \{G \mvdash{} \_:(Path\_T app(f; a) app(f; b))\})
By
Latex:
((Auto
THEN (Assert \{G.\mBbbI{} \mvdash{} \_:((S {}\mrightarrow{} T))p\} = \{G.\mBbbI{} \mvdash{} \_:((S)p {}\mrightarrow{} (T)p)\} BY
(EqCDA THEN Auto))
THEN (Assert (f)p \mmember{} \{G.\mBbbI{} \mvdash{} \_:((S)p {}\mrightarrow{} (T)p)\} BY
((Assert (f)p \mmember{} \{G.\mBbbI{} \mvdash{} \_:((S {}\mrightarrow{} T))p\} BY Auto) THEN InferEqualTypeUp THEN Eq)))
THEN Unfold `map-path` 0
THEN (InstLemma `term-to-path\_wf` [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}app((f)p; path-eta(pth))\mkleeneclose{}]\mcdot{} THENA Auto)
THEN InferEqualType
THEN Auto
THEN EqCDA
THEN (RWO "csm-cubical-app" 0 THENA Auto)
THEN Symmetry
THEN EqCDA
THEN RWW "path-eta-0 path-eta-1" 0
THEN Auto
THEN Symmetry
THEN Fold `cubical-path-app` 0
THEN Auto)
Home
Index