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 -3
   THEN -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 -1
   THEN (InstLemma `rename-one-same` [⌜K⌝]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

1
1. CubicalSet
2. {X ⊢ _}
3. {X ⊢ _:A}
4. {X ⊢ _:A}
5. Cname List
6. Cname List
7. name-morph(I;K)
8. alpha X(I)
9. {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. 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