---

Step * of Lemma cubical-type-ap-rename-one-equal

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[x,y:Cname]. ∀[a:X([x / I])]. ∀[u,v:A(a)].
  u = v ∈ A(a) ⇐⇒ (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a)) 
  supposing (¬(y ∈ I)) ∧ (¬(x ∈ I))
BY
{ (Auto THEN Assert ⌜(rename-one-name(x;y) o rename-one-name(y;x)) = 1 ∈ name-morph([x / I];[x / I])⌝⋅) }

1
.....assertion..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. x : Cname
5. y : Cname
6. a : X([x / I])
7. u : A(a)
8. v : A(a)
9. ¬(y ∈ I)
10. ¬(x ∈ I)
11. (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a))
⊢ (rename-one-name(x;y) o rename-one-name(y;x)) = 1 ∈ name-morph([x / I];[x / I])

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. x : Cname
5. y : Cname
6. a : X([x / I])
7. u : A(a)
8. v : A(a)
9. ¬(y ∈ I)
10. ¬(x ∈ I)
11. (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a))
12. (rename-one-name(x;y) o rename-one-name(y;x)) = 1 ∈ name-morph([x / I];[x / I])
⊢ u = v ∈ A(a)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I:Cname  List].  \mforall{}[x,y:Cname].  \mforall{}[a:X([x  /  I])].  \mforall{}[u,v:A(a)].
    u  =  v  \mLeftarrow{}{}\mRightarrow{}  (u  a  rename-one-name(x;y))  =  (v  a  rename-one-name(x;y)) 
    supposing  (\mneg{}(y  \mmember{}  I))  \mwedge{}  (\mneg{}(x  \mmember{}  I))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}(rename-one-name(x;y)  o  rename-one-name(y;x))  =  1\mkleeneclose{}\mcdot{})

---

Home Index