Step
*
1
1
1
1
1
2
2
2
1
1
2
1
of Lemma
glue-comp-agrees
.....assertion.....
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.𝕀 ⊢ _:𝔽}
20. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T ⟶ A))sigma}
21. (equiv-fun(f))sigma ∈ {H.𝕀 ⊢ _:((T)sigma ⟶ (A)sigma)}
22. H ⊢ ((T)sigma)[0(𝕀)]
23. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T ⟶ A))sigma)[0(𝕀)]}
24. ((equiv-fun(f))sigma)[0(𝕀)] ∈ {H ⊢ _:(((T)sigma)[0(𝕀)] ⟶ ((A)sigma)[0(𝕀)])}
25. ((phi)sigma)[0(𝕀)] = 1(𝔽) ∈ {H ⊢ _:𝔽}
26. app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
27. a : {H.𝕀, (psi)p ⊢ _:(A)sigma}
28. unglue(b) = a ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
29. a = app((equiv-fun(f))sigma; b) ∈ {H.𝕀, (psi)p ⊢ _:(A)sigma}
30. a0 : {H ⊢ _:((A)sigma)[0(𝕀)]}
31. unglue(b0) = a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
32. a0 = app(((equiv-fun(f))sigma)[0(𝕀)]; b0) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
33. a0 ∈ {H ⊢ _:((A)sigma)[0(𝕀)][psi |⟶ a[0]]}
⊢ comp (cA)sigma [psi ⊢→ a] a0 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][psi |⟶ a[1]]}
BY
{ ((InstLemma `comp_term_wf` [⌜H⌝;⌜psi⌝;⌜(A)sigma⌝;⌜(cA)sigma⌝]⋅ THENA Auto)
THEN (InstHyp [⌜a⌝;⌜a0⌝] (-1)⋅ THENM (Fold `partial-term-1` (-1) THEN Trivial))
THEN Try ((NthHypSq (-2) THEN Fold `partial-term-0` 0 THEN Trivial))
THEN DoSubsume
THEN Auto) }
Latex:
Latex:
.....assertion.....
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\}
18. \{b \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:Glue [(phi)sigma \mvdash{}\mrightarrow{} ((T)sigma;(equiv-fun(f))sigma)] (A)sigma\}\}
19. (phi)sigma = 1(\mBbbF{})
20. (equiv-fun(f))sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:((T {}\mrightarrow{} A))sigma\}
21. (equiv-fun(f))sigma \mmember{} \{H.\mBbbI{} \mvdash{} \_:((T)sigma {}\mrightarrow{} (A)sigma)\}
22. H \mvdash{} ((T)sigma)[0(\mBbbI{})]
23. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H \mvdash{} \_:(((T {}\mrightarrow{} A))sigma)[0(\mBbbI{})]\}
24. ((equiv-fun(f))sigma)[0(\mBbbI{})] \mmember{} \{H \mvdash{} \_:(((T)sigma)[0(\mBbbI{})] {}\mrightarrow{} ((A)sigma)[0(\mBbbI{})])\}
25. ((phi)sigma)[0(\mBbbI{})] = 1(\mBbbF{})
26. app((equiv-fun(f))sigma; b) \mmember{} \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma\}
27. a : \{H.\mBbbI{}, (psi)p \mvdash{} \_:(A)sigma\}
28. unglue(b) = a
29. a = app((equiv-fun(f))sigma; b)
30. a0 : \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})]\}
31. unglue(b0) = a0
32. a0 = app(((equiv-fun(f))sigma)[0(\mBbbI{})]; b0)
33. a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][psi |{}\mrightarrow{} a[0]]\}
\mvdash{} comp (cA)sigma [psi \mvdash{}\mrightarrow{} a] a0 \mmember{} \{H \mvdash{} \_:((A)sigma)[1(\mBbbI{})][psi |{}\mrightarrow{} a[1]]\}
By
Latex:
((InstLemma `comp\_term\_wf` [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}(A)sigma\mkleeneclose{};\mkleeneopen{}(cA)sigma\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstHyp [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a0\mkleeneclose{}] (-1)\mcdot{} THENM (Fold `partial-term-1` (-1) THEN Trivial))
THEN Try ((NthHypSq (-2) THEN Fold `partial-term-0` 0 THEN Trivial))
THEN DoSubsume
THEN Auto)
Home
Index