---

Step * of Lemma csm-fill_term

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(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
{ (Intros
   THEN Unhide
   THEN (Assert Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+) BY
               (RepeatFor 2 ((D 0 THENA Auto))
                THEN (D 0 THENM (NthHypSq (-1) THEN CsmUnfolding THEN Auto))
                THEN GenConcl ⌜((phi)s)p = psi ∈ {Delta.𝕀 ⊢ _:𝔽}⌝⋅
                THEN Auto))
   THEN (Assert (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+} BY
               (CsmApTermWfSubset THEN Auto))
   THEN Assert ⌜(a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}⌝⋅) }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(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. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
10. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
⊢ (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}

2
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(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. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
10. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
11. (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}
⊢ (fill cA [phi ⊢→ u] a0)s+ = fill (cA)s+ [(phi)s ⊢→ (u)s+] (a0)s ∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  Compositon(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:
(Intros
  THEN  Unhide
  THEN  (Assert  Delta.\mBbbI{}  \mvdash{}  (((phi)s)p  {}\mRightarrow{}  ((phi)p)s+)  BY
                          (RepeatFor  2  ((D  0  THENA  Auto))
                            THEN  (D  0  THENM  (NthHypSq  (-1)  THEN  CsmUnfolding  THEN  Auto))
                            THEN  GenConcl  \mkleeneopen{}((phi)s)p  =  psi\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  THEN  (Assert  (u)s+  \mmember{}  \{Delta.\mBbbI{},  ((phi)s)p  \mvdash{}  \_:(A)s+\}  BY
                          (CsmApTermWfSubset  THEN  Auto))
  THEN  Assert  \mkleeneopen{}(a0)s  \mmember{}  \{Delta  \mvdash{}  \_:((A)s+)[0(\mBbbI{})][(phi)s  |{}\mrightarrow{}  (u)s+[0]]\}\mkleeneclose{}\mcdot{})

---

Home Index