---

Step * 1 of Lemma csm-glue-comp-agrees

.....assertion..... 
1. H : CubicalSet{j}
2. G : CubicalSet{j}
3. tau : H j⟶ G
4. A : {G ⊢ _}
5. cA : G +⊢ Compositon(A)
6. psi : {G ⊢ _:𝔽}
7. T : {G, psi ⊢ _}
8. cT : G, psi +⊢ Compositon(T)
9. f : {G, psi ⊢ _:Equiv(T;A)}
10. H ⊢ (1(𝔽) ⇒ (psi)tau)
11. (cT)tau ∈ H, (psi)tau +⊢ Compositon((T)tau)
⊢ (f)tau ∈ {H, (psi)tau ⊢ _:Equiv((T)tau;(A)tau)}
BY
{ (InstLemma `csm-ap-term_wf` [⌜H, (psi)tau⌝;⌜G, psi⌝;⌜Equiv(T;A)⌝;⌜tau⌝;⌜f⌝]⋅ THENA Auto) }

1
1. H : CubicalSet{j}
2. G : CubicalSet{j}
3. tau : H j⟶ G
4. A : {G ⊢ _}
5. cA : G +⊢ Compositon(A)
6. psi : {G ⊢ _:𝔽}
7. T : {G, psi ⊢ _}
8. cT : G, psi +⊢ Compositon(T)
9. f : {G, psi ⊢ _:Equiv(T;A)}
10. H ⊢ (1(𝔽) ⇒ (psi)tau)
11. (cT)tau ∈ H, (psi)tau +⊢ Compositon((T)tau)
12. (f)tau ∈ {H, (psi)tau ⊢ _:(Equiv(T;A))tau}
⊢ (f)tau ∈ {H, (psi)tau ⊢ _:Equiv((T)tau;(A)tau)}

---

Latex:

---

Latex:
.....assertion..... 
1.  H  :  CubicalSet\{j\}
2.  G  :  CubicalSet\{j\}
3.  tau  :  H  j{}\mrightarrow{}  G
4.  A  :  \{G  \mvdash{}  \_\}
5.  cA  :  G  +\mvdash{}  Compositon(A)
6.  psi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
7.  T  :  \{G,  psi  \mvdash{}  \_\}
8.  cT  :  G,  psi  +\mvdash{}  Compositon(T)
9.  f  :  \{G,  psi  \mvdash{}  \_:Equiv(T;A)\}
10.  H  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (psi)tau)
11.  (cT)tau  \mmember{}  H,  (psi)tau  +\mvdash{}  Compositon((T)tau)
\mvdash{}  (f)tau  \mmember{}  \{H,  (psi)tau  \mvdash{}  \_:Equiv((T)tau;(A)tau)\}


By

---

Latex:
(InstLemma  `csm-ap-term\_wf`  [\mkleeneopen{}H,  (psi)tau\mkleeneclose{};\mkleeneopen{}G,  psi\mkleeneclose{};\mkleeneopen{}Equiv(T;A)\mkleeneclose{};\mkleeneopen{}tau\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index