---

Step * 1 1 1 1 of Lemma cubical-refl_wf

.....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)))
BY
{ (BLemma `cubical-type-ap-morph-id` THEN 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)} 
⊢ rename-one-name(v1;v1) = 1 ∈ name-morph([v1 / J];[v1 / J])

---

Latex:

---

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


By

---

Latex:
(BLemma  `cubical-type-ap-morph-id`  THEN  Auto)

---

Home Index