---

Step * 1 1 of Lemma set-path-name_wf


1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. alpha : X(I)@i
7. I-path(X;A;a;b;I;alpha) ⊆r cubical-path(X;A;a;b;I;alpha)
8. x : {x:Cname| ¬(x ∈ I)} 
9. named-path(X;A;a;b;I;1(alpha);x) ⊆r A(iota(x)(alpha))
10. p : cubical-path(X;A;a;b;I;alpha)@i
⊢ set-path-name(X;A;I;alpha;x;p) ∈ {q:I-path(X;A;a;b;I;alpha)| 
                                    ((fst(q)) = x ∈ Cname) ∧ (q = p ∈ cubical-path(X;A;a;b;I;alpha))} 
BY
{ TACTIC:MemTypeCD }

1
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. alpha : X(I)@i
7. I-path(X;A;a;b;I;alpha) ⊆r cubical-path(X;A;a;b;I;alpha)
8. x : {x:Cname| ¬(x ∈ I)} 
9. named-path(X;A;a;b;I;1(alpha);x) ⊆r A(iota(x)(alpha))
10. p : cubical-path(X;A;a;b;I;alpha)@i
⊢ set-path-name(X;A;I;alpha;x;p) ∈ I-path(X;A;a;b;I;alpha)

2
.....set predicate..... 
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. alpha : X(I)@i
7. I-path(X;A;a;b;I;alpha) ⊆r cubical-path(X;A;a;b;I;alpha)
8. x : {x:Cname| ¬(x ∈ I)} 
9. named-path(X;A;a;b;I;1(alpha);x) ⊆r A(iota(x)(alpha))
10. p : cubical-path(X;A;a;b;I;alpha)@i
⊢ ((fst(set-path-name(X;A;I;alpha;x;p))) = x ∈ Cname)
∧ (set-path-name(X;A;I;alpha;x;p) = p ∈ cubical-path(X;A;a;b;I;alpha))

3
.....wf..... 
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. alpha : X(I)@i
7. I-path(X;A;a;b;I;alpha) ⊆r cubical-path(X;A;a;b;I;alpha)
8. x : {x:Cname| ¬(x ∈ I)} 
9. named-path(X;A;a;b;I;1(alpha);x) ⊆r A(iota(x)(alpha))
10. p : cubical-path(X;A;a;b;I;alpha)@i
11. q : I-path(X;A;a;b;I;alpha)
⊢ ((fst(q)) = x ∈ Cname) ∧ (q = p ∈ cubical-path(X;A;a;b;I;alpha)) ∈ Type

---

Latex:

---

Latex:

1.  X  :  CubicalSet@i'
2.  A  :  \{X  \mvdash{}  \_\}@i'
3.  a  :  \{X  \mvdash{}  \_:A\}@i
4.  b  :  \{X  \mvdash{}  \_:A\}@i
5.  I  :  Cname  List@i
6.  alpha  :  X(I)@i
7.  I-path(X;A;a;b;I;alpha)  \msubseteq{}r  cubical-path(X;A;a;b;I;alpha)
8.  x  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
9.  named-path(X;A;a;b;I;1(alpha);x)  \msubseteq{}r  A(iota(x)(alpha))
10.  p  :  cubical-path(X;A;a;b;I;alpha)@i
\mvdash{}  set-path-name(X;A;I;alpha;x;p)  \mmember{}  \{q:I-path(X;A;a;b;I;alpha)|  ((fst(q))  =  x)  \mwedge{}  (q  =  p)\} 


By

---

Latex:
TACTIC:MemTypeCD

---

Home Index