---

Step * of Lemma glue-comp_wf

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)  ∈ composition-function{j:l,i:l}(G;Glue [psi ⊢→ (T;equiv-fun(f))] A))
BY
{ (Intros
   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 (Assert b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma} BY
               (SubsumeC  ⌜{H, psi.𝕀 ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}⌝⋅
                THEN Try ((InferEqualTypeGen THEN Try (Trivial) THEN EqCD THEN Auto))
                THEN BLemma `subset-cubical-term`
                THEN Auto))) }

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


By

---

Latex:
(Intros
  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  (Assert  b  \mmember{}  \{H.\mBbbI{},  (psi)p  \mvdash{}  \_:Glue  [(phi)sigma  \mvdash{}\mrightarrow{}  ((T)sigma;(equiv-fun(f))sigma)]  (A)sigma\}  BY
                          (SubsumeC    \mkleeneopen{}\{H,  psi.\mBbbI{}  \mvdash{}  \_:Glue  [(phi)sigma  \mvdash{}\mrightarrow{}  ((T)sigma;(equiv-fun(f))sigma)]
                                                                                        (A)sigma\}\mkleeneclose{}\mcdot{}
                            THEN  Try  ((InferEqualTypeGen  THEN  Try  (Trivial)  THEN  EqCD  THEN  Auto))
                            THEN  BLemma  `subset-cubical-term`
                            THEN  Auto)))

---

Home Index