---

Step * 1 of Lemma cubical-refl_wf


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)
⊢ 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)) ∈ cubical-path(X;A;a;a;J;f(a@0))
BY
{ (EqTypeCD THEN Auto) }

1
.....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)))

---

Latex:

---

Latex:

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{}  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:
(EqTypeCD  THEN  Auto)

---

Home Index