---

Step * 1 1 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. 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)))
BY
{ Assert ⌜(((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1]) iota(v1)(f(alpha)) rename-one-name(v1;v1))
          = ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
          ∈ A(iota(v1)(f(alpha)))⌝⋅ }

1
.....assertion..... 
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 I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
∈ A(iota(v1)(f(alpha)))

2
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)} 
12. (((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1]) iota(v1)(f(alpha)) rename-one-name(v1;v1))
= ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
∈ A(iota(v1)(f(alpha)))
⊢ (((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:

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.  alpha  :  X(I)
8.  v  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
9.  fresh-cname(I)  =  v
10.  v1  :  \{x:Cname|  \mneg{}(x  \mmember{}  J)\} 
11.  fresh-cname(J)  =  v1
\mvdash{}  (((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))


By

---

Latex:
Assert 
\mkleeneopen{}(((a  I  alpha  alpha  iota(v))  iota(v)(alpha)  f[v:=v1])  iota(v1)(f(alpha))  rename-one-name(v1;v1))
  =  ((a  I  alpha  alpha  iota(v))  iota(v)(alpha)  f[v:=v1])\mkleeneclose{}\mcdot{}

---

Home Index