---

Step * of Lemma set-path-name_wf

No Annotations
∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:X(I).
  ∀[x:{x:Cname| ¬(x ∈ I)} ]
    ∀p:(Id_A a b)(alpha)
      (set-path-name(X;A;I;alpha;x;p) ∈ {q:I-path(X;A;a;b;I;alpha)| 
                                         ((fst(q)) = x ∈ Cname) ∧ (q = p ∈ (Id_A a b)(alpha))} )
BY
{ (Auto
   THEN (Assert I-path(X;A;a;b;I;alpha) ⊆r cubical-path(X;A;a;b;I;alpha) BY
               (Unfold `cubical-path` 0 THEN BLemma `subtype_quotient` THEN Auto))
   THEN PromoteHyp (-1) (-3)
   THEN (Assert ⌜named-path(X;A;a;b;I;1(alpha);x) ⊆r A(iota(x)(alpha))⌝⋅
         THENA (Subst' 1(alpha) = alpha ∈ X(I) 0 THEN Auto)
         )
   THEN PromoteHyp (-1) (-2)) }

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 : (Id_A a b)(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 ∈ (Id_A a b)(alpha))} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.  \mforall{}I:Cname  List.  \mforall{}alpha:X(I).
    \mforall{}[x:\{x:Cname|  \mneg{}(x  \mmember{}  I)\}  ]
        \mforall{}p:(Id\_A  a  b)(alpha)
            (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:
(Auto
  THEN  (Assert  I-path(X;A;a;b;I;alpha)  \msubseteq{}r  cubical-path(X;A;a;b;I;alpha)  BY
                          (Unfold  `cubical-path`  0  THEN  BLemma  `subtype\_quotient`  THEN  Auto))
  THEN  PromoteHyp  (-1)  (-3)
  THEN  (Assert  \mkleeneopen{}named-path(X;A;a;b;I;1(alpha);x)  \msubseteq{}r  A(iota(x)(alpha))\mkleeneclose{}\mcdot{}
              THENA  (Subst'  1(alpha)  =  alpha  0  THEN  Auto)
              )
  THEN  PromoteHyp  (-1)  (-2))

---

Home Index