---

Step * of Lemma path-eq-equiv

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)].
  EquivRel(I-path(X;A;a;b;I;alpha);p,q.path-eq(X;A;I;alpha;p;q))
BY
{ (Intros
   THEN Unfold `I-path` 0
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN DProds
   THEN DSetVars
   THEN All (RepUR ``path-eq``)
   THEN Auto
   THEN Try ((BLemma `cubical-type-ap-morph-id` THEN Auto))) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. z : Cname
8. ¬(z ∈ I)
9. a2 : named-path(X;A;a;b;I;alpha;z)
⊢ rename-one-name(z;z) = 1 ∈ name-morph([z / I];[z / I])

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. z1 : Cname
8. ¬(z1 ∈ I)
9. a1 : named-path(X;A;a;b;I;alpha;z1)
10. z : Cname
11. ¬(z ∈ I)
12. b2 : named-path(X;A;a;b;I;alpha;z)
13. (a1 iota(z1)(alpha) rename-one-name(z1;z)) = b2 ∈ A(iota(z)(alpha))
⊢ (b2 iota(z)(alpha) rename-one-name(z;z1)) = a1 ∈ A(iota(z1)(alpha))

3
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. Sym(z:{z:Cname| ¬(z ∈ I)}  × named-path(X;A;a;b;I;alpha;z);p,q.let z,w = p 
                                                        in let z',w' = q 
                                                           in (w iota(z)(alpha) rename-one-name(z;z'))
                                                              = w'
                                                              ∈ A(iota(z')(alpha)))
8. z2 : Cname
9. ¬(z2 ∈ I)
10. a1 : named-path(X;A;a;b;I;alpha;z2)
11. z1 : Cname
12. ¬(z1 ∈ I)
13. b1 : named-path(X;A;a;b;I;alpha;z1)
14. z : Cname
15. ¬(z ∈ I)
16. c1 : named-path(X;A;a;b;I;alpha;z)
17. (a1 iota(z2)(alpha) rename-one-name(z2;z1)) = b1 ∈ A(iota(z1)(alpha))
18. (b1 iota(z1)(alpha) rename-one-name(z1;z)) = c1 ∈ A(iota(z)(alpha))
⊢ (a1 iota(z2)(alpha) rename-one-name(z2;z)) = c1 ∈ A(iota(z)(alpha))

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].
    EquivRel(I-path(X;A;a;b;I;alpha);p,q.path-eq(X;A;I;alpha;p;q))


By

---

Latex:
(Intros
  THEN  Unfold  `I-path`  0
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  DProds
  THEN  DSetVars
  THEN  All  (RepUR  ``path-eq``)
  THEN  Auto
  THEN  Try  ((BLemma  `cubical-type-ap-morph-id`  THEN  Auto)))

---

Home Index