---

Step * 1 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.𝕀 ⊢ _}
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(𝕀)]}
BY
{ ((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 ((BLemma `subset-cubical-term` THEN Auto))
           THEN InferEqualTypeGen
           THEN Try (Trivial)
           THEN EqCDA
           THEN SubsumeC ⌜{H.𝕀 ⊢ _}⌝⋅
           THEN Auto))
   THEN (Assert (phi)sigma = 1(𝔽) ∈ {H.𝕀 ⊢ _:𝔽} BY
               ((Assert phi = 1(𝔽) ∈ {G, phi ⊢ _:𝔽} BY
                       (BLemma `face-1-in-context-subset` THENA Auto))
                THEN ApFunToHypEquands `Z' ⌜(Z)sigma⌝ ⌜{H.𝕀 ⊢ _:𝔽}⌝ (-1)⋅
                THEN Try ((RWO "csm-face-1" (-1) THEN Auto))
                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']}
18. b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}
19. (phi)sigma = 1(𝔽) ∈ {H.𝕀 ⊢ _:𝔽}
⊢ (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
16.  (T)sigma  =  H.\mBbbI{}  \mvdash{}  Glue  [(phi)sigma  \mvdash{}\mrightarrow{}  ((T)sigma;(equiv-fun(f))sigma)]  (A)sigma
17.  \{H.\mBbbI{}  \mvdash{}  \_:Glue  [(phi)sigma  \mvdash{}\mrightarrow{}  ((T)sigma;(equiv-fun(f))sigma)]  (A)sigma\}  =  \{H.\mBbbI{}  \mvdash{}  \_:(T)sigma\}
\mvdash{}  (cT  H  sigma  psi  b  b0)  =  (comp(Glue  [phi  \mvdash{}\mrightarrow{}  (T,  f)]  A)    H  sigma  psi  b  b0)


By

---

Latex:
((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  ((BLemma  `subset-cubical-term`  THEN  Auto))
                  THEN  InferEqualTypeGen
                  THEN  Try  (Trivial)
                  THEN  EqCDA
                  THEN  SubsumeC  \mkleeneopen{}\{H.\mBbbI{}  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
                  THEN  Auto))
  THEN  (Assert  (phi)sigma  =  1(\mBbbF{})  BY
                          ((Assert  phi  =  1(\mBbbF{})  BY
                                          (BLemma  `face-1-in-context-subset`  THENA  Auto))
                            THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}(Z)sigma\mkleeneclose{}  \mkleeneopen{}\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}\mkleeneclose{}  (-1)\mcdot{}
                            THEN  Try  ((RWO  "csm-face-1"  (-1)  THEN  Auto))
                            THEN  Auto))
  )

---

Home Index