---

Step * 1 of Lemma refl-path_wf

.....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)))
BY
{ TACTIC:(D 0
          THEN  Fold `iota\'` 0
          THEN (Subst' [fresh-cname(I) / I] ~ I+ 0
                THENA (Unfold `add-fresh-cname` 0 THEN CallByValueReduce 0 THEN Auto)
                )
          THEN RWO "cubical-type-ap-morph-comp" 0
          THEN Auto) }

---

Latex:

---

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


By

---

Latex:
TACTIC:(D  0
                THEN    Fold  `iota\mbackslash{}'`  0
                THEN  (Subst'  [fresh-cname(I)  /  I]  \msim{}  I+  0
                            THENA  (Unfold  `add-fresh-cname`  0  THEN  CallByValueReduce  0  THEN  Auto)
                            )
                THEN  RWO  "cubical-type-ap-morph-comp"  0
                THEN  Auto)

---

Home Index