---

Step * of Lemma csm-pres

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}]. ∀[A,T:{G.𝕀 ⊢ _}]. ∀[f:{G.𝕀 ⊢ _:(T ⟶ A)}]. ∀[t:{G.𝕀, (phi)p ⊢ _:T}].
∀[t0:{G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}]. ∀[cT:G.𝕀 +⊢ Compositon(T)]. ∀[cA:G.𝕀 +⊢ Compositon(A)]. ∀[H:j⊢]. ∀[s:H j⟶ G].
  ((pres f [phi ⊢→ t] t0)s
  = pres (f)s+ [(phi)s ⊢→ (t)s+] (t0)s
  ∈ {H ⊢ _:(Path_((A)s+)[1(𝕀)] pres-c1(H;(phi)s;(f)s+;(t)s+;(t0)s;(cA)s+) pres-c2(H;(phi)s;(f)s+;(t)s+;(t0)s;(cT)s+))})
BY
{ (Intros
   THEN Unhide
   THEN (InstLemma `csm+_wf` [⌜G⌝;⌜H⌝;⌜𝕀⌝;⌜s⌝]⋅ THENA Auto)
   THEN (RWO "csm-interval-type" (-1) THENA Auto)) }

1
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G.𝕀 ⊢ _}
4. T : {G.𝕀 ⊢ _}
5. f : {G.𝕀 ⊢ _:(T ⟶ A)}
6. t : {G.𝕀, (phi)p ⊢ _:T}
7. t0 : {G ⊢ _:(T)[0(𝕀)][phi |⟶ t[0]]}
8. cT : G.𝕀 +⊢ Compositon(T)
9. cA : G.𝕀 +⊢ Compositon(A)
10. H : CubicalSet{j}
11. s : H j⟶ G
12. s+ ∈ H.𝕀 ij⟶ G.𝕀
⊢ (pres f [phi ⊢→ t] t0)s
= pres (f)s+ [(phi)s ⊢→ (t)s+] (t0)s
∈ {H ⊢ _:(Path_((A)s+)[1(𝕀)] pres-c1(H;(phi)s;(f)s+;(t)s+;(t0)s;(cA)s+) pres-c2(H;(phi)s;(f)s+;(t)s+;(t0)s;(cT)s+))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A,T:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[f:\{G.\mBbbI{}  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[t:\{G.\mBbbI{},  (phi)p  \mvdash{}  \_:T\}].
\mforall{}[t0:\{G  \mvdash{}  \_:(T)[0(\mBbbI{})][phi  |{}\mrightarrow{}  t[0]]\}].  \mforall{}[cT:G.\mBbbI{}  +\mvdash{}  Compositon(T)].  \mforall{}[cA:G.\mBbbI{}  +\mvdash{}  Compositon(A)].
\mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].
    ((pres  f  [phi  \mvdash{}\mrightarrow{}  t]  t0)s  =  pres  (f)s+  [(phi)s  \mvdash{}\mrightarrow{}  (t)s+]  (t0)s)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (InstLemma  `csm+\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "csm-interval-type"  (-1)  THENA  Auto))

---

Home Index