---

Step * 1 of Lemma glue-comp-agrees


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(𝕀)]}
BY
{ ((Assert (T)sigma = H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma ∈ {H.𝕀 ⊢ _} BY
          ((Assert (T)sigma = (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma ∈ {H.𝕀 ⊢ _} BY
                  (EqCDA
                   THEN Symmetry
                   THEN (InstLemma `glue-type-constraint` [⌜G⌝;⌜A⌝;⌜phi⌝;⌜T⌝;⌜equiv-fun(f)⌝]⋅ THENA Auto)
                   THEN UnfoldTopAb (-1)
                   THEN Trivial))
           THEN NthHypEqGen (-1)
           THEN EqCDA
           THEN Auto))
   THEN (Assert {H.𝕀 ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}
               = {H.𝕀 ⊢ _:(T)sigma}
               ∈ 𝕌{[i' | j']} BY
               (EqCDA THEN 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.𝕀 ⊢ _}
16. (T)sigma = H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma ∈ {H.𝕀 ⊢ _}
17. {H.𝕀 ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma} = {H.𝕀 ⊢ _:(T)sigma} ∈ 𝕌{[i' | j']}
⊢ (cT H sigma psi b b0) = (comp(Glue [phi ⊢→ (T, f)] A)  H sigma psi b b0) ∈ {H ⊢ _:((T)sigma)[1(𝕀)]}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  cA  :  G  +\mvdash{}  Compositon(A)
4.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
5.  T  :  \{G,  phi  \mvdash{}  \_\}
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  \mvdash{}  \_:Equiv(T;A)\}
9.  H  :  CubicalSet\{j\}
10.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  G,  phi
11.  psi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
12.  b  :  \{H,  psi.\mBbbI{}  \mvdash{}  \_:(T)sigma\}
13.  b0  :  \{H  \mvdash{}  \_:((T)sigma)[0(\mBbbI{})][psi  |{}\mrightarrow{}  (b)[0(\mBbbI{})]]\}
14.  G  \mvdash{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;equiv-fun(f))]  A
15.  (Glue  [phi  \mvdash{}\mrightarrow{}  (T;equiv-fun(f))]  A)sigma
=  H.\mBbbI{}  \mvdash{}  Glue  [(phi)sigma  \mvdash{}\mrightarrow{}  ((T)sigma;(equiv-fun(f))sigma)]  (A)sigma
\mvdash{}  (cT  H  sigma  psi  b  b0)  =  (comp(Glue  [phi  \mvdash{}\mrightarrow{}  (T,  f)]  A)    H  sigma  psi  b  b0)


By

---

Latex:
((Assert  (T)sigma  =  H.\mBbbI{}  \mvdash{}  Glue  [(phi)sigma  \mvdash{}\mrightarrow{}  ((T)sigma;(equiv-fun(f))sigma)]  (A)sigma  BY
                ((Assert  (T)sigma  =  (Glue  [phi  \mvdash{}\mrightarrow{}  (T;equiv-fun(f))]  A)sigma  BY
                                (EqCDA
                                  THEN  Symmetry
                                  THEN  (InstLemma  `glue-type-constraint`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}equiv-fun(f)\mkleeneclose{}]\mcdot{}
                                              THENA  Auto
                                              )
                                  THEN  UnfoldTopAb  (-1)
                                  THEN  Trivial))
                  THEN  NthHypEqGen  (-1)
                  THEN  EqCDA
                  THEN  Auto))
  THEN  (Assert  \{H.\mBbbI{}  \mvdash{}  \_:Glue  [(phi)sigma  \mvdash{}\mrightarrow{}  ((T)sigma;(equiv-fun(f))sigma)]  (A)sigma\}
                          =  \{H.\mBbbI{}  \mvdash{}  \_:(T)sigma\}  BY
                          (EqCDA  THEN  Auto))
  )

---

Home Index