---

Step * of Lemma refl-path_wf

∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:X(I).  (refl-path(A;a;I;alpha) ∈ I-path(X;A;a;a;I;alpha))
BY
{ (ProveWfLemma
   THEN Unfold `named-path` 0
   THEN MemTypeCD
   THEN Auto
   THEN Try ((InferEqualType
              THEN Auto
              THEN (Subst' [fresh-cname(I) / I] ~ I+ 0
                    THENA (Unfold `add-fresh-cname` 0 THEN CallByValueReduce 0 THEN Auto)
                    )
              THEN Complete (Auto)))) }

1
.....set predicate..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. I : Cname List
5. alpha : X(I)
⊢ name-path-endpoints(X;A;a;a;I;alpha;fresh-cname(I);(a I alpha alpha iota'(I)))

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a:\{X  \mvdash{}  \_:A\}.  \mforall{}I:Cname  List.  \mforall{}alpha:X(I).
    (refl-path(A;a;I;alpha)  \mmember{}  I-path(X;A;a;a;I;alpha))


By

---

Latex:
(ProveWfLemma
  THEN  Unfold  `named-path`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((InferEqualType
                        THEN  Auto
                        THEN  (Subst'  [fresh-cname(I)  /  I]  \msim{}  I+  0
                                    THENA  (Unfold  `add-fresh-cname`  0  THEN  CallByValueReduce  0  THEN  Auto)
                                    )
                        THEN  Complete  (Auto))))

---

Home Index