---

Step * 1 of Lemma I-path-morph-id

.....antecedent..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. z : {z:Cname| ¬(z ∈ I)} 
8. w2 : named-path(X;A;a;b;I;alpha;z)
9. z1 : {z:Cname| ¬(z ∈ I)} 
10. w3 : named-path(X;A;a;b;I;alpha;z1)
11. path-eq(X;A;I;alpha;<z, w2>;<z1, w3>)
⊢ path-eq(X;A;I;alpha;I-path-morph(X;A;I;I;1;alpha;<z, w2>);<z1, w3>)
BY
{ ((RepUR ``path-eq I-path-morph named-path-morph`` 0
    THEN (GenConclTerm ⌜fresh-cname(I)⌝⋅ THENA Auto)
    THEN Thin (-1)
    THEN D -1)
   THEN RepUR ``path-eq`` -3
   THEN NthHypEq (-3)
   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. z : {z:Cname| ¬(z ∈ I)} 
8. w2 : named-path(X;A;a;b;I;alpha;z)
9. z1 : {z:Cname| ¬(z ∈ I)} 
10. w3 : named-path(X;A;a;b;I;alpha;z1)
11. (w2 iota(z)(alpha) rename-one-name(z;z1)) = w3 ∈ A(iota(z1)(alpha))
12. v : Cname
13. ¬(v ∈ I)
⊢ ((w2 iota(z)(alpha) 1[z:=v]) iota(v)(alpha) rename-one-name(v;z1))
= (w2 iota(z)(alpha) rename-one-name(z;z1))
∈ A(iota(z1)(alpha))

---

Latex:

---

Latex:
.....antecedent..... 
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.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
8.  w2  :  named-path(X;A;a;b;I;alpha;z)
9.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
10.  w3  :  named-path(X;A;a;b;I;alpha;z1)
11.  path-eq(X;A;I;alpha;<z,  w2><z1,  w3>)
\mvdash{}  path-eq(X;A;I;alpha;I-path-morph(X;A;I;I;1;alpha;<z,  w2>);<z1,  w3>)


By

---

Latex:
((RepUR  ``path-eq  I-path-morph  named-path-morph``  0
    THEN  (GenConclTerm  \mkleeneopen{}fresh-cname(I)\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  Thin  (-1)
    THEN  D  -1)
  THEN  RepUR  ``path-eq``  -3
  THEN  NthHypEq  (-3)
  THEN  EqCD\mcdot{}
  THEN  Auto)

---

Home Index