---

Step * 1 1 of Lemma I-path-morph_functionality


1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : {z:Cname| ¬(z ∈ I)} 
10. p1 : named-path(X;A;a;b;I;alpha;z)
11. z1 : {z:Cname| ¬(z ∈ I)} 
12. q1 : named-path(X;A;a;b;I;alpha;z1)
13. (p1 iota(z)(alpha) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(alpha))
14. v : Cname
15. ¬(v ∈ K)
16. ∀z:Cname. rename-one-name(z;z) = 1 ∈ name-morph([z / K];[z / K]) supposing ¬(z ∈ K)
⊢ (p1 iota(z)(alpha) f[z:=v])
= ((p1 iota(z)(alpha) rename-one-name(z;z1)) iota(z1)(alpha) f[z1:=v])
∈ A(iota(v)(f(alpha)))
BY
{ ((InstLemma `cubical-type-ap-morph-comp`
       [⌜X⌝;⌜A⌝;⌜[z / I]⌝;⌜[z1 / I]⌝;⌜[v / K]⌝;⌜rename-one-name(z;z1)⌝;⌜f[z1:=v]⌝;⌜iota(z)(alpha)⌝;⌜p1⌝]⋅
    THENA Auto
    )
   THEN (Symmetry 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. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : {z:Cname| ¬(z ∈ I)} 
10. p1 : named-path(X;A;a;b;I;alpha;z)
11. z1 : {z:Cname| ¬(z ∈ I)} 
12. q1 : named-path(X;A;a;b;I;alpha;z1)
13. (p1 iota(z)(alpha) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(alpha))
14. v : Cname
15. ¬(v ∈ K)
16. ∀z:Cname. rename-one-name(z;z) = 1 ∈ name-morph([z / K];[z / K]) supposing ¬(z ∈ K)
17. ((p1 iota(z)(alpha) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(alpha)) f[z1:=v])
= (p1 iota(z)(alpha) (rename-one-name(z;z1) o f[z1:=v]))
∈ A((rename-one-name(z;z1) o f[z1:=v])(iota(z)(alpha)))
⊢ (f o iota(v)) = (iota(z) o (rename-one-name(z;z1) o f[z1:=v])) ∈ name-morph(I;[v / K])

2
.....subterm..... T:t
4:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : {z:Cname| ¬(z ∈ I)} 
10. p1 : named-path(X;A;a;b;I;alpha;z)
11. z1 : {z:Cname| ¬(z ∈ I)} 
12. q1 : named-path(X;A;a;b;I;alpha;z1)
13. (p1 iota(z)(alpha) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(alpha))
14. v : Cname
15. ¬(v ∈ K)
16. ∀z:Cname. rename-one-name(z;z) = 1 ∈ name-morph([z / K];[z / K]) supposing ¬(z ∈ K)
17. ((p1 iota(z)(alpha) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(alpha)) f[z1:=v])
= (p1 iota(z)(alpha) (rename-one-name(z;z1) o f[z1:=v]))
∈ A((rename-one-name(z;z1) o f[z1:=v])(iota(z)(alpha)))
⊢ iota(z1) = (iota(z) o rename-one-name(z;z1)) ∈ name-morph(I;[z1 / I])

3
.....subterm..... T:t
4:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. alpha : X(I)
9. z : {z:Cname| ¬(z ∈ I)} 
10. p1 : named-path(X;A;a;b;I;alpha;z)
11. z1 : {z:Cname| ¬(z ∈ I)} 
12. q1 : named-path(X;A;a;b;I;alpha;z1)
13. (p1 iota(z)(alpha) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(alpha))
14. v : Cname
15. ¬(v ∈ K)
16. ∀z:Cname. rename-one-name(z;z) = 1 ∈ name-morph([z / K];[z / K]) supposing ¬(z ∈ K)
17. ((p1 iota(z)(alpha) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(alpha)) f[z1:=v])
= (p1 iota(z)(alpha) (rename-one-name(z;z1) o f[z1:=v]))
∈ A((rename-one-name(z;z1) o f[z1:=v])(iota(z)(alpha)))
⊢ f[z:=v] = (rename-one-name(z;z1) o f[z1:=v]) ∈ name-morph([z / I];[v / K])

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  I  :  Cname  List
6.  K  :  Cname  List
7.  f  :  name-morph(I;K)
8.  alpha  :  X(I)
9.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
10.  p1  :  named-path(X;A;a;b;I;alpha;z)
11.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
12.  q1  :  named-path(X;A;a;b;I;alpha;z1)
13.  (p1  iota(z)(alpha)  rename-one-name(z;z1))  =  q1
14.  v  :  Cname
15.  \mneg{}(v  \mmember{}  K)
16.  \mforall{}z:Cname.  rename-one-name(z;z)  =  1  supposing  \mneg{}(z  \mmember{}  K)
\mvdash{}  (p1  iota(z)(alpha)  f[z:=v])  =  ((p1  iota(z)(alpha)  rename-one-name(z;z1))  iota(z1)(alpha)  f[z1:=v])


By

---

Latex:
((InstLemma  `cubical-type-ap-morph-comp`
          [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[z  /  I]\mkleeneclose{};\mkleeneopen{}[z1  /  I]\mkleeneclose{};\mkleeneopen{}[v  /  K]\mkleeneclose{};\mkleeneopen{}rename-one-name(z;z1)\mkleeneclose{};\mkleeneopen{}f[z1:=v]\mkleeneclose{};\mkleeneopen{}iota(z)(alpha)\mkleeneclose{};
    \mkleeneopen{}p1\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (Symmetry  THEN  NthHypEq  (-1)  THEN  EqCD  THEN  Auto)
  )

---

Home Index