Step
*
1
1
2
2
1
1
1
of Lemma
set-path-name_wf
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. a@0 : X(I)@i
7. (z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;a@0;z)) ⊆r cubical-path(X;A;a;b;I;a@0)
8. v : {x:Cname| ¬(x ∈ I)}
9. named-path(X;A;a;b;I;1(a@0);v) ⊆r A(iota(v)(a@0))
10. z : {z:Cname| ¬(z ∈ I)} @i
11. u2 : named-path(X;A;a;b;I;a@0;z)@i
12. z1 : {z:Cname| ¬(z ∈ I)} @i
13. q1 : named-path(X;A;a;b;I;a@0;z1)@i
14. (u2 iota(z)(a@0) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(a@0))
⊢ ((u2 iota(z)(a@0) 1[z:=v]) iota(v)(a@0) rename-one-name(v;z1))
= (u2 iota(z)(a@0) rename-one-name(z;z1))
∈ A(iota(z1)(a@0))
BY
{ ((InstLemma `cubical-type-ap-morph-comp`
[⌜X⌝;⌜A⌝;⌜[z / I]⌝;⌜[v / I]⌝;⌜[z1 / I]⌝;⌜1[z:=v]⌝;⌜rename-one-name(v;z1)⌝;⌜iota(z)(a@0)⌝;⌜u2⌝]⋅
THENA Auto
)
THEN NthHypEq (-1)
THEN EqCDA) }
1
.....subterm..... T:t
1:n
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. a@0 : X(I)@i
7. (z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;a@0;z)) ⊆r cubical-path(X;A;a;b;I;a@0)
8. v : {x:Cname| ¬(x ∈ I)}
9. named-path(X;A;a;b;I;1(a@0);v) ⊆r A(iota(v)(a@0))
10. z : {z:Cname| ¬(z ∈ I)} @i
11. u2 : named-path(X;A;a;b;I;a@0;z)@i
12. z1 : {z:Cname| ¬(z ∈ I)} @i
13. q1 : named-path(X;A;a;b;I;a@0;z1)@i
14. (u2 iota(z)(a@0) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(a@0))
15. ((u2 iota(z)(a@0) 1[z:=v]) 1[z:=v](iota(z)(a@0)) rename-one-name(v;z1))
= (u2 iota(z)(a@0) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(a@0)))
⊢ A(iota(z1)(a@0)) = A((1[z:=v] o rename-one-name(v;z1))(iota(z)(a@0))) ∈ Type
2
.....subterm..... T:t
2:n
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. a@0 : X(I)@i
7. (z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;a@0;z)) ⊆r cubical-path(X;A;a;b;I;a@0)
8. v : {x:Cname| ¬(x ∈ I)}
9. named-path(X;A;a;b;I;1(a@0);v) ⊆r A(iota(v)(a@0))
10. z : {z:Cname| ¬(z ∈ I)} @i
11. u2 : named-path(X;A;a;b;I;a@0;z)@i
12. z1 : {z:Cname| ¬(z ∈ I)} @i
13. q1 : named-path(X;A;a;b;I;a@0;z1)@i
14. (u2 iota(z)(a@0) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(a@0))
15. ((u2 iota(z)(a@0) 1[z:=v]) 1[z:=v](iota(z)(a@0)) rename-one-name(v;z1))
= (u2 iota(z)(a@0) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(a@0)))
⊢ ((u2 iota(z)(a@0) 1[z:=v]) iota(v)(a@0) rename-one-name(v;z1))
= ((u2 iota(z)(a@0) 1[z:=v]) 1[z:=v](iota(z)(a@0)) rename-one-name(v;z1))
∈ A(iota(z1)(a@0))
3
.....subterm..... T:t
3:n
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. a@0 : X(I)@i
7. (z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;a@0;z)) ⊆r cubical-path(X;A;a;b;I;a@0)
8. v : {x:Cname| ¬(x ∈ I)}
9. named-path(X;A;a;b;I;1(a@0);v) ⊆r A(iota(v)(a@0))
10. z : {z:Cname| ¬(z ∈ I)} @i
11. u2 : named-path(X;A;a;b;I;a@0;z)@i
12. z1 : {z:Cname| ¬(z ∈ I)} @i
13. q1 : named-path(X;A;a;b;I;a@0;z1)@i
14. (u2 iota(z)(a@0) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(a@0))
15. ((u2 iota(z)(a@0) 1[z:=v]) 1[z:=v](iota(z)(a@0)) rename-one-name(v;z1))
= (u2 iota(z)(a@0) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(a@0)))
⊢ (u2 iota(z)(a@0) rename-one-name(z;z1)) = (u2 iota(z)(a@0) (1[z:=v] o rename-one-name(v;z1))) ∈ A(iota(z1)(a@0))
Latex:
Latex:
1. X : CubicalSet@i'
2. A : \{X \mvdash{} \_\}@i'
3. a : \{X \mvdash{} \_:A\}@i
4. b : \{X \mvdash{} \_:A\}@i
5. I : Cname List@i
6. a@0 : X(I)@i
7. (z:\{z:Cname| \mneg{}(z \mmember{} I)\} \mtimes{} named-path(X;A;a;b;I;a@0;z)) \msubseteq{}r cubical-path(X;A;a;b;I;a@0)
8. v : \{x:Cname| \mneg{}(x \mmember{} I)\}
9. named-path(X;A;a;b;I;1(a@0);v) \msubseteq{}r A(iota(v)(a@0))
10. z : \{z:Cname| \mneg{}(z \mmember{} I)\} @i
11. u2 : named-path(X;A;a;b;I;a@0;z)@i
12. z1 : \{z:Cname| \mneg{}(z \mmember{} I)\} @i
13. q1 : named-path(X;A;a;b;I;a@0;z1)@i
14. (u2 iota(z)(a@0) rename-one-name(z;z1)) = q1
\mvdash{} ((u2 iota(z)(a@0) 1[z:=v]) iota(v)(a@0) rename-one-name(v;z1))
= (u2 iota(z)(a@0) rename-one-name(z;z1))
By
Latex:
((InstLemma `cubical-type-ap-morph-comp`
[\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[z / I]\mkleeneclose{};\mkleeneopen{}[v / I]\mkleeneclose{};\mkleeneopen{}[z1 / I]\mkleeneclose{};\mkleeneopen{}1[z:=v]\mkleeneclose{};\mkleeneopen{}rename-one-name(v;z1)\mkleeneclose{};\mkleeneopen{}iota(z)(a@0)\mkleeneclose{};\mkleeneopen{}u2\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN NthHypEq (-1)
THEN EqCDA)
Home
Index