---

Step * of Lemma csm-glue-comp-agrees

No Annotations
∀[H,G:j⊢]. ∀[tau:H j⟶ G]. ∀[A:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[psi:{G ⊢ _:𝔽}]. ∀[T:{G, psi ⊢ _}].
∀[cT:G, psi +⊢ Compositon(T)]. ∀[f:{G, psi ⊢ _:Equiv(T;A)}].
  (comp(Glue [psi ⊢→ (T, f)] A) )tau = (cT)tau ∈ H ⊢ Compositon((T)tau) supposing H ⊢ (1(𝔽) ⇒ (psi)tau)
BY
{ (Intros
   THEN (RWO "csm-glue-comp" 0 THENA Auto)
   THEN ((Assert (cT)tau ∈ H, (psi)tau +⊢ Compositon((T)tau) BY
                ((InstLemmaIJ `csm-comp-structure_wf` [⌜G, psi⌝; ⌜H, (psi)tau⌝;⌜tau⌝;⌜T⌝;⌜cT⌝]⋅ THENA Auto)
                 THEN NthHypSq (-1)
                 THEN CsmUnfoldingComp))
         THENM Assert ⌜(f)tau ∈ {H, (psi)tau ⊢ _:Equiv((T)tau;(A)tau)}⌝⋅
         THENM (BLemma `glue-comp-agrees2` THEN Auto))) }

1
.....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)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,G:j\mvdash{}].  \mforall{}[tau:H  j{}\mrightarrow{}  G].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[psi:\{G  \mvdash{}  \_:\mBbbF{}\}].
\mforall{}[T:\{G,  psi  \mvdash{}  \_\}].  \mforall{}[cT:G,  psi  +\mvdash{}  Compositon(T)].  \mforall{}[f:\{G,  psi  \mvdash{}  \_:Equiv(T;A)\}].
    (comp(Glue  [psi  \mvdash{}\mrightarrow{}  (T,  f)]  A)  )tau  =  (cT)tau  supposing  H  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (psi)tau)


By

---

Latex:
(Intros
  THEN  (RWO  "csm-glue-comp"  0  THENA  Auto)
  THEN  ((Assert  (cT)tau  \mmember{}  H,  (psi)tau  +\mvdash{}  Compositon((T)tau)  BY
                            ((InstLemmaIJ  `csm-comp-structure\_wf`  [\mkleeneopen{}G,  psi\mkleeneclose{};  \mkleeneopen{}H,  (psi)tau\mkleeneclose{};\mkleeneopen{}tau\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}cT\mkleeneclose{}]\mcdot{}
                                THENA  Auto
                                )
                              THEN  NthHypSq  (-1)
                              THEN  CsmUnfoldingComp))
              THENM  Assert  \mkleeneopen{}(f)tau  \mmember{}  \{H,  (psi)tau  \mvdash{}  \_:Equiv((T)tau;(A)tau)\}\mkleeneclose{}\mcdot{}
              THENM  (BLemma  `glue-comp-agrees2`  THEN  Auto)))

---

Home Index