---

Step * 1 1 of Lemma cubical-refl_wf

.....antecedent..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a@0 : X(I)
⊢ path-eq(X;A;J;f(a@0);I-path-morph(X;A;I;J;f;a@0;refl-path(A;a;I;a@0));refl-path(A;a;J;f(a@0)))
BY
{ (RenameVar `alpha' (-1)
   THEN RepUR ``I-path-morph path-eq refl-path named-path-morph iota\' add-fresh-cname`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (GenConclTerm ⌜fresh-cname(I)⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜fresh-cname(J)⌝⋅ THENA Auto)) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. alpha : X(I)
8. v : {x:Cname| ¬(x ∈ I)} 
9. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
10. v1 : {x:Cname| ¬(x ∈ J)} 
11. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)} 
⊢ (((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1]) iota(v1)(f(alpha)) rename-one-name(v1;v1))
= (a J f(alpha) f(alpha) iota(v1))
∈ A(iota(v1)(f(alpha)))

---

Latex:

---

Latex:
.....antecedent..... 
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  I  :  Cname  List
5.  J  :  Cname  List
6.  f  :  name-morph(I;J)
7.  a@0  :  X(I)
\mvdash{}  path-eq(X;A;J;f(a@0);I-path-morph(X;A;I;J;f;a@0;refl-path(A;a;I;a@0));refl-path(A;a;J;f(a@0)))


By

---

Latex:
(RenameVar  `alpha'  (-1)
  THEN  RepUR  ``I-path-morph  path-eq  refl-path  named-path-morph  iota\mbackslash{}'  add-fresh-cname``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}fresh-cname(I)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}fresh-cname(J)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index