---

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

.....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))
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)(alpha)⌝;⌜w2⌝]⋅
    THENA Auto
    )
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
4: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)
14. ((w2 iota(z)(alpha) 1[z:=v]) 1[z:=v](iota(z)(alpha)) rename-one-name(v;z1))
= (w2 iota(z)(alpha) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(alpha)))
⊢ iota(z1) = (iota(z) o (1[z:=v] o rename-one-name(v;z1))) ∈ name-morph(I;[z1 / I])

2
.....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)
14. ((w2 iota(z)(alpha) 1[z:=v]) 1[z:=v](iota(z)(alpha)) rename-one-name(v;z1))
= (w2 iota(z)(alpha) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(alpha)))
⊢ ((w2 iota(z)(alpha) 1[z:=v]) iota(v)(alpha) rename-one-name(v;z1))
= ((w2 iota(z)(alpha) 1[z:=v]) 1[z:=v](iota(z)(alpha)) rename-one-name(v;z1))
∈ A(iota(z1)(alpha))

3
.....subterm..... T:t
3: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)
14. ((w2 iota(z)(alpha) 1[z:=v]) 1[z:=v](iota(z)(alpha)) rename-one-name(v;z1))
= (w2 iota(z)(alpha) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(alpha)))
⊢ (w2 iota(z)(alpha) rename-one-name(z;z1)) = (w2 iota(z)(alpha) (1[z:=v] o rename-one-name(v;z1))) ∈ A(iota(z1)(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.  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.  (w2  iota(z)(alpha)  rename-one-name(z;z1))  =  w3
12.  v  :  Cname
13.  \mneg{}(v  \mmember{}  I)
\mvdash{}  ((w2  iota(z)(alpha)  1[z:=v])  iota(v)(alpha)  rename-one-name(v;z1))
=  (w2  iota(z)(alpha)  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)(alpha)\mkleeneclose{};\mkleeneopen{}w2\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index