---

Step * of Lemma trans-const-path_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[a:{G ⊢ _:A}].
  (trans-const-path(G;cA;a) ∈ {G ⊢ _:(Path_A transprt-const(G;cA;a) a)})
BY
{ ((ProveWfLemma
    THEN (InstLemma `rev_fill_term_wf` [⌜G⌝;⌜0(𝔽)⌝;⌜(A)p⌝;⌜(cA)p⌝]⋅ THENA Auto)
    THEN (RWO  "csm-face-0" (-1) THENA Auto))
   THEN (Assert discr(⋅) ∈ {G.𝕀, 0(𝔽) ⊢ _:(A)p} BY
               Auto)
   THEN (Assert a ∈ {G ⊢ _:((A)p)[1(𝕀)][0(𝔽) |⟶ discr(⋅)[1]]} BY
               (MemTypeCD THEN Auto))
   THEN (Assert rev_fill_term(G;(cA)p;0(𝔽);discr(⋅);a) ∈ {G.𝕀 ⊢ _:(A)p} BY
               BackThruSomeHyp)
   THEN (BLemma `term-to-path-wf` THENW Auto)
   THEN RWO  "rev_fill_term_0 rev_fill_term_1" 0
   THEN Try (RWO "csm-face-0" 0)
   THEN Auto
   THEN UnfoldTopAb 0
   THEN Auto) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. ∀[u:{G.𝕀, 0(𝔽) ⊢ _:(A)p}]. ∀[a1:{G ⊢ _:((A)p)[1(𝕀)][0(𝔽) |⟶ u[1]]}].
     (rev_fill_term(G;(cA)p;0(𝔽);u;a1) ∈ {G.𝕀 ⊢ _:(A)p[0(𝔽) |⟶ u]})
6. discr(⋅) ∈ {G.𝕀, 0(𝔽) ⊢ _:(A)p}
7. a ∈ {G ⊢ _:((A)p)[1(𝕀)][0(𝔽) |⟶ discr(⋅)[1]]}
8. rev_fill_term(G;(cA)p;0(𝔽);discr(⋅);a) ∈ {G.𝕀 ⊢ _:(A)p}
⊢ comp rev-type-comp(G;(cA)p) [0(𝔽) ⊢→ (discr(⋅))(p;1-(q))] a = transprt-const(G;cA;a) ∈ {G ⊢ _:A}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[a:\{G  \mvdash{}  \_:A\}].
    (trans-const-path(G;cA;a)  \mmember{}  \{G  \mvdash{}  \_:(Path\_A  transprt-const(G;cA;a)  a)\})


By

---

Latex:
((ProveWfLemma
    THEN  (InstLemma  `rev\_fill\_term\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}0(\mBbbF{})\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(cA)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (RWO    "csm-face-0"  (-1)  THENA  Auto))
  THEN  (Assert  discr(\mcdot{})  \mmember{}  \{G.\mBbbI{},  0(\mBbbF{})  \mvdash{}  \_:(A)p\}  BY
                          Auto)
  THEN  (Assert  a  \mmember{}  \{G  \mvdash{}  \_:((A)p)[1(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  discr(\mcdot{})[1]]\}  BY
                          (MemTypeCD  THEN  Auto))
  THEN  (Assert  rev\_fill\_term(G;(cA)p;0(\mBbbF{});discr(\mcdot{});a)  \mmember{}  \{G.\mBbbI{}  \mvdash{}  \_:(A)p\}  BY
                          BackThruSomeHyp)
  THEN  (BLemma  `term-to-path-wf`  THENW  Auto)
  THEN  RWO    "rev\_fill\_term\_0  rev\_fill\_term\_1"  0
  THEN  Try  (RWO  "csm-face-0"  0)
  THEN  Auto
  THEN  UnfoldTopAb  0
  THEN  Auto)

---

Home Index