---

Step * 1 1 1 2 1 1 of Lemma cubical-refl_wf

.....subterm..... T:t
3:n
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)))
13. ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
= (a I alpha alpha (iota(v) o f[v:=v1]))
∈ A((iota(v) o f[v:=v1])(alpha))
⊢ (a J f(alpha) f(alpha) iota(v1)) = (a I alpha alpha (iota(v) o f[v:=v1])) ∈ A(iota(v1)(f(alpha)))
BY
{ TACTIC:((Assert X ⊢ A BY
                 Auto)
          THEN RepeatFor 2 (DVar `A')
          THEN DVar `a'
          THEN RepUR ``cubical-type-ap-morph`` 0
          THEN All Reduce) }

1
1. X : CubicalSet
2. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
3. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
4. (∀I:Cname List. ∀a:X(I). ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
     ((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a))))
5. a : I:(Cname List) ⟶ a:X(I) ⟶ (A1 I a)
6. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a@0:X(I).  ((A2 I J f a@0 (a I a@0)) = (a J f(a@0)) ∈ (A1 J f(a@0)))
7. I : Cname List
8. J : Cname List
9. f : name-morph(I;J)
10. alpha : X(I)
11. v : {x:Cname| ¬(x ∈ I)} 
12. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)} 
13. v1 : {x:Cname| ¬(x ∈ J)} 
14. fresh-cname(J) = v1 ∈ {x:Cname| ¬(x ∈ J)} 
15. (((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])
∈ <A1, A2>(iota(v1)(f(alpha)))
16. ((a I alpha alpha iota(v)) iota(v)(alpha) f[v:=v1])
= (a I alpha alpha (iota(v) o f[v:=v1]))
∈ <A1, A2>((iota(v) o f[v:=v1])(alpha))
17. X ⊢ <A1, A2>
⊢ (A2 J [v1 / J] iota(v1) f(alpha) (a J f(alpha)))
= (A2 I [v1 / J] (iota(v) o f[v:=v1]) alpha (a I alpha))
∈ <A1, A2>(iota(v1)(f(alpha)))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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
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])
13.  ((a  I  alpha  alpha  iota(v))  iota(v)(alpha)  f[v:=v1])  =  (a  I  alpha  alpha  (iota(v)  o  f[v:=v1]))
\mvdash{}  (a  J  f(alpha)  f(alpha)  iota(v1))  =  (a  I  alpha  alpha  (iota(v)  o  f[v:=v1]))


By

---

Latex:
TACTIC:((Assert  X  \mvdash{}  A  BY
                              Auto)
                THEN  RepeatFor  2  (DVar  `A')
                THEN  DVar  `a'
                THEN  RepUR  ``cubical-type-ap-morph``  0
                THEN  All  Reduce)

---

Home Index