---

Step * 1 of Lemma named-path-morph_wf


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 : Cname
10. ¬(z ∈ I)
11. w : A(iota(z)(alpha))
12. name-path-endpoints(X;A;a;b;I;alpha;z;w)
13. x : Cname
14. ¬(x ∈ K)
⊢ named-path-morph(X;A;I;K;z;x;f;alpha;w) ∈ A(iota(x)(f(alpha)))
BY
{ (RepUR ``named-path-morph`` 0 THEN InferEqualType) }

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 : Cname
10. ¬(z ∈ I)
11. w : A(iota(z)(alpha))
12. name-path-endpoints(X;A;a;b;I;alpha;z;w)
13. x : Cname
14. ¬(x ∈ K)
⊢ A(f[z:=x](iota(z)(alpha))) = A(iota(x)(f(alpha))) ∈ Type

2
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 : Cname
10. ¬(z ∈ I)
11. w : A(iota(z)(alpha))
12. name-path-endpoints(X;A;a;b;I;alpha;z;w)
13. x : Cname
14. ¬(x ∈ K)
15. A(f[z:=x](iota(z)(alpha))) = A(iota(x)(f(alpha))) ∈ Type
⊢ (w iota(z)(alpha) f[z:=x]) ∈ A(f[z:=x](iota(z)(alpha)))

---

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  :  Cname
10.  \mneg{}(z  \mmember{}  I)
11.  w  :  A(iota(z)(alpha))
12.  name-path-endpoints(X;A;a;b;I;alpha;z;w)
13.  x  :  Cname
14.  \mneg{}(x  \mmember{}  K)
\mvdash{}  named-path-morph(X;A;I;K;z;x;f;alpha;w)  \mmember{}  A(iota(x)(f(alpha)))


By

---

Latex:
(RepUR  ``named-path-morph``  0  THEN  InferEqualType)

---

Home Index