---

Step * of Lemma I-path-morph_functionality

∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I).
∀p,q:I-path(X;A;a;b;I;alpha).
  (path-eq(X;A;I;alpha;p;q) ⇒ path-eq(X;A;K;f(alpha);I-path-morph(X;A;I;K;f;alpha;p);I-path-morph(X;A;I;K;f;alpha;q)))
BY
{ (Auto
   THEN D -3
   THEN D -2
   THEN RepUR ``I-path-morph path-eq named-path-morph`` 0
   THEN RepUR ``path-eq`` -1
   THEN (GenConclTerm ⌜fresh-cname(K)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (InstLemma `rename-one-same` [⌜K⌝]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

1
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]) iota(v)(f(alpha)) 1) = (q1 iota(z1)(alpha) f[z1:=v]) ∈ A(iota(v)(f(alpha)))

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.  \mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}alpha:X(I).
\mforall{}p,q:I-path(X;A;a;b;I;alpha).
    (path-eq(X;A;I;alpha;p;q)
    {}\mRightarrow{}  path-eq(X;A;K;f(alpha);I-path-morph(X;A;I;K;f;alpha;p);I-path-morph(X;A;I;K;f;alpha;q)))


By

---

Latex:
(Auto
  THEN  D  -3
  THEN  D  -2
  THEN  RepUR  ``I-path-morph  path-eq  named-path-morph``  0
  THEN  RepUR  ``path-eq``  -1
  THEN  (GenConclTerm  \mkleeneopen{}fresh-cname(K)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (InstLemma  `rename-one-same`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index