---

Step * of Lemma named-path-morph_wf

∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I). ∀z:{z:Cname| ¬(z ∈ I)} .
∀w:named-path(X;A;a;b;I;alpha;z). ∀x:{x:Cname| ¬(x ∈ K)} .
  (named-path-morph(X;A;I;K;z;x;f;alpha;w) ∈ named-path(X;A;a;b;K;f(alpha);x))
BY
{ (Auto THEN D -2 THEN DSetVars THEN MemTypeCD) }

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)
⊢ named-path-morph(X;A;I;K;z;x;f;alpha;w) ∈ A(iota(x)(f(alpha)))

2
.....set predicate..... 
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)
⊢ name-path-endpoints(X;A;a;b;K;f(alpha);x;named-path-morph(X;A;I;K;z;x;f;alpha;w))

3
.....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)
15. omega : A(iota(x)(f(alpha)))
⊢ name-path-endpoints(X;A;a;b;K;f(alpha);x;omega) ∈ Type

---

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{}z:\{z:Cname|  \mneg{}(z  \mmember{}  I)\}  .  \mforall{}w:named-path(X;A;a;b;I;alpha;z).  \mforall{}x:\{x:Cname|  \mneg{}(x  \mmember{}  K)\}  .
    (named-path-morph(X;A;I;K;z;x;f;alpha;w)  \mmember{}  named-path(X;A;a;b;K;f(alpha);x))


By

---

Latex:
(Auto  THEN  D  -2  THEN  DSetVars  THEN  MemTypeCD)

---

Home Index