Step
*
of Lemma
glue-comp_wf2
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) ∈ G ⊢ Compositon(Glue [psi ⊢→ (T;equiv-fun(f))] A))
BY
{ (InstLemma `glue-comp_wf` []
THEN RepeatFor 7 (ParallelLast')
THEN (MemTypeCD THENW Auto)
THEN Try (Trivial)
THEN (D 0 THENA Auto)
THEN Intros
THEN RenameVar `b' (-2)
THEN RenameVar `b0' (-1)
THEN ((MemTypeCD⋅ THENW (EqualityIsType1 THEN Auto))
THENL [Id
; ((GenConclTerm ⌜comp(Glue [psi ⊢→ (T, f)] A) H sigma phi b b0⌝⋅ THENA Auto)
THEN Thin (-1)
THEN D -1
THEN ApFunToHypEquands `Z' ⌜(Z)tau⌝ ⌜{K, (phi)tau ⊢ _:(((Glue [psi ⊢→ (T;equiv-fun(f))] A)sigma)
[1(𝕀)])tau}⌝ (-1)⋅
THEN Try (Eq)
THEN Fold `member` 0
THEN Auto)]
)
THEN RepUR ``glue-comp`` 0
THEN (Subst' unglue((b)tau+) ~ (unglue(b))tau+ 0 THENA ((RWO "csm-unglue" 0 THENA Auto) THEN CsmUnfolding THEN Auto))
THEN (Subst' unglue((b0)tau) ~ (unglue(b0))tau 0 THENA ((RWO "csm-unglue" 0 THENA Auto) THEN CsmUnfolding THEN Auto))
THEN SwapVars `phi' `psi'
THEN (Assert G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
∧ ((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _})
∧ (b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma})
∧ ((phi)sigma ∈ {H.𝕀 ⊢ _:𝔽})
∧ ((equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T)sigma ⟶ (A)sigma)})
∧ ({H.𝕀, (phi)sigma ⊢ _} ⊆r {H.𝕀, (psi)p, (phi)sigma ⊢ _})
∧ H, ((phi)sigma)[0(𝕀)] ⊢ ((T)sigma)[0(𝕀)]
∧ (((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]})
∧ (((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])})
∧ (sub_cubical_set{j:l}(H, (∀ (phi)sigma), psi.𝕀; H.𝕀, (psi)p, (phi)sigma)
∧ H, (∀ (phi)sigma).𝕀 ⊢ (T)sigma
∧ (H.𝕀, (phi)sigma +⊢ Compositon((T)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma))
∧ (H.𝕀, (phi)sigma +⊢ Compositon((A)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma))
∧ H.𝕀, (psi)p, (phi)sigma ⊢ (T)sigma
∧ H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
∧ ({H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _})
∧ H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)])
∧ (unglue(b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]})
∧ (unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]})
∧ ((cT)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma))
∧ ((cA)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)) BY
Auto)
THEN ExRepD
THEN (Assert b0 ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((T)sigma)[0(𝕀)]} BY
(DVar `b0' THEN DoSubsume THEN Auto))
THEN (Assert b ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(T)sigma} BY
(DoSubsume THEN Auto))
THEN (Assert app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(A)sigma} BY
Auto)
THEN (Assert H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
∧ ({H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _})
∧ H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)] BY
Auto)
THEN ExRepD) }
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. comp(Glue [phi ⊢→ (T, f)] A) ∈ composition-function{j:l,i:l}(G;Glue [phi ⊢→ (T;equiv-fun(f))] A)
9. H : CubicalSet{j}
10. K : CubicalSet{j}
11. tau : K j⟶ H
12. sigma : H.𝕀 j⟶ G
13. psi : {H ⊢ _:𝔽}
14. b : {H, psi.𝕀 ⊢ _:(Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma}
15. b0 : {H ⊢ _:((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[0(𝕀)][psi |⟶ (b)[0(𝕀)]]}
16. G ⊢ Glue [phi ⊢→ (T;equiv-fun(f))] A
17. (Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma
= H.𝕀 ⊢ Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma
∈ {H.𝕀 ⊢ _}
18. b ∈ {H.𝕀, (psi)p ⊢ _:Glue [(phi)sigma ⊢→ ((T)sigma;(equiv-fun(f))sigma)] (A)sigma}
19. (phi)sigma ∈ {H.𝕀 ⊢ _:𝔽}
20. (equiv-fun(f))sigma ∈ {H.𝕀, (phi)sigma ⊢ _:((T)sigma ⟶ (A)sigma)}
21. {H.𝕀, (phi)sigma ⊢ _} ⊆r {H.𝕀, (psi)p, (phi)sigma ⊢ _}
22. H, ((phi)sigma)[0(𝕀)] ⊢ ((T)sigma)[0(𝕀)]
23. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}
24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}
25. sub_cubical_set{j:l}(H, (∀ (phi)sigma), psi.𝕀; H.𝕀, (psi)p, (phi)sigma)
26. H, (∀ (phi)sigma).𝕀 ⊢ (T)sigma
27. H.𝕀, (phi)sigma +⊢ Compositon((T)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
28. H.𝕀, (phi)sigma +⊢ Compositon((A)sigma) ⊆r H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
29. H.𝕀, (psi)p, (phi)sigma ⊢ (T)sigma
30. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
31. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
32. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
33. unglue(b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma[(phi)sigma |⟶ app((equiv-fun(f))sigma; b)]}
34. unglue(b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)][((phi)sigma)[0(𝕀)] |⟶ app(((equiv-fun(f))sigma)[0(𝕀)]; b0)]}
35. (cT)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((T)sigma)
36. (cA)sigma ∈ H, (∀ (phi)sigma).𝕀 +⊢ Compositon((A)sigma)
37. b0 ∈ {H, ((phi)sigma)[0(𝕀)] ⊢ _:((T)sigma)[0(𝕀)]}
38. b ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(T)sigma}
39. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p, (phi)sigma ⊢ _:(A)sigma}
40. H, ((phi)sigma)[1(𝕀)] ⊢ ((T)sigma)[1(𝕀)]
41. {H, ((phi)sigma)[1(𝕀)] ⊢ _} ⊆r {H, (∀ (phi)sigma) ⊢ _}
42. H, (∀ (phi)sigma) ⊢ ((T)sigma)[1(𝕀)]
⊢ (let a = unglue(b) in
let a0 = unglue(b0) in
let a'1 = comp (cA)sigma [psi ⊢→ a] a0 in
let t'1 = comp (cT)sigma [psi ⊢→ b] b0 in
let w = pres (equiv-fun(f))sigma [psi ⊢→ b] b0 in
let st = (t'1 ∨ (b)[1(𝕀)]) in
let sw = (w ∨ <>((app((equiv-fun(f))sigma; b)[1])p)) in
let cF = fiber-comp(H, ((phi)sigma)[1(𝕀)];((T)sigma)[1(𝕀)];((A)sigma)[1(𝕀)];equiv-fun(((f)sigma)[1(𝕀)]);a'1;
(cT)sigma o [1(𝕀)];(cA)sigma o [1(𝕀)]) in
let z = equiv ((f)sigma)[1(𝕀)] [((∀ (phi)sigma) ∨ psi) ⊢→ (st, sw)] a'1 in
let t1 = fiber-member(z) in
let alpha = fiber-path(z) in
let a1 = comp (cA)sigma o [1(𝕀)] o p [(((phi)sigma)[1(𝕀)] ∨ psi) ⊢→ ((alpha)p @ q ∨ (a[1])p)] a'1 in
glue [((phi)sigma)[1(𝕀)] ⊢→ t1] a1)tau
= let a = (unglue(b))tau+ in
let a0 = (unglue(b0))tau in
let a'1 = comp (cA)sigma o tau+ [(psi)tau ⊢→ a] a0 in
let t'1 = comp (cT)sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau in
let w = pres (equiv-fun(f))sigma o tau+ [(psi)tau ⊢→ (b)tau+] (b0)tau in
let st = (t'1 ∨ ((b)tau+)[1(𝕀)]) in
let sw = (w ∨ <>((app((equiv-fun(f))sigma o tau+; (b)tau+)[1])p)) in
let cF = fiber-comp(K, ((phi)sigma o tau+)[1(𝕀)];((T)sigma o tau+)[1(𝕀)];((A)sigma o tau+)[1(𝕀)];
equiv-fun(((f)sigma o tau+)[1(𝕀)]);a'1;(cT)sigma o tau+ o [1(𝕀)];(cA)sigma o tau+ o [1(𝕀)]) in
let z = equiv ((f)sigma o tau+)[1(𝕀)] [((∀ (phi)sigma o tau+) ∨ (psi)tau) ⊢→ (st, sw)] a'1 in
let t1 = fiber-member(z) in
let alpha = fiber-path(z) in
let a1 = comp (cA)sigma o tau+ o [1(𝕀)] o p [(((phi)sigma o tau+)[1(𝕀)] ∨ (psi)tau) ⊢→ ((alpha)p @ q ∨ (a[1])p)]
a'1 in
glue [((phi)sigma o tau+)[1(𝕀)] ⊢→ t1] a1
∈ {K ⊢ _:(((Glue [phi ⊢→ (T;equiv-fun(f))] A)sigma)[1(𝕀)])tau}
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{} G \mvdash{} Compositon(Glue [psi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A))
By
Latex:
(InstLemma `glue-comp\_wf` []
THEN RepeatFor 7 (ParallelLast')
THEN (MemTypeCD THENW Auto)
THEN Try (Trivial)
THEN (D 0 THENA Auto)
THEN Intros
THEN RenameVar `b' (-2)
THEN RenameVar `b0' (-1)
THEN ((MemTypeCD\mcdot{} THENW (EqualityIsType1 THEN Auto))
THENL [Id
; ((GenConclTerm \mkleeneopen{}comp(Glue [psi \mvdash{}\mrightarrow{} (T, f)] A) H sigma phi b b0\mkleeneclose{}\mcdot{} THENA Auto)
THEN Thin (-1)
THEN D -1
THEN ApFunToHypEquands `Z' \mkleeneopen{}(Z)tau\mkleeneclose{}
\mkleeneopen{}\{K, (phi)tau \mvdash{} \_:(((Glue [psi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A)sigma)[1(\mBbbI{})])tau\}\mkleeneclose{} (-1)\mcdot{}
THEN Try (Eq)
THEN Fold `member` 0
THEN Auto)]
)
THEN RepUR ``glue-comp`` 0
THEN (Subst' unglue((b)tau+) \msim{} (unglue(b))tau+ 0
THENA ((RWO "csm-unglue" 0 THENA Auto) THEN CsmUnfolding THEN Auto)
)
THEN (Subst' unglue((b0)tau) \msim{} (unglue(b0))tau 0
THENA ((RWO "csm-unglue" 0 THENA Auto) THEN CsmUnfolding THEN Auto)
)
THEN SwapVars `phi' `psi'
THEN (Assert G \mvdash{} Glue [phi \mvdash{}\mrightarrow{} (T;equiv-fun(f))] A
\mwedge{} ((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)
\mwedge{} (b \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma\})
\mwedge{} ((phi)sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:\mBbbF{}\})
\mwedge{} ((equiv-fun(f))sigma \mmember{} \{H.\mBbbI{}, (phi)sigma \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\})
\mwedge{} (\{H.\mBbbI{}, (phi)sigma \mvdash{} \_\} \msubseteq{}r \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_\})
\mwedge{} H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} ((T)sigma)[0(\mBbbI{})]
\mwedge{} (((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T {}\mrightarrow{} A))sigma)[0(\mBbbI{})]\})
\mwedge{} (((equiv-fun(f))sigma)[0(\mBbbI{})]
\mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:(((T)sigma)[0(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[0(\mBbbI{})])\})
\mwedge{} (sub\_cubical\_set\{j:l\}(H, (\mforall{} (phi)sigma), psi.\mBbbI{}; H.\mBbbI{}, (psi)p, (phi)sigma)
\mwedge{} H, (\mforall{} (phi)sigma).\mBbbI{} \mvdash{} (T)sigma
\mwedge{} (H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((T)sigma)
\msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma))
\mwedge{} (H.\mBbbI{}, (phi)sigma +\mvdash{} Compositon((A)sigma)
\msubseteq{}r H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma))
\mwedge{} H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} (T)sigma
\mwedge{} H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})]
\mwedge{} (\{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\})
\mwedge{} H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})])
\mwedge{} (unglue(b) \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma[(phi)sigma |{}\mrightarrow{} app((equiv-fun(f))sigma; b)]\})
\mwedge{} (unglue(b0) \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][((phi)sigma)[0(\mBbbI{})]
|{}\mrightarrow{} app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)]\})
\mwedge{} ((cT)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((T)sigma))
\mwedge{} ((cA)sigma \mmember{} H, (\mforall{} (phi)sigma).\mBbbI{} +\mvdash{} Compositon((A)sigma)) BY
Auto)
THEN ExRepD
THEN (Assert b0 \mmember{} \{H, ((phi)sigma)[0(\mBbbI{})] \mvdash{} \_:((T)sigma)[0(\mBbbI{})]\} BY
(DVar `b0' THEN DoSubsume THEN Auto))
THEN (Assert b \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(T)sigma\} BY
(DoSubsume THEN Auto))
THEN (Assert app((equiv-fun(f))sigma; b) \mmember{} \{H.\mBbbI{}, (psi)p, (phi)sigma \mvdash{} \_:(A)sigma\} BY
Auto)
THEN (Assert H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} ((T)sigma)[1(\mBbbI{})]
\mwedge{} (\{H, ((phi)sigma)[1(\mBbbI{})] \mvdash{} \_\} \msubseteq{}r \{H, (\mforall{} (phi)sigma) \mvdash{} \_\})
\mwedge{} H, (\mforall{} (phi)sigma) \mvdash{} ((T)sigma)[1(\mBbbI{})] BY
Auto)
THEN ExRepD)
Home
Index