Step
*
1
1
2
2
1
1
3
of Lemma
cubical-id-box_wf
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)}
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
20. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
21. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
22. (iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I)
23. alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I)
⊢ (iota(fresh-cname(I)) o ((x1:=i1) o (fresh-cname(I):=c)))(alpha)
= ((fresh-cname(I):=c) o (x1:=i1))(iota(fresh-cname(I))(alpha))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
BY
{ TACTIC:(RWO "cube-set-restriction-comp" 0 THEN Try (NameCompWf) THEN Auto) }
1
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)}
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
20. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
21. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
22. (iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I)
23. alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I)
⊢ (iota(fresh-cname(I)) o ((x1:=i1) o (fresh-cname(I):=c))) ∈ name-morph(I;[fresh-cname(I) / I]-[fresh-cname(I); x1])
2
.....wf.....
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)}
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
20. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
21. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
22. (iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I)
23. alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I)
24. ∀[f:name-morph([fresh-cname(I) / I];[fresh-cname(I) / I]-[fresh-cname(I)])].
∀[g:name-morph([fresh-cname(I) / I]-[fresh-cname(I)];[fresh-cname(I) / I]-[fresh-cname(I); x1])].
((f o g) ∈ name-morph([fresh-cname(I) / I];[fresh-cname(I) / I]-[fresh-cname(I); x1]))
⊢ (x1:=i1) ∈ name-morph([fresh-cname(I) / I]-[fresh-cname(I)];[fresh-cname(I) / I]-[fresh-cname(I); x1])
3
.....subterm..... T:t
4:n
1. c : ℕ2
2. I : Cname List
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. v : {x:Cname| ¬(x ∈ I)}
14. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
15. x1 : nameset(I)
16. i1 : ℕ2
17. ¬(fresh-cname(I) = x1 ∈ Cname)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
20. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
21. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
22. (iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I)
23. alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I)
⊢ (iota(fresh-cname(I)) o ((x1:=i1) o (fresh-cname(I):=c)))
= (iota(fresh-cname(I)) o ((fresh-cname(I):=c) o (x1:=i1)))
∈ name-morph(I;[fresh-cname(I) / I]-[fresh-cname(I); x1])
Latex:
Latex:
1. c : \mBbbN{}2
2. I : Cname List
3. X : CubicalSet
4. A : \{X \mvdash{} \_\}
5. a : \{X \mvdash{} \_:A\}
6. b : \{X \mvdash{} \_:A\}
7. J : nameset(I) List
8. x : nameset(I)
9. i : \mBbbN{}2
10. alpha : X(I)
11. \mneg{}(fresh-cname(I) \mmember{} J)
12. \mneg{}(x = fresh-cname(I))
13. v : \{x:Cname| \mneg{}(x \mmember{} I)\}
14. fresh-cname(I) = v
15. x1 : nameset(I)
16. i1 : \mBbbN{}2
17. \mneg{}(fresh-cname(I) = x1)
18. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
19. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha))
20. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]]
21. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1]
22. (iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1
23. alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha))
\mvdash{} (iota(fresh-cname(I)) o ((x1:=i1) o (fresh-cname(I):=c)))(alpha)
= ((fresh-cname(I):=c) o (x1:=i1))(iota(fresh-cname(I))(alpha))
By
Latex:
TACTIC:(RWO "cube-set-restriction-comp" 0 THEN Try (NameCompWf) THEN Auto)
Home
Index