---

Step * of Lemma csm-pres-c2

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)]. ∀[H:j⊢]. ∀[s:H j⟶ G].
  ((pres-c2(G;phi;f;t;t0;cT))s
  = pres-c2(H;(phi)s;(f)s+;(t)s+;(t0)s;(cT)s+)
  ∈ {H ⊢ _:((A)s+)[1(𝕀)][(phi)s |⟶ app((f)s+; (t)s+)[1]]})
BY
{ (InstLemma `pres-c2_wf` []
   THEN RepeatFor 8 (ParallelLast')
   THEN Intros
   THEN (Assert ⌜app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}⌝⋅
         THENA ((Assert ⌜f ∈ {G.𝕀, (phi)p ⊢ _:(T ⟶ A)}⌝⋅ THENA Auto)
                THEN CubicalAppFun⋅
                THEN RWW "cubical-fun-subset" 0
                THEN Auto)
         )
   THEN (MemTypeHD (-4) THENA Auto)
   THEN (Assert ⌜partial-term-1(H;app((f)s+; (t)s+)) = (pres-c2(G;phi;f;t;t0;cT))s ∈ {H, (phi)s ⊢ _:((A)s+)[1(𝕀)]}⌝⋅
   THENM (MemTypeCD THEN Auto)
   )) }

1
.....assertion..... 
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. pres-c2(G;phi;f;t;t0;cT) = pres-c2(G;phi;f;t;t0;cT) ∈ {G ⊢ _:(A)[1(𝕀)]}
10. partial-term-1(G;app(f; t)) = pres-c2(G;phi;f;t;t0;cT) ∈ {G, phi ⊢ _:(A)[1(𝕀)]}
11. H : CubicalSet{j}
12. s : H j⟶ G
13. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
⊢ partial-term-1(H;app((f)s+; (t)s+)) = (pres-c2(G;phi;f;t;t0;cT))s ∈ {H, (phi)s ⊢ _:((A)s+)[1(𝕀)]}

2
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. pres-c2(G;phi;f;t;t0;cT) = pres-c2(G;phi;f;t;t0;cT) ∈ {G ⊢ _:(A)[1(𝕀)]}
10. partial-term-1(G;app(f; t)) = pres-c2(G;phi;f;t;t0;cT) ∈ {G, phi ⊢ _:(A)[1(𝕀)]}
11. H : CubicalSet{j}
12. s : H j⟶ G
13. app(f; t) ∈ {G.𝕀, (phi)p ⊢ _:A}
14. partial-term-1(H;app((f)s+; (t)s+)) = (pres-c2(G;phi;f;t;t0;cT))s ∈ {H, (phi)s ⊢ _:((A)s+)[1(𝕀)]}
⊢ (pres-c2(G;phi;f;t;t0;cT))s = pres-c2(H;(phi)s;(f)s+;(t)s+;(t0)s;(cT)s+) ∈ {H ⊢ _:((A)s+)[1(𝕀)]}

---

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{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].
    ((pres-c2(G;phi;f;t;t0;cT))s  =  pres-c2(H;(phi)s;(f)s+;(t)s+;(t0)s;(cT)s+))


By

---

Latex:
(InstLemma  `pres-c2\_wf`  []
  THEN  RepeatFor  8  (ParallelLast')
  THEN  Intros
  THEN  (Assert  \mkleeneopen{}app(f;  t)  \mmember{}  \{G.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}
              THENA  ((Assert  \mkleeneopen{}f  \mmember{}  \{G.\mBbbI{},  (phi)p  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  CubicalAppFun\mcdot{}
                            THEN  RWW  "cubical-fun-subset"  0
                            THEN  Auto)
              )
  THEN  (MemTypeHD  (-4)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}partial-term-1(H;app((f)s+;  (t)s+))  =  (pres-c2(G;phi;f;t;t0;cT))s\mkleeneclose{}\mcdot{}
  THENM  (MemTypeCD  THEN  Auto)
  ))

---

Home Index