---

Step * of Lemma I-path-morph-comp

No Annotations
∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀alpha:X(I).
∀u:cubical-path(X;A;a;b;I;alpha).
  (I-path-morph(X;A;I;K;(f o g);alpha;u)
  = I-path-morph(X;A;J;K;g;f(alpha);I-path-morph(X;A;I;J;f;alpha;u))
  ∈ cubical-path(X;A;a;b;K;(f o g)(alpha)))
BY
{ (Auto
   THEN quotD (-1)
   THEN EqTypeCD
   THEN Auto
   THEN D -3
   THEN D -2
   THEN RepUR ``path-eq`` -1
   THEN RepUR ``path-eq I-path-morph named-path-morph`` 0
   THEN (GenConclTerm ⌜fresh-cname(K)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (GenConclTerm ⌜fresh-cname(J)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. alpha : X(I)
11. z : {z:Cname| ¬(z ∈ I)} 
12. u2 : named-path(X;A;a;b;I;alpha;z)
13. z1 : {z:Cname| ¬(z ∈ I)} 
14. u3 : named-path(X;A;a;b;I;alpha;z1)
15. (u2 iota(z)(alpha) rename-one-name(z;z1)) = u3 ∈ A(iota(z1)(alpha))
16. v : Cname
17. ¬(v ∈ K)
18. v1 : Cname
19. ¬(v1 ∈ J)
⊢ ((u2 iota(z)(alpha) (f o g)[z:=v]) iota(v)((f o g)(alpha)) rename-one-name(v;v))
= ((u3 iota(z1)(alpha) f[z1:=v1]) iota(v1)(f(alpha)) g[v1:=v])
∈ A(iota(v)((f o g)(alpha)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).
\mforall{}g:name-morph(J;K).  \mforall{}alpha:X(I).  \mforall{}u:cubical-path(X;A;a;b;I;alpha).
    (I-path-morph(X;A;I;K;(f  o  g);alpha;u)
    =  I-path-morph(X;A;J;K;g;f(alpha);I-path-morph(X;A;I;J;f;alpha;u)))


By

---

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

---

Home Index