---

Step * of Lemma csm-filling_term

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)]. ∀[u:{Gamma.𝕀, (phi)p ⊢ _:A}].
∀[a0:{Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ Gamma].
  ((fill cA [phi ⊢→ u] a0)s+ = fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]})
BY
{ (InstLemma `csm-fill_term` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Intro
   THEN (InstHyp [cop-to-cfun(cA)] (-2)⋅ THENA Auto)
   THEN Thin (-3)
   THEN RepeatFor 4 (ParallelLast')
   THEN (Subst' (cop-to-cfun(cA))s+ ~ cop-to-cfun((cA)s+) -1 THENM (Fold `filling_term` (-1) THEN Trivial))) }

1
.....equality..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ CompOp(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. (fill cop-to-cfun(cA) [phi ⊢→ u] a0)s+
= fill (cop-to-cfun(cA))s+ [(phi)s ⊢→ (u)s+] (a0)s
∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}
⊢ (cop-to-cfun(cA))s+ ~ cop-to-cfun((cA)s+)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  CompOp(A)].
\mforall{}[u:\{Gamma.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}].  \mforall{}[a0:\{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  u[0]]\}].  \mforall{}[Delta:j\mvdash{}].
\mforall{}[s:Delta  j{}\mrightarrow{}  Gamma].
    ((fill  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0)s+  =  fill  (cA)s+  [(phi)s  \mvdash{}\mrightarrow{}  (u)s+]  (a0)s)


By

---

Latex:
(InstLemma  `csm-fill\_term`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Intro
  THEN  (InstHyp  [cop-to-cfun(cA)]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (Subst'  (cop-to-cfun(cA))s+  \msim{}  cop-to-cfun((cA)s+)  -1
  THENM  (Fold  `filling\_term`  (-1)  THEN  Trivial)
  ))

---

Home Index