Step
*
3
2
1
1
of Lemma
path-eq-equiv
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. Sym(z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;alpha;z);p,q.let z,w = p
in let z',w' = q
in (w iota(z)(alpha) rename-one-name(z;z'))
= w'
∈ A(iota(z')(alpha)))
8. z2 : Cname
9. ¬(z2 ∈ I)
10. a1 : A(iota(z2)(alpha))
11. name-path-endpoints(X;A;a;b;I;alpha;z2;a1)
12. z1 : Cname
13. ¬(z1 ∈ I)
14. b1 : named-path(X;A;a;b;I;alpha;z1)
15. z : Cname
16. ¬(z ∈ I)
17. c1 : named-path(X;A;a;b;I;alpha;z)
18. (a1 iota(z2)(alpha) rename-one-name(z2;z1)) = b1 ∈ A(iota(z1)(alpha))
19. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z)) = c1 ∈ A(iota(z)(alpha))
20. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) rename-one-name(z2;z1)(iota(z2)(alpha)) rename-one-name(z1;z))
= (a1 iota(z2)(alpha) (rename-one-name(z2;z1) o rename-one-name(z1;z)))
∈ A((rename-one-name(z2;z1) o rename-one-name(z1;z))(iota(z2)(alpha)))
⊢ (a1 iota(z2)(alpha) rename-one-name(z2;z))
= ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z))
∈ A(iota(z)(alpha))
BY
{ TACTIC:(Symmetry THEN NthHypEq (-1) THEN EqCD THEN Auto) }
1
.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. Sym(z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;alpha;z);p,q.let z,w = p
in let z',w' = q
in (w iota(z)(alpha) rename-one-name(z;z'))
= w'
∈ A(iota(z')(alpha)))
8. z2 : Cname
9. ¬(z2 ∈ I)
10. a1 : A(iota(z2)(alpha))
11. name-path-endpoints(X;A;a;b;I;alpha;z2;a1)
12. z1 : Cname
13. ¬(z1 ∈ I)
14. b1 : named-path(X;A;a;b;I;alpha;z1)
15. z : Cname
16. ¬(z ∈ I)
17. c1 : named-path(X;A;a;b;I;alpha;z)
18. (a1 iota(z2)(alpha) rename-one-name(z2;z1)) = b1 ∈ A(iota(z1)(alpha))
19. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z)) = c1 ∈ A(iota(z)(alpha))
20. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) rename-one-name(z2;z1)(iota(z2)(alpha)) rename-one-name(z1;z))
= (a1 iota(z2)(alpha) (rename-one-name(z2;z1) o rename-one-name(z1;z)))
∈ A((rename-one-name(z2;z1) o rename-one-name(z1;z))(iota(z2)(alpha)))
⊢ iota(z)(alpha) = (rename-one-name(z2;z1) o rename-one-name(z1;z))(iota(z2)(alpha)) ∈ X([z / I])
2
.....subterm..... T:t
2:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. Sym(z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;alpha;z);p,q.let z,w = p
in let z',w' = q
in (w iota(z)(alpha) rename-one-name(z;z'))
= w'
∈ A(iota(z')(alpha)))
8. z2 : Cname
9. ¬(z2 ∈ I)
10. a1 : A(iota(z2)(alpha))
11. name-path-endpoints(X;A;a;b;I;alpha;z2;a1)
12. z1 : Cname
13. ¬(z1 ∈ I)
14. b1 : named-path(X;A;a;b;I;alpha;z1)
15. z : Cname
16. ¬(z ∈ I)
17. c1 : named-path(X;A;a;b;I;alpha;z)
18. (a1 iota(z2)(alpha) rename-one-name(z2;z1)) = b1 ∈ A(iota(z1)(alpha))
19. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z)) = c1 ∈ A(iota(z)(alpha))
20. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) rename-one-name(z2;z1)(iota(z2)(alpha)) rename-one-name(z1;z))
= (a1 iota(z2)(alpha) (rename-one-name(z2;z1) o rename-one-name(z1;z)))
∈ A((rename-one-name(z2;z1) o rename-one-name(z1;z))(iota(z2)(alpha)))
⊢ ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z))
= ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) rename-one-name(z2;z1)(iota(z2)(alpha)) rename-one-name(z1;z))
∈ A(iota(z)(alpha))
3
.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. Sym(z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;alpha;z);p,q.let z,w = p
in let z',w' = q
in (w iota(z)(alpha) rename-one-name(z;z'))
= w'
∈ A(iota(z')(alpha)))
8. z2 : Cname
9. ¬(z2 ∈ I)
10. a1 : A(iota(z2)(alpha))
11. name-path-endpoints(X;A;a;b;I;alpha;z2;a1)
12. z1 : Cname
13. ¬(z1 ∈ I)
14. b1 : named-path(X;A;a;b;I;alpha;z1)
15. z : Cname
16. ¬(z ∈ I)
17. c1 : named-path(X;A;a;b;I;alpha;z)
18. (a1 iota(z2)(alpha) rename-one-name(z2;z1)) = b1 ∈ A(iota(z1)(alpha))
19. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z)) = c1 ∈ A(iota(z)(alpha))
20. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) rename-one-name(z2;z1)(iota(z2)(alpha)) rename-one-name(z1;z))
= (a1 iota(z2)(alpha) (rename-one-name(z2;z1) o rename-one-name(z1;z)))
∈ A((rename-one-name(z2;z1) o rename-one-name(z1;z))(iota(z2)(alpha)))
⊢ (a1 iota(z2)(alpha) rename-one-name(z2;z))
= (a1 iota(z2)(alpha) (rename-one-name(z2;z1) o rename-one-name(z1;z)))
∈ A(iota(z)(alpha))
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_\}
3. a : \{X \mvdash{} \_:A\}
4. b : \{X \mvdash{} \_:A\}
5. I : Cname List
6. alpha : X(I)
7. Sym(z:\{z:Cname| \mneg{}(z \mmember{} I)\}
\mtimes{} named-path(X;A;a;b;I;alpha;z);p,q.let z,w = p
in let z',w' = q
in (w iota(z)(alpha) rename-one-name(z;z')) = w')
8. z2 : Cname
9. \mneg{}(z2 \mmember{} I)
10. a1 : A(iota(z2)(alpha))
11. name-path-endpoints(X;A;a;b;I;alpha;z2;a1)
12. z1 : Cname
13. \mneg{}(z1 \mmember{} I)
14. b1 : named-path(X;A;a;b;I;alpha;z1)
15. z : Cname
16. \mneg{}(z \mmember{} I)
17. c1 : named-path(X;A;a;b;I;alpha;z)
18. (a1 iota(z2)(alpha) rename-one-name(z2;z1)) = b1
19. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z)) = c1
20. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) rename-one-name(z2;z1)(iota(z2)(alpha)) ...)
= (a1 iota(z2)(alpha) (rename-one-name(z2;z1) o rename-one-name(z1;z)))
\mvdash{} (a1 iota(z2)(alpha) rename-one-name(z2;z))
= ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z))
By
Latex:
TACTIC:(Symmetry THEN NthHypEq (-1) THEN EqCD THEN Auto)
Home
Index