---

Step * 1 of Lemma glue-comp_wf


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(𝕀)]]}
BY
{ ((Assert (phi)sigma ∈ {H.𝕀 ⊢ _:𝔽} BY
          Auto)
   THEN (Assert (equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T)sigma ⟶ (A)sigma)} BY
               ((Assert (equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T ⟶ A))sigma} BY
                       Auto)
                THEN InferEqualTypeGen
                THEN Try (Trivial)
                THEN EqCDA
                THEN (Assert ⌜sigma ∈ H.𝕀, (phi)sigma j⟶ G, phi⌝⋅ THENA Auto)
                THEN RWO "csm-cubical-fun<" 0
                THEN (Hypothesis ORELSE (Thin (-1) THEN Auto))))
   THEN (Assert {H.𝕀, (phi)sigma ⊢ _} ⊆r {H.𝕀, (psi)p, (phi)sigma ⊢ _} BY
               (Using [`B',⌜{H.𝕀, ((phi)sigma ∧ (psi)p) ⊢ _}⌝] (BLemma  `subtype_rel_transitivity`)⋅ 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}
16. (phi)sigma ∈ {H.𝕀 ⊢ _:𝔽}
17. (equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T)sigma ⟶ (A)sigma)}
18. {H.𝕀, (phi)sigma ⊢ _} ⊆r {H.𝕀, (psi)p, (phi)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:

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


By

---

Latex:
((Assert  (phi)sigma  \mmember{}  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}  BY
                Auto)
  THEN  (Assert  (equiv-fun(f))sigma  \mmember{}  \{H.\mBbbI{},  (phi)sigma  \mvdash{}  \_:((T)sigma  {}\mrightarrow{}  (A)sigma)\}  BY
                          ((Assert  (equiv-fun(f))sigma  \mmember{}  \{H.\mBbbI{},  (phi)sigma  \mvdash{}  \_:((T  {}\mrightarrow{}  A))sigma\}  BY
                                          Auto)
                            THEN  InferEqualTypeGen
                            THEN  Try  (Trivial)
                            THEN  EqCDA
                            THEN  (Assert  \mkleeneopen{}sigma  \mmember{}  H.\mBbbI{},  (phi)sigma  j{}\mrightarrow{}  G,  phi\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  RWO  "csm-cubical-fun<"  0
                            THEN  (Hypothesis  ORELSE  (Thin  (-1)  THEN  Auto))))
  THEN  (Assert  \{H.\mBbbI{},  (phi)sigma  \mvdash{}  \_\}  \msubseteq{}r  \{H.\mBbbI{},  (psi)p,  (phi)sigma  \mvdash{}  \_\}  BY
                          (Using  [`B',\mkleeneopen{}\{H.\mBbbI{},  ((phi)sigma  \mwedge{}  (psi)p)  \mvdash{}  \_\}\mkleeneclose{}]  (BLemma    `subtype\_rel\_transitivity`)\mcdot{}
                            THEN  Auto
                            )))

---

Home Index