Step
*
1
1
1
2
2
2
2
2
2
of Lemma
case-type-comp_wf
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ composition-function{j:l,i:l}(Gamma, (phi ∨ psi);(if phi then A else B))
12. H : CubicalSet{j}
13. K : CubicalSet{j}
14. I : fset(ℕ)
15. alpha : K(I)
16. tau : K j⟶ H
17. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
18. chi : {H ⊢ _:𝔽}
19. u : {H, chi.𝕀 ⊢ _:(if (phi)sigma then (A)sigma else (B)sigma)}
20. a0 : {H ⊢ _:(if ((phi)sigma)[0(𝕀)] then ((A)sigma)[0(𝕀)] else ((B)sigma)[0(𝕀)])[chi |⟶ (u)[0(𝕀)]]}
21. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
22. H.𝕀 ⊢ (if (phi)sigma then (A)sigma else (B)sigma)
23. H.𝕀 ⊢ (1(𝔽) ⇒ ((phi)sigma ∨ (psi)sigma))
24. (∀ (phi)sigma) ∈ {H ⊢ _:𝔽}
25. (∀ (psi)sigma) ∈ {H ⊢ _:𝔽}
26. H.𝕀, ((phi)sigma ∧ (psi)sigma) ⊢ (A)sigma = (B)sigma
27. {u ∈ {H, (∀ (phi)sigma), chi.𝕀 ⊢ _:(A)sigma}}
28. {a0 ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}}
29. (cA H, (∀ (phi)sigma) sigma chi u a0)tau
= (cA K, (∀ (phi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau)
∈ {K, (∀ (phi)sigma o tau+) ⊢ _:(((A)sigma)[1(𝕀)])tau[(chi)tau |⟶ ((u)[1(𝕀)])tau]}
30. u ∈ {H, (∀ (psi)sigma), chi.𝕀 ⊢ _:(B)sigma}
31. a0 ∈ {H, (∀ (psi)sigma) ⊢ _:((B)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
32. (cB H, (∀ (psi)sigma) sigma chi u a0)tau
= (cB K, (∀ (psi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau)
∈ {K, (∀ (psi)sigma o tau+) ⊢ _:(((B)sigma)[1(𝕀)])tau[(chi)tau |⟶ ((u)[1(𝕀)])tau]}
⊢ (((cA H, (∀ (phi)sigma) sigma chi u a0)tau ∨ (cB H, (∀ (psi)sigma) sigma chi u a0)tau) I alpha)
= ((cA K, (∀ (phi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau ∨ cB K, (∀ (psi)sigma o tau+) sigma o tau+
(chi)tau
(u)tau+
(a0)tau)
I
alpha)
∈ (if (((phi)sigma)[1(𝕀)])tau then (((A)sigma)[1(𝕀)])tau else (((B)sigma)[1(𝕀)])tau)(alpha)
BY
{ ((Assert H, (∀ (phi)sigma) ⊢ ((A)sigma)[1(𝕀)] BY
(InstLemma `face-forall-map` [⌜Gamma⌝;⌜H⌝;⌜phi⌝;⌜sigma⌝]⋅ THEN Auto))
THEN (Assert H, (∀ (psi)sigma) ⊢ ((B)sigma)[1(𝕀)] BY
(InstLemma `face-forall-map` [⌜Gamma⌝;⌜H⌝;⌜psi⌝;⌜sigma⌝]⋅ THEN Auto))
THEN (Assert K, ((∀ (phi)sigma))tau ⊢ (((A)sigma)[1(𝕀)])tau BY
Auto)
THEN (Assert K, ((∀ (psi)sigma))tau ⊢ (((B)sigma)[1(𝕀)])tau BY
Auto)) }
1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ composition-function{j:l,i:l}(Gamma, (phi ∨ psi);(if phi then A else B))
12. H : CubicalSet{j}
13. K : CubicalSet{j}
14. I : fset(ℕ)
15. alpha : K(I)
16. tau : K j⟶ H
17. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
18. chi : {H ⊢ _:𝔽}
19. u : {H, chi.𝕀 ⊢ _:(if (phi)sigma then (A)sigma else (B)sigma)}
20. a0 : {H ⊢ _:(if ((phi)sigma)[0(𝕀)] then ((A)sigma)[0(𝕀)] else ((B)sigma)[0(𝕀)])[chi |⟶ (u)[0(𝕀)]]}
21. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
22. H.𝕀 ⊢ (if (phi)sigma then (A)sigma else (B)sigma)
23. H.𝕀 ⊢ (1(𝔽) ⇒ ((phi)sigma ∨ (psi)sigma))
24. (∀ (phi)sigma) ∈ {H ⊢ _:𝔽}
25. (∀ (psi)sigma) ∈ {H ⊢ _:𝔽}
26. H.𝕀, ((phi)sigma ∧ (psi)sigma) ⊢ (A)sigma = (B)sigma
27. {u ∈ {H, (∀ (phi)sigma), chi.𝕀 ⊢ _:(A)sigma}}
28. {a0 ∈ {H, (∀ (phi)sigma) ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}}
29. (cA H, (∀ (phi)sigma) sigma chi u a0)tau
= (cA K, (∀ (phi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau)
∈ {K, (∀ (phi)sigma o tau+) ⊢ _:(((A)sigma)[1(𝕀)])tau[(chi)tau |⟶ ((u)[1(𝕀)])tau]}
30. u ∈ {H, (∀ (psi)sigma), chi.𝕀 ⊢ _:(B)sigma}
31. a0 ∈ {H, (∀ (psi)sigma) ⊢ _:((B)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
32. (cB H, (∀ (psi)sigma) sigma chi u a0)tau
= (cB K, (∀ (psi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau)
∈ {K, (∀ (psi)sigma o tau+) ⊢ _:(((B)sigma)[1(𝕀)])tau[(chi)tau |⟶ ((u)[1(𝕀)])tau]}
33. H, (∀ (phi)sigma) ⊢ ((A)sigma)[1(𝕀)]
34. H, (∀ (psi)sigma) ⊢ ((B)sigma)[1(𝕀)]
35. K, ((∀ (phi)sigma))tau ⊢ (((A)sigma)[1(𝕀)])tau
36. K, ((∀ (psi)sigma))tau ⊢ (((B)sigma)[1(𝕀)])tau
⊢ (((cA H, (∀ (phi)sigma) sigma chi u a0)tau ∨ (cB H, (∀ (psi)sigma) sigma chi u a0)tau) I alpha)
= ((cA K, (∀ (phi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau ∨ cB K, (∀ (psi)sigma o tau+) sigma o tau+
(chi)tau
(u)tau+
(a0)tau)
I
alpha)
∈ (if (((phi)sigma)[1(𝕀)])tau then (((A)sigma)[1(𝕀)])tau else (((B)sigma)[1(𝕀)])tau)(alpha)
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. phi : \{Gamma \mvdash{} \_:\mBbbF{}\}
3. psi : \{Gamma \mvdash{} \_:\mBbbF{}\}
4. A : \{Gamma, phi \mvdash{} \_\}
5. B : \{Gamma, psi \mvdash{} \_\}
6. cA : Gamma, phi \mvdash{} Compositon(A)
7. cB : Gamma, psi \mvdash{} Compositon(B)
8. Gamma, (phi \mwedge{} psi) \mvdash{} A = B
9. compatible-composition\{j:l, i:l\}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi \mvee{} psi) \mvdash{} (if phi then A else B)
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
\mmember{} composition-function\{j:l,i:l\}(Gamma, (phi \mvee{} psi);(if phi then A else B))
12. H : CubicalSet\{j\}
13. K : CubicalSet\{j\}
14. I : fset(\mBbbN{})
15. alpha : K(I)
16. tau : K j{}\mrightarrow{} H
17. sigma : H.\mBbbI{} j{}\mrightarrow{} Gamma, (phi \mvee{} psi)
18. chi : \{H \mvdash{} \_:\mBbbF{}\}
19. u : \{H, chi.\mBbbI{} \mvdash{} \_:(if (phi)sigma then (A)sigma else (B)sigma)\}
20. a0 : \{H \mvdash{} \_:(if ((phi)sigma)[0(\mBbbI{})] then ((A)sigma)[0(\mBbbI{})] else ((B)sigma)[0(\mBbbI{})])[chi
|{}\mrightarrow{} (u)[0(\mBbbI{})]]\}
21. Gamma, (phi \mvee{} psi) \mvdash{} (if phi then A else B)
22. H.\mBbbI{} \mvdash{} (if (phi)sigma then (A)sigma else (B)sigma)
23. H.\mBbbI{} \mvdash{} (1(\mBbbF{}) {}\mRightarrow{} ((phi)sigma \mvee{} (psi)sigma))
24. (\mforall{} (phi)sigma) \mmember{} \{H \mvdash{} \_:\mBbbF{}\}
25. (\mforall{} (psi)sigma) \mmember{} \{H \mvdash{} \_:\mBbbF{}\}
26. H.\mBbbI{}, ((phi)sigma \mwedge{} (psi)sigma) \mvdash{} (A)sigma = (B)sigma
27. \{u \mmember{} \{H, (\mforall{} (phi)sigma), chi.\mBbbI{} \mvdash{} \_:(A)sigma\}\}
28. \{a0 \mmember{} \{H, (\mforall{} (phi)sigma) \mvdash{} \_:((A)sigma)[0(\mBbbI{})][chi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}\}
29. (cA H, (\mforall{} (phi)sigma) sigma chi u a0)tau
= (cA K, (\mforall{} (phi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau)
30. u \mmember{} \{H, (\mforall{} (psi)sigma), chi.\mBbbI{} \mvdash{} \_:(B)sigma\}
31. a0 \mmember{} \{H, (\mforall{} (psi)sigma) \mvdash{} \_:((B)sigma)[0(\mBbbI{})][chi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}
32. (cB H, (\mforall{} (psi)sigma) sigma chi u a0)tau
= (cB K, (\mforall{} (psi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau)
\mvdash{} (((cA H, (\mforall{} (phi)sigma) sigma chi u a0)tau \mvee{} (cB H, (\mforall{} (psi)sigma) sigma chi u a0)tau) I alpha)
= ((cA K, (\mforall{} (phi)sigma o tau+) sigma o tau+ (chi)tau (u)tau+ (a0)tau \mvee{} cB K, (\mforall{} (psi)sigma o tau+)
sigma o tau+
(chi)tau
(u)tau+
(a0)tau)
I
alpha)
By
Latex:
((Assert H, (\mforall{} (phi)sigma) \mvdash{} ((A)sigma)[1(\mBbbI{})] BY
(InstLemma `face-forall-map` [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}sigma\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert H, (\mforall{} (psi)sigma) \mvdash{} ((B)sigma)[1(\mBbbI{})] BY
(InstLemma `face-forall-map` [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}sigma\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert K, ((\mforall{} (phi)sigma))tau \mvdash{} (((A)sigma)[1(\mBbbI{})])tau BY
Auto)
THEN (Assert K, ((\mforall{} (psi)sigma))tau \mvdash{} (((B)sigma)[1(\mBbbI{})])tau BY
Auto))
Home
Index