---

Step * 1 of Lemma csm-pres


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+))}
BY
{ Unfold `pres` 0 }

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.𝕀
⊢ (<>(comp (cA)p+ [((phi)p ∨ (q=1)) ⊢→ (presw(G;phi;f;t;t0;cT))p+] (pres-a0(G;f;t0))p))s
= H ⊢ <>(comp ((cA)s+)p+ [(((phi)s)p ∨ (q=1)) ⊢→ (presw(H;(phi)s;(f)s+;(t)s+;(t0)s;(cT)s+))p+]
             (pres-a0(H;(f)s+;(t0)s))p)
∈ {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:

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.  cA  :  G.\mBbbI{}  +\mvdash{}  Compositon(A)
10.  H  :  CubicalSet\{j\}
11.  s  :  H  j{}\mrightarrow{}  G
12.  s+  \mmember{}  H.\mBbbI{}  ij{}\mrightarrow{}  G.\mBbbI{}
\mvdash{}  (pres  f  [phi  \mvdash{}\mrightarrow{}  t]  t0)s  =  pres  (f)s+  [(phi)s  \mvdash{}\mrightarrow{}  (t)s+]  (t0)s


By

---

Latex:
Unfold  `pres`  0

---

Home Index