Step
*
1
1
2
2
1
2
1
2
of Lemma
cubical-id-box_wf
.....subterm..... T:t
2:n
1. I : Cname List
2. c : ℕ2
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. x1 : nameset(I)
14. i1 : ℕ2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
16. ¬(fresh-cname(I) = x1 ∈ Cname)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I))
∧ (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I))
⊢ (v2 (x1:=i1)(iota(fresh-cname(I))(alpha)) (fresh-cname(I):=c))
= (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c))
∈ A(((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha)))
BY
{ TACTIC:(EquationSubsume EqCD THEN Try (QuickAuto) THEN Try (Fold `member` 0)) }
1
1. I : Cname List
2. c : ℕ2
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. x1 : nameset(I)
14. i1 : ℕ2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
16. ¬(fresh-cname(I) = x1 ∈ Cname)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I))
∧ (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I))
⊢ A(((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha)))
= A((fresh-cname(I):=c)((x1:=i1)(iota(fresh-cname(I))(alpha))))
∈ Type
2
1. I : Cname List
2. c : ℕ2
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. x1 : nameset(I)
14. i1 : ℕ2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
16. ¬(fresh-cname(I) = x1 ∈ Cname)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I))
∧ (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I))
22. A(((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha)))
= A((fresh-cname(I):=c)((x1:=i1)(iota(fresh-cname(I))(alpha))))
∈ Type
⊢ (fresh-cname(I):=c) ∈ name-morph([fresh-cname(I) / I]-[x1];[fresh-cname(I) / I]-[fresh-cname(I); x1])
3
.....subterm..... T:t
5:n
1. I : Cname List
2. c : ℕ2
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. x1 : nameset(I)
14. i1 : ℕ2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
16. ¬(fresh-cname(I) = x1 ∈ Cname)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I))
∧ (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I))
22. A(((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha)))
= A((fresh-cname(I):=c)((x1:=i1)(iota(fresh-cname(I))(alpha))))
∈ Type
⊢ (x1:=i1)(iota(fresh-cname(I))(alpha)) = iota(fresh-cname(I))((x1:=i1)(alpha)) ∈ X([fresh-cname(I) / I]-[x1])
4
1. I : Cname List
2. c : ℕ2
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. x1 : nameset(I)
14. i1 : ℕ2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
16. ¬(fresh-cname(I) = x1 ∈ Cname)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I))
∧ (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I))
22. A(((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha)))
= A((fresh-cname(I):=c)((x1:=i1)(iota(fresh-cname(I))(alpha))))
∈ Type
⊢ v2 ∈ A((x1:=i1)(iota(fresh-cname(I))(alpha)))
Latex:
Latex:
.....subterm..... T:t
2:n
1. I : Cname List
2. c : \mBbbN{}2
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. x1 : nameset(I)
14. i1 : \mBbbN{}2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
16. \mneg{}(fresh-cname(I) = x1)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]]
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1]
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1)
\mwedge{} (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
\mvdash{} (v2 (x1:=i1)(iota(fresh-cname(I))(alpha)) (fresh-cname(I):=c))
= (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c))
By
Latex:
TACTIC:(EquationSubsume EqCD THEN Try (QuickAuto) THEN Try (Fold `member` 0))
Home
Index