---

Step * of Lemma glue-comp-agrees

No Annotations
∀[G:j⊢]. ∀[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)  = cT ∈ G, psi ⊢ Compositon(T))
BY
{ (Intros
   THEN Symmetry
   THEN D -2
   THEN EqTypeCD
   THEN Auto
   THEN Try ((BLemma `uniform-comp-function-cumulativity` THEN Auto))
   THEN Unfold `composition-function` 0
   THEN RepeatFor 5 ((FunExt THENA Auto))
   THEN RenameVar `b' (-2)
   THEN RenameVar `b0' (-1)
   THEN (Assert G ⊢ Glue [psi ⊢→ (T;equiv-fun(f))] A BY
               Auto)
   THEN SwapVars `phi' `psi'
   THEN (InstLemma `csm-glue-type` [⌜G⌝;⌜A⌝;⌜phi⌝;⌜T⌝;⌜equiv-fun(f)⌝;⌜H.𝕀⌝;⌜sigma⌝]⋅ THENA Auto)
   THEN (EqTypeCD THENL [Id; ((GenConclTerm ⌜cT H sigma psi b b0⌝⋅ THENA Auto) THEN D -2 THEN Eq); Auto])) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. phi : {G ⊢ _:𝔽}
5. T : {G, phi ⊢ _}
6. cT : composition-function{[i | j]:l, i:l}(G, phi; T)
7. uniform-comp-function{[i | j]:l, i:l}(G, phi; T; cT)
8. f : {G, phi ⊢ _:Equiv(T;A)}
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ G, phi
11. psi : {H ⊢ _:𝔽}
12. b : {H, psi.𝕀 ⊢ _:(T)sigma}
13. b0 : {H ⊢ _:((T)sigma)[0(𝕀)][psi |⟶ (b)[0(𝕀)]]}
14. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
15. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
⊢ (cT H sigma psi b b0) = (comp(Glue [phi ⊢→ (T, f)] A)  H sigma psi b b0) ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \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)    =  cT)


By

---

Latex:
(Intros
  THEN  Symmetry
  THEN  D  -2
  THEN  EqTypeCD
  THEN  Auto
  THEN  Try  ((BLemma  `uniform-comp-function-cumulativity`  THEN  Auto))
  THEN  Unfold  `composition-function`  0
  THEN  RepeatFor  5  ((FunExt  THENA  Auto))
  THEN  RenameVar  `b'  (-2)
  THEN  RenameVar  `b0'  (-1)
  THEN  (Assert  G  \mvdash{}  Glue  [psi  \mvdash{}\mrightarrow{}  (T;equiv-fun(f))]  A  BY
                          Auto)
  THEN  SwapVars  `phi'  `psi'
  THEN  (InstLemma  `csm-glue-type`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}equiv-fun(f)\mkleeneclose{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}sigma\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (EqTypeCD
              THENL  [Id;  ((GenConclTerm  \mkleeneopen{}cT  H  sigma  psi  b  b0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Eq);  Auto]
  ))

---

Home Index