---

Step * 1 1 2 2 1 2 1 3 of Lemma cubical-id-box_wf

.....subterm..... T:t
3:n
1. I : Cname List
2. c : ℕ2
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. x1 : nameset(I)
14. i1 : ℕ2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
16. ¬(fresh-cname(I) = x1 ∈ Cname)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I))
∧ (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I))
⊢ (a(alpha) (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) (x1:=i1))
= (a I-[x1] (x1:=i1)(alpha))
∈ A(((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha)))
BY
{ (InstLemma `cubical-type-ap-morph-comp` [⌜X⌝;⌜A⌝]⋅ THENA Auto) }

1
1. I : Cname List
2. c : ℕ2
3. X : CubicalSet
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. alpha : X(I)
11. ¬(fresh-cname(I) ∈ J)
12. ¬(x = fresh-cname(I) ∈ Cname)
13. x1 : nameset(I)
14. i1 : ℕ2
15. ((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
= (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
∈ X([fresh-cname(I) / I]-[fresh-cname(I); x1])
16. ¬(fresh-cname(I) = x1 ∈ Cname)
17. v2 : A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18. (v2 iota(fresh-cname(I))((x1:=i1)(alpha)) (fresh-cname(I):=c)) = (a I-[x1] (x1:=i1)(alpha)) ∈ A((x1:=i1)(alpha))
19. [fresh-cname(I) / I]-[x1] = [fresh-cname(I) / I-[x1]] ∈ (Cname List)
20. [fresh-cname(I) / I]-[fresh-cname(I); x1] = I-[x1] ∈ (Cname List)
21. ((iota(fresh-cname(I)) o (fresh-cname(I):=c)) = 1 ∈ name-morph(I;I))
∧ (alpha = (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) ∈ X(I))
22. ∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)]. ∀[a:X(I)]. ∀[u:A(a)].
      (((u a f) f(a) g) = (u a (f o g)) ∈ A((f o g)(a)))
⊢ (a(alpha) (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)) (x1:=i1))
= (a I-[x1] (x1:=i1)(alpha))
∈ A(((x1:=i1) o (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha)))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  I  :  Cname  List
2.  c  :  \mBbbN{}2
3.  X  :  CubicalSet
4.  A  :  \{X  \mvdash{}  \_\}
5.  a  :  \{X  \mvdash{}  \_:A\}
6.  b  :  \{X  \mvdash{}  \_:A\}
7.  J  :  nameset(I)  List
8.  x  :  nameset(I)
9.  i  :  \mBbbN{}2
10.  alpha  :  X(I)
11.  \mneg{}(fresh-cname(I)  \mmember{}  J)
12.  \mneg{}(x  =  fresh-cname(I))
13.  x1  :  nameset(I)
14.  i1  :  \mBbbN{}2
15.  ((x1:=i1)  o  (fresh-cname(I):=c))(iota(fresh-cname(I))(alpha))
=  (x1:=i1)((fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
16.  \mneg{}(fresh-cname(I)  =  x1)
17.  v2  :  A(iota(fresh-cname(I))((x1:=i1)(alpha)))
18.  (v2  iota(fresh-cname(I))((x1:=i1)(alpha))  (fresh-cname(I):=c))  =  (a  I-[x1]  (x1:=i1)(alpha))
19.  [fresh-cname(I)  /  I]-[x1]  =  [fresh-cname(I)  /  I-[x1]]
20.  [fresh-cname(I)  /  I]-[fresh-cname(I);  x1]  =  I-[x1]
21.  ((iota(fresh-cname(I))  o  (fresh-cname(I):=c))  =  1)
\mwedge{}  (alpha  =  (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha)))
\mvdash{}  (a(alpha)  (fresh-cname(I):=c)(iota(fresh-cname(I))(alpha))  (x1:=i1))  =  (a  I-[x1]  (x1:=i1)(alpha))


By

---

Latex:
(InstLemma  `cubical-type-ap-morph-comp`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index