---

Step * 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. z1 : Cname
8. ¬(z1 ∈ I)
9. a1 : A(iota(z1)(alpha))
10. name-path-endpoints(X;A;a;b;I;alpha;z1;a1)
11. z : Cname
12. ¬(z ∈ I)
13. b2 : named-path(X;A;a;b;I;alpha;z)
14. (a1 iota(z1)(alpha) rename-one-name(z1;z)) = b2 ∈ A(iota(z)(alpha))
15. ((a1 iota(z1)(alpha) rename-one-name(z1;z)) rename-one-name(z1;z)(iota(z1)(alpha)) rename-one-name(z;z1))
= (a1 iota(z1)(alpha) (rename-one-name(z1;z) o rename-one-name(z;z1)))
∈ A((rename-one-name(z1;z) o rename-one-name(z;z1))(iota(z1)(alpha)))
⊢ ((a1 iota(z1)(alpha) rename-one-name(z1;z)) iota(z)(alpha) rename-one-name(z;z1)) = a1 ∈ A(iota(z1)(alpha))
BY
{ TACTIC:((Assert ⌜(rename-one-name(z1;z) o rename-one-name(z;z1)) = 1 ∈ name-morph([z1 / I];[z1 / I])⌝⋅
           THENA ((InstLemma `rename-one-comp` [⌜I⌝]⋅ THENA Auto)
                  THEN (RWO "-1" 0 THEN Auto)
                  THEN BLemma `rename-one-same` 
                  THEN Auto)
           )
          THEN NthHypEq (-2)
          THEN EqCD
          THEN Auto) }

1
.....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. z1 : Cname
8. ¬(z1 ∈ I)
9. a1 : A(iota(z1)(alpha))
10. name-path-endpoints(X;A;a;b;I;alpha;z1;a1)
11. z : Cname
12. ¬(z ∈ I)
13. b2 : named-path(X;A;a;b;I;alpha;z)
14. (a1 iota(z1)(alpha) rename-one-name(z1;z)) = b2 ∈ A(iota(z)(alpha))
15. ((a1 iota(z1)(alpha) rename-one-name(z1;z)) rename-one-name(z1;z)(iota(z1)(alpha)) rename-one-name(z;z1))
= (a1 iota(z1)(alpha) (rename-one-name(z1;z) o rename-one-name(z;z1)))
∈ A((rename-one-name(z1;z) o rename-one-name(z;z1))(iota(z1)(alpha)))
16. (rename-one-name(z1;z) o rename-one-name(z;z1)) = 1 ∈ name-morph([z1 / I];[z1 / I])
⊢ ((a1 iota(z1)(alpha) rename-one-name(z1;z)) iota(z)(alpha) rename-one-name(z;z1))
= ((a1 iota(z1)(alpha) rename-one-name(z1;z)) rename-one-name(z1;z)(iota(z1)(alpha)) rename-one-name(z;z1))
∈ A(iota(z1)(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.  z1  :  Cname
8.  \mneg{}(z1  \mmember{}  I)
9.  a1  :  A(iota(z1)(alpha))
10.  name-path-endpoints(X;A;a;b;I;alpha;z1;a1)
11.  z  :  Cname
12.  \mneg{}(z  \mmember{}  I)
13.  b2  :  named-path(X;A;a;b;I;alpha;z)
14.  (a1  iota(z1)(alpha)  rename-one-name(z1;z))  =  b2
15.  ((a1  iota(z1)(alpha)  rename-one-name(z1;z))  rename-one-name(z1;z)(iota(z1)(alpha))  ...)
=  (a1  iota(z1)(alpha)  (rename-one-name(z1;z)  o  rename-one-name(z;z1)))
\mvdash{}  ((a1  iota(z1)(alpha)  rename-one-name(z1;z))  iota(z)(alpha)  rename-one-name(z;z1))  =  a1


By

---

Latex:
TACTIC:((Assert  \mkleeneopen{}(rename-one-name(z1;z)  o  rename-one-name(z;z1))  =  1\mkleeneclose{}\mcdot{}
                  THENA  ((InstLemma  `rename-one-comp`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  (RWO  "-1"  0  THEN  Auto)
                                THEN  BLemma  `rename-one-same` 
                                THEN  Auto)
                  )
                THEN  NthHypEq  (-2)
                THEN  EqCD
                THEN  Auto)

---

Home Index