---

Step * 2 of Lemma csm-pres-c2


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(𝕀)]}
BY
{ (Unfold `pres-c2` 0
   THEN (RWO "csm-cubical-app" 0 THENA Auto)
   THEN (InstLemma `csm-comp_term` [⌜G⌝;⌜phi⌝;⌜T⌝;⌜cT⌝;⌜t⌝;⌜t0⌝;⌜H⌝;⌜s⌝]⋅ 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. 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(𝕀)]}
15. (comp cT [phi ⊢→ t] t0)s = comp (cT)s+ [(phi)s ⊢→ (t)s+] (t0)s ∈ {H ⊢ _:((T)s+)[1(𝕀)][(phi)s |⟶ ((t)s+)[1(𝕀)]]}
⊢ app(((f)[1(𝕀)])s; (comp cT [phi ⊢→ t] t0)s)
= app(((f)s+)[1(𝕀)]; comp (cT)s+ [(phi)s ⊢→ (t)s+] (t0)s)
∈ {H ⊢ _:((A)s+)[1(𝕀)]}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{G.\mBbbI{}  \mvdash{}  \_\}
4.  T  :  \{G.\mBbbI{}  \mvdash{}  \_\}
5.  f  :  \{G.\mBbbI{}  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
6.  t  :  \{G.\mBbbI{},  (phi)p  \mvdash{}  \_:T\}
7.  t0  :  \{G  \mvdash{}  \_:(T)[0(\mBbbI{})][phi  |{}\mrightarrow{}  t[0]]\}
8.  cT  :  G.\mBbbI{}  \mvdash{}  Compositon(T)
9.  pres-c2(G;phi;f;t;t0;cT)  =  pres-c2(G;phi;f;t;t0;cT)
10.  partial-term-1(G;app(f;  t))  =  pres-c2(G;phi;f;t;t0;cT)
11.  H  :  CubicalSet\{j\}
12.  s  :  H  j{}\mrightarrow{}  G
13.  app(f;  t)  \mmember{}  \{G.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}
14.  partial-term-1(H;app((f)s+;  (t)s+))  =  (pres-c2(G;phi;f;t;t0;cT))s
\mvdash{}  (pres-c2(G;phi;f;t;t0;cT))s  =  pres-c2(H;(phi)s;(f)s+;(t)s+;(t0)s;(cT)s+)


By

---

Latex:
(Unfold  `pres-c2`  0
  THEN  (RWO  "csm-cubical-app"  0  THENA  Auto)
  THEN  (InstLemma  `csm-comp\_term`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}cT\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}t0\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index