Step
*
1
1
1
2
2
2
1
2
3
2
1
1
1
2
1
1
2
1
of Lemma
comp-to-fill_wf2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. H : CubicalSet{j}
5. K : CubicalSet{j}
6. tau : K j⟶ H
7. sigma : H.𝕀 j⟶ Gamma
8. phi : {H ⊢ _:𝔽}
9. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
10. ((phi)p ∨ (q=0)) ∈ {H.𝕀 ⊢ _:𝔽}
11. (((phi)p ∨ (q=0)))tau+ ∈ {K.𝕀 ⊢ _:𝔽}
12. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
13. ∀u:{H.𝕀, ((phi)p ∨ (q=0)).𝕀 ⊢ _:(A)sigma o m}. ∀a0:{H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (u)[0(𝕀)]]}.
((cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) u a0)tau+
= (cA K.𝕀 sigma o m o tau++ (((phi)p ∨ (q=0)))tau+ (u)tau++ (a0)tau+)
∈ {K.𝕀 ⊢ _:(((A)sigma o m)[1(𝕀)])tau+[(((phi)p ∨ (q=0)))tau+ |⟶ ((u)[1(𝕀)])tau+]})
14. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
15. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
16. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:((A)sigma)m}
17. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
18. (u)m = ((a0)p)m ∈ {H.𝕀.𝕀, (((phi)p)m ∧ ((q=0))p) ⊢ _:((A)sigma)m}
19. ((u)m ∨ ((a0)p)m) ∈ {H.𝕀.𝕀, (((phi)p)m ∨ ((q=0))p) ⊢ _:(A)sigma o m}
20. (a0)p ∈ {H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (((u)m ∨ ((a0)p)m))[0(𝕀)]]}
21. ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ∈ {K.𝕀.𝕀 ⊢ _:𝔽}
⊢ (((u)m)tau++ ∨ (((a0)p)m)tau++)
= (((u)tau+)m ∨ (((a0)tau)p)m)
∈ {K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ⊢ _:(((A)sigma)m)tau++}
BY
{ CubicalTermEqual }
1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. H : CubicalSet{j}
5. K : CubicalSet{j}
6. tau : K j⟶ H
7. sigma : H.𝕀 j⟶ Gamma
8. phi : {H ⊢ _:𝔽}
9. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
10. ((phi)p ∨ (q=0)) ∈ {H.𝕀 ⊢ _:𝔽}
11. (((phi)p ∨ (q=0)))tau+ ∈ {K.𝕀 ⊢ _:𝔽}
12. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
13. ∀u:{H.𝕀, ((phi)p ∨ (q=0)).𝕀 ⊢ _:(A)sigma o m}. ∀a0:{H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (u)[0(𝕀)]]}.
((cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) u a0)tau+
= (cA K.𝕀 sigma o m o tau++ (((phi)p ∨ (q=0)))tau+ (u)tau++ (a0)tau+)
∈ {K.𝕀 ⊢ _:(((A)sigma o m)[1(𝕀)])tau+[(((phi)p ∨ (q=0)))tau+ |⟶ ((u)[1(𝕀)])tau+]})
14. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
15. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
16. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:((A)sigma)m}
17. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
18. (u)m = ((a0)p)m ∈ {H.𝕀.𝕀, (((phi)p)m ∧ ((q=0))p) ⊢ _:((A)sigma)m}
19. ((u)m ∨ ((a0)p)m) ∈ {H.𝕀.𝕀, (((phi)p)m ∨ ((q=0))p) ⊢ _:(A)sigma o m}
20. (a0)p ∈ {H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (((u)m ∨ ((a0)p)m))[0(𝕀)]]}
21. ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ∈ {K.𝕀.𝕀 ⊢ _:𝔽}
22. I : fset(ℕ)
23. a : K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++)(I)
⊢ ((((u)m)tau++ ∨ (((a0)p)m)tau++) I a) = ((((u)tau+)m ∨ (((a0)tau)p)m) I a) ∈ (((A)sigma)m)tau++(a)
2
.....wf.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. H : CubicalSet{j}
5. K : CubicalSet{j}
6. tau : K j⟶ H
7. sigma : H.𝕀 j⟶ Gamma
8. phi : {H ⊢ _:𝔽}
9. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
10. ((phi)p ∨ (q=0)) ∈ {H.𝕀 ⊢ _:𝔽}
11. (((phi)p ∨ (q=0)))tau+ ∈ {K.𝕀 ⊢ _:𝔽}
12. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
13. ∀u:{H.𝕀, ((phi)p ∨ (q=0)).𝕀 ⊢ _:(A)sigma o m}. ∀a0:{H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (u)[0(𝕀)]]}.
((cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) u a0)tau+
= (cA K.𝕀 sigma o m o tau++ (((phi)p ∨ (q=0)))tau+ (u)tau++ (a0)tau+)
∈ {K.𝕀 ⊢ _:(((A)sigma o m)[1(𝕀)])tau+[(((phi)p ∨ (q=0)))tau+ |⟶ ((u)[1(𝕀)])tau+]})
14. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
15. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
16. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:((A)sigma)m}
17. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
18. (u)m = ((a0)p)m ∈ {H.𝕀.𝕀, (((phi)p)m ∧ ((q=0))p) ⊢ _:((A)sigma)m}
19. ((u)m ∨ ((a0)p)m) ∈ {H.𝕀.𝕀, (((phi)p)m ∨ ((q=0))p) ⊢ _:(A)sigma o m}
20. (a0)p ∈ {H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (((u)m ∨ ((a0)p)m))[0(𝕀)]]}
21. ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ∈ {K.𝕀.𝕀 ⊢ _:𝔽}
22. I : fset(ℕ)
⊢ K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++)(I) ∈ 𝕌{j'}
3
.....wf.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. H : CubicalSet{j}
5. K : CubicalSet{j}
6. tau : K j⟶ H
7. sigma : H.𝕀 j⟶ Gamma
8. phi : {H ⊢ _:𝔽}
9. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
10. ((phi)p ∨ (q=0)) ∈ {H.𝕀 ⊢ _:𝔽}
11. (((phi)p ∨ (q=0)))tau+ ∈ {K.𝕀 ⊢ _:𝔽}
12. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
13. ∀u:{H.𝕀, ((phi)p ∨ (q=0)).𝕀 ⊢ _:(A)sigma o m}. ∀a0:{H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (u)[0(𝕀)]]}.
((cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) u a0)tau+
= (cA K.𝕀 sigma o m o tau++ (((phi)p ∨ (q=0)))tau+ (u)tau++ (a0)tau+)
∈ {K.𝕀 ⊢ _:(((A)sigma o m)[1(𝕀)])tau+[(((phi)p ∨ (q=0)))tau+ |⟶ ((u)[1(𝕀)])tau+]})
14. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
15. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
16. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:((A)sigma)m}
17. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
18. (u)m = ((a0)p)m ∈ {H.𝕀.𝕀, (((phi)p)m ∧ ((q=0))p) ⊢ _:((A)sigma)m}
19. ((u)m ∨ ((a0)p)m) ∈ {H.𝕀.𝕀, (((phi)p)m ∨ ((q=0))p) ⊢ _:(A)sigma o m}
20. (a0)p ∈ {H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (((u)m ∨ ((a0)p)m))[0(𝕀)]]}
21. ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ∈ {K.𝕀.𝕀 ⊢ _:𝔽}
⊢ fset(ℕ) ∈ Type
4
.....aux.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. H : CubicalSet{j}
5. K : CubicalSet{j}
6. tau : K j⟶ H
7. sigma : H.𝕀 j⟶ Gamma
8. phi : {H ⊢ _:𝔽}
9. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
10. ((phi)p ∨ (q=0)) ∈ {H.𝕀 ⊢ _:𝔽}
11. (((phi)p ∨ (q=0)))tau+ ∈ {K.𝕀 ⊢ _:𝔽}
12. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
13. ∀u:{H.𝕀, ((phi)p ∨ (q=0)).𝕀 ⊢ _:(A)sigma o m}. ∀a0:{H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (u)[0(𝕀)]]}.
((cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) u a0)tau+
= (cA K.𝕀 sigma o m o tau++ (((phi)p ∨ (q=0)))tau+ (u)tau++ (a0)tau+)
∈ {K.𝕀 ⊢ _:(((A)sigma o m)[1(𝕀)])tau+[(((phi)p ∨ (q=0)))tau+ |⟶ ((u)[1(𝕀)])tau+]})
14. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
15. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
16. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:((A)sigma)m}
17. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
18. (u)m = ((a0)p)m ∈ {H.𝕀.𝕀, (((phi)p)m ∧ ((q=0))p) ⊢ _:((A)sigma)m}
19. ((u)m ∨ ((a0)p)m) ∈ {H.𝕀.𝕀, (((phi)p)m ∨ ((q=0))p) ⊢ _:(A)sigma o m}
20. (a0)p ∈ {H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (((u)m ∨ ((a0)p)m))[0(𝕀)]]}
21. ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ∈ {K.𝕀.𝕀 ⊢ _:𝔽}
22. (((u)m)tau++ ∨ (((a0)p)m)tau++)
= (((u)tau+)m ∨ (((a0)tau)p)m)
∈ (I:fset(ℕ) ⟶ a:K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++)(I) ⟶ (((A)sigma)m)tau++(a))
23. ∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
⊢ K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) j⊢
5
.....aux.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. H : CubicalSet{j}
5. K : CubicalSet{j}
6. tau : K j⟶ H
7. sigma : H.𝕀 j⟶ Gamma
8. phi : {H ⊢ _:𝔽}
9. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
10. ((phi)p ∨ (q=0)) ∈ {H.𝕀 ⊢ _:𝔽}
11. (((phi)p ∨ (q=0)))tau+ ∈ {K.𝕀 ⊢ _:𝔽}
12. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
13. ∀u:{H.𝕀, ((phi)p ∨ (q=0)).𝕀 ⊢ _:(A)sigma o m}. ∀a0:{H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (u)[0(𝕀)]]}.
((cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) u a0)tau+
= (cA K.𝕀 sigma o m o tau++ (((phi)p ∨ (q=0)))tau+ (u)tau++ (a0)tau+)
∈ {K.𝕀 ⊢ _:(((A)sigma o m)[1(𝕀)])tau+[(((phi)p ∨ (q=0)))tau+ |⟶ ((u)[1(𝕀)])tau+]})
14. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
15. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
16. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:((A)sigma)m}
17. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
18. (u)m = ((a0)p)m ∈ {H.𝕀.𝕀, (((phi)p)m ∧ ((q=0))p) ⊢ _:((A)sigma)m}
19. ((u)m ∨ ((a0)p)m) ∈ {H.𝕀.𝕀, (((phi)p)m ∨ ((q=0))p) ⊢ _:(A)sigma o m}
20. (a0)p ∈ {H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (((u)m ∨ ((a0)p)m))[0(𝕀)]]}
21. ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ∈ {K.𝕀.𝕀 ⊢ _:𝔽}
22. (((u)m)tau++ ∨ (((a0)p)m)tau++)
= (((u)tau+)m ∨ (((a0)tau)p)m)
∈ (I:fset(ℕ) ⟶ a:K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++)(I) ⟶ (((A)sigma)m)tau++(a))
23. ∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
⊢ K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ⊢ (((A)sigma)m)tau++
6
.....aux.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. H : CubicalSet{j}
5. K : CubicalSet{j}
6. tau : K j⟶ H
7. sigma : H.𝕀 j⟶ Gamma
8. phi : {H ⊢ _:𝔽}
9. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
10. ((phi)p ∨ (q=0)) ∈ {H.𝕀 ⊢ _:𝔽}
11. (((phi)p ∨ (q=0)))tau+ ∈ {K.𝕀 ⊢ _:𝔽}
12. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
13. ∀u:{H.𝕀, ((phi)p ∨ (q=0)).𝕀 ⊢ _:(A)sigma o m}. ∀a0:{H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (u)[0(𝕀)]]}.
((cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) u a0)tau+
= (cA K.𝕀 sigma o m o tau++ (((phi)p ∨ (q=0)))tau+ (u)tau++ (a0)tau+)
∈ {K.𝕀 ⊢ _:(((A)sigma o m)[1(𝕀)])tau+[(((phi)p ∨ (q=0)))tau+ |⟶ ((u)[1(𝕀)])tau+]})
14. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
15. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
16. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:((A)sigma)m}
17. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
18. (u)m = ((a0)p)m ∈ {H.𝕀.𝕀, (((phi)p)m ∧ ((q=0))p) ⊢ _:((A)sigma)m}
19. ((u)m ∨ ((a0)p)m) ∈ {H.𝕀.𝕀, (((phi)p)m ∨ ((q=0))p) ⊢ _:(A)sigma o m}
20. (a0)p ∈ {H.𝕀 ⊢ _:((A)sigma o m)[0(𝕀)][((phi)p ∨ (q=0)) |⟶ (((u)m ∨ ((a0)p)m))[0(𝕀)]]}
21. ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ∈ {K.𝕀.𝕀 ⊢ _:𝔽}
22. (((u)m)tau++ ∨ (((a0)p)m)tau++)
= (((u)tau+)m ∨ (((a0)tau)p)m)
∈ (I:fset(ℕ) ⟶ a:K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++)(I) ⟶ (((A)sigma)m)tau++(a))
23. ∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:fset(ℕ) ⟶ a:X(I) ⟶ A(a)].
u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:fset(ℕ) ⟶ a:X(I) ⟶ A(a))
⊢ (((u)m)tau++ ∨ (((a0)p)m)tau++) ∈ {K.𝕀.𝕀, ((((phi)p)m)tau++ ∨ (((q=0))p)tau++) ⊢ _:(((A)sigma)m)tau++}
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. cA : composition-function\{j:l,i:l\}(Gamma;A)
4. H : CubicalSet\{j\}
5. K : CubicalSet\{j\}
6. tau : K j{}\mrightarrow{} H
7. sigma : H.\mBbbI{} j{}\mrightarrow{} Gamma
8. phi : \{H \mvdash{} \_:\mBbbF{}\}
9. u : \{H.\mBbbI{}, (phi)p \mvdash{} \_:(A)sigma\}
10. ((phi)p \mvee{} (q=0)) \mmember{} \{H.\mBbbI{} \mvdash{} \_:\mBbbF{}\}
11. (((phi)p \mvee{} (q=0)))tau+ \mmember{} \{K.\mBbbI{} \mvdash{} \_:\mBbbF{}\}
12. a0 : \{H \mvdash{} \_:((A)sigma)[0(\mBbbI{})][phi |{}\mrightarrow{} u[0]]\}
13. \mforall{}u:\{H.\mBbbI{}, ((phi)p \mvee{} (q=0)).\mBbbI{} \mvdash{} \_:(A)sigma o m\}.
\mforall{}a0:\{H.\mBbbI{} \mvdash{} \_:((A)sigma o m)[0(\mBbbI{})][((phi)p \mvee{} (q=0)) |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}.
((cA H.\mBbbI{} sigma o m ((phi)p \mvee{} (q=0)) u a0)tau+
= (cA K.\mBbbI{} sigma o m o tau++ (((phi)p \mvee{} (q=0)))tau+ (u)tau++ (a0)tau+))
14. ((phi)p)m \mmember{} \{H.\mBbbI{}.\mBbbI{} \mvdash{} \_:\mBbbF{}\}
15. (u)m \mmember{} \{H.\mBbbI{}.\mBbbI{}, ((phi)p)m \mvdash{} \_:((A)sigma)m\}
16. ((a0)p)m \mmember{} \{H.\mBbbI{}.\mBbbI{}, ((q=0))p \mvdash{} \_:((A)sigma)m\}
17. ((A)sigma o m)[1(\mBbbI{})] = (A)sigma
18. (u)m = ((a0)p)m
19. ((u)m \mvee{} ((a0)p)m) \mmember{} \{H.\mBbbI{}.\mBbbI{}, (((phi)p)m \mvee{} ((q=0))p) \mvdash{} \_:(A)sigma o m\}
20. (a0)p \mmember{} \{H.\mBbbI{} \mvdash{} \_:((A)sigma o m)[0(\mBbbI{})][((phi)p \mvee{} (q=0)) |{}\mrightarrow{} (((u)m \mvee{} ((a0)p)m))[0(\mBbbI{})]]\}
21. ((((phi)p)m)tau++ \mvee{} (((q=0))p)tau++) \mmember{} \{K.\mBbbI{}.\mBbbI{} \mvdash{} \_:\mBbbF{}\}
\mvdash{} (((u)m)tau++ \mvee{} (((a0)p)m)tau++) = (((u)tau+)m \mvee{} (((a0)tau)p)m)
By
Latex:
CubicalTermEqual
Home
Index