Step
*
1
1
1
4
1
of Lemma
I-path-morph-comp
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a@0 : X(I)
11. z : {z:Cname| ¬(z ∈ I)}
12. u2 : named-path(X;A;a;b;I;a@0;z)
13. z1 : {z:Cname| ¬(z ∈ I)}
14. u3 : named-path(X;A;a;b;I;a@0;z1)
15. (u2 iota(z)(a@0) rename-one-name(z;z1)) = u3 ∈ A(iota(z1)(a@0))
16. v : Cname
17. ¬(v ∈ K)
18. v1 : Cname
19. ¬(v1 ∈ J)
20. ((u2 iota(z)(a@0) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(a@0)) f[z1:=v1])
= (u2 iota(z)(a@0) (rename-one-name(z;z1) o f[z1:=v1]))
∈ A((rename-one-name(z;z1) o f[z1:=v1])(iota(z)(a@0)))
⊢ (u2 iota(z)(a@0) (f o g)[z:=v])
= (((u2 iota(z)(a@0) rename-one-name(z;z1)) iota(z1)(a@0) f[z1:=v1]) iota(v1)(f(a@0)) g[v1:=v])
∈ A(iota(v)((f o g)(a@0)))
BY
{ ApFunToHypEquands `Z' ⌜(Z iota(v1)(f(a@0)) g[v1:=v])⌝ ⌜A(iota(v)((f o g)(a@0)))⌝ (-1)⋅ }
1
.....fun wf.....
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a@0 : X(I)
11. z : {z:Cname| ¬(z ∈ I)}
12. u2 : named-path(X;A;a;b;I;a@0;z)
13. z1 : {z:Cname| ¬(z ∈ I)}
14. u3 : named-path(X;A;a;b;I;a@0;z1)
15. (u2 iota(z)(a@0) rename-one-name(z;z1)) = u3 ∈ A(iota(z1)(a@0))
16. v : Cname
17. ¬(v ∈ K)
18. v1 : Cname
19. ¬(v1 ∈ J)
20. ((u2 iota(z)(a@0) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(a@0)) f[z1:=v1])
= (u2 iota(z)(a@0) (rename-one-name(z;z1) o f[z1:=v1]))
∈ A((rename-one-name(z;z1) o f[z1:=v1])(iota(z)(a@0)))
21. Z : A((rename-one-name(z;z1) o f[z1:=v1])(iota(z)(a@0)))
⊢ (Z iota(v1)(f(a@0)) g[v1:=v]) = (Z iota(v1)(f(a@0)) g[v1:=v]) ∈ A(iota(v)((f o g)(a@0)))
2
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a@0 : X(I)
11. z : {z:Cname| ¬(z ∈ I)}
12. u2 : named-path(X;A;a;b;I;a@0;z)
13. z1 : {z:Cname| ¬(z ∈ I)}
14. u3 : named-path(X;A;a;b;I;a@0;z1)
15. (u2 iota(z)(a@0) rename-one-name(z;z1)) = u3 ∈ A(iota(z1)(a@0))
16. v : Cname
17. ¬(v ∈ K)
18. v1 : Cname
19. ¬(v1 ∈ J)
20. ((u2 iota(z)(a@0) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(a@0)) f[z1:=v1])
= (u2 iota(z)(a@0) (rename-one-name(z;z1) o f[z1:=v1]))
∈ A((rename-one-name(z;z1) o f[z1:=v1])(iota(z)(a@0)))
21. (((u2 iota(z)(a@0) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(a@0)) f[z1:=v1]) iota(v1)(f(a@0)) g[v1:=v])
= ((u2 iota(z)(a@0) (rename-one-name(z;z1) o f[z1:=v1])) iota(v1)(f(a@0)) g[v1:=v])
∈ A(iota(v)((f o g)(a@0)))
⊢ (u2 iota(z)(a@0) (f o g)[z:=v])
= (((u2 iota(z)(a@0) rename-one-name(z;z1)) iota(z1)(a@0) f[z1:=v1]) iota(v1)(f(a@0)) g[v1:=v])
∈ A(iota(v)((f o g)(a@0)))
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_\}
3. a : \{X \mvdash{} \_:A\}
4. b : \{X \mvdash{} \_:A\}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a@0 : X(I)
11. z : \{z:Cname| \mneg{}(z \mmember{} I)\}
12. u2 : named-path(X;A;a;b;I;a@0;z)
13. z1 : \{z:Cname| \mneg{}(z \mmember{} I)\}
14. u3 : named-path(X;A;a;b;I;a@0;z1)
15. (u2 iota(z)(a@0) rename-one-name(z;z1)) = u3
16. v : Cname
17. \mneg{}(v \mmember{} K)
18. v1 : Cname
19. \mneg{}(v1 \mmember{} J)
20. ((u2 iota(z)(a@0) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(a@0)) f[z1:=v1])
= (u2 iota(z)(a@0) (rename-one-name(z;z1) o f[z1:=v1]))
\mvdash{} (u2 iota(z)(a@0) (f o g)[z:=v])
= (((u2 iota(z)(a@0) rename-one-name(z;z1)) iota(z1)(a@0) f[z1:=v1]) iota(v1)(f(a@0)) g[v1:=v])
By
Latex:
ApFunToHypEquands `Z' \mkleeneopen{}(Z iota(v1)(f(a@0)) g[v1:=v])\mkleeneclose{} \mkleeneopen{}A(iota(v)((f o g)(a@0)))\mkleeneclose{} (-1)\mcdot{}
Home
Index