---

Step * 3 2 1 of Lemma path-eq-equiv

.....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 : named-path(X;A;a;b;I;alpha;z2)
11. z1 : Cname
12. ¬(z1 ∈ I)
13. b1 : named-path(X;A;a;b;I;alpha;z1)
14. z : Cname
15. ¬(z ∈ I)
16. c1 : named-path(X;A;a;b;I;alpha;z)
17. (a1 iota(z2)(alpha) rename-one-name(z2;z1)) = b1 ∈ A(iota(z1)(alpha))
18. ((a1 iota(z2)(alpha) rename-one-name(z2;z1)) iota(z1)(alpha) rename-one-name(z1;z)) = c1 ∈ A(iota(z)(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:(DVar `a1'
          THEN (InstLemma `cubical-type-ap-morph-comp` 
                [⌜X⌝;⌜A⌝;⌜[z2 / I]⌝;⌜[z1 / I]⌝;⌜[z / I]⌝
                ;⌜rename-one-name(z2;z1)⌝;⌜rename-one-name(z1;z)⌝
                ;⌜iota(z2)(alpha)⌝;⌜a1⌝]⋅
                THENA Auto
                )
          ) }

1
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))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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  :  named-path(X;A;a;b;I;alpha;z2)
11.  z1  :  Cname
12.  \mneg{}(z1  \mmember{}  I)
13.  b1  :  named-path(X;A;a;b;I;alpha;z1)
14.  z  :  Cname
15.  \mneg{}(z  \mmember{}  I)
16.  c1  :  named-path(X;A;a;b;I;alpha;z)
17.  (a1  iota(z2)(alpha)  rename-one-name(z2;z1))  =  b1
18.  ((a1  iota(z2)(alpha)  rename-one-name(z2;z1))  iota(z1)(alpha)  rename-one-name(z1;z))  =  c1
\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:(DVar  `a1'
                THEN  (InstLemma  `cubical-type-ap-morph-comp` 
                            [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[z2  /  I]\mkleeneclose{};\mkleeneopen{}[z1  /  I]\mkleeneclose{};\mkleeneopen{}[z  /  I]\mkleeneclose{}
                            ;\mkleeneopen{}rename-one-name(z2;z1)\mkleeneclose{};\mkleeneopen{}rename-one-name(z1;z)\mkleeneclose{}
                            ;\mkleeneopen{}iota(z2)(alpha)\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}
                            THENA  Auto
                            )
                )

---

Home Index