---

Step * 1 1 1 1 of Lemma set-path-name_wf

.....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. alpha : X(I)@i
7. (z:{z:Cname| ¬(z ∈ I)}  × named-path(X;A;a;b;I;alpha;z)) ⊆r cubical-path(X;A;a;b;I;alpha)
8. x : {x:Cname| ¬(x ∈ I)} 
9. named-path(X;A;a;b;I;1(alpha);x) ⊆r A(iota(x)(alpha))
10. z : {z:Cname| ¬(z ∈ I)} @i
11. p1 : named-path(X;A;a;b;I;alpha;z)@i
12. z1 : {z:Cname| ¬(z ∈ I)} @i
13. q1 : named-path(X;A;a;b;I;alpha;z1)@i
14. (p1 iota(z)(alpha) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(alpha))
⊢ named-path-morph(X;A;I;I;z;x;1;alpha;p1) = named-path-morph(X;A;I;I;z1;x;1;alpha;q1) ∈ named-path(X;A;a;b;I;alpha;x)
BY
{ TACTIC:(BLemma `equal-named-paths`
          THEN Auto
          THEN (Assert ⌜(A(1[z1:=x](iota(z1)(alpha))) = A(iota(x)(alpha)) ∈ Type)
                        ∧ (A(1[z:=x](iota(z)(alpha))) = A(iota(x)(alpha)) ∈ Type)⌝⋅
                THENA (Auto THEN EqCD THEN Auto THEN RWO "cube-set-restriction-comp" 0 THEN Auto THEN EqCD THEN Auto)
                )) }

1
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. alpha : X(I)@i
7. (z:{z:Cname| ¬(z ∈ I)}  × named-path(X;A;a;b;I;alpha;z)) ⊆r cubical-path(X;A;a;b;I;alpha)
8. x : {x:Cname| ¬(x ∈ I)} 
9. named-path(X;A;a;b;I;1(alpha);x) ⊆r A(iota(x)(alpha))
10. z : {z:Cname| ¬(z ∈ I)} @i
11. p1 : named-path(X;A;a;b;I;alpha;z)@i
12. z1 : {z:Cname| ¬(z ∈ I)} @i
13. q1 : named-path(X;A;a;b;I;alpha;z1)@i
14. (p1 iota(z)(alpha) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(alpha))
15. (A(1[z1:=x](iota(z1)(alpha))) = A(iota(x)(alpha)) ∈ Type) ∧ (A(1[z:=x](iota(z)(alpha))) = A(iota(x)(alpha)) ∈ Type)
⊢ named-path-morph(X;A;I;I;z;x;1;alpha;p1) = named-path-morph(X;A;I;I;z1;x;1;alpha;q1) ∈ A(iota(x)(alpha))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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.  alpha  :  X(I)@i
7.  (z:\{z:Cname|  \mneg{}(z  \mmember{}  I)\}    \mtimes{}  named-path(X;A;a;b;I;alpha;z))  \msubseteq{}r  cubical-path(X;A;a;b;I;alpha)
8.  x  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
9.  named-path(X;A;a;b;I;1(alpha);x)  \msubseteq{}r  A(iota(x)(alpha))
10.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\}  @i
11.  p1  :  named-path(X;A;a;b;I;alpha;z)@i
12.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\}  @i
13.  q1  :  named-path(X;A;a;b;I;alpha;z1)@i
14.  (p1  iota(z)(alpha)  rename-one-name(z;z1))  =  q1
\mvdash{}  named-path-morph(X;A;I;I;z;x;1;alpha;p1)  =  named-path-morph(X;A;I;I;z1;x;1;alpha;q1)


By

---

Latex:
TACTIC:(BLemma  `equal-named-paths`
                THEN  Auto
                THEN  (Assert  \mkleeneopen{}(A(1[z1:=x](iota(z1)(alpha)))  =  A(iota(x)(alpha)))
                                            \mwedge{}  (A(1[z:=x](iota(z)(alpha)))  =  A(iota(x)(alpha)))\mkleeneclose{}\mcdot{}
                            THENA  (Auto
                                          THEN  EqCD
                                          THEN  Auto
                                          THEN  RWO  "cube-set-restriction-comp"  0
                                          THEN  Auto
                                          THEN  EqCD
                                          THEN  Auto)
                            ))

---

Home Index