---

Step * 1 1 1 1 of Lemma cubical-pi_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : X(I)
8. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))
9. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:A(f(a)).
     ((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)) ∈ B(g((f(a);u))))
10. H : Cname List
11. K : Cname List
12. h : name-morph(J;H)
13. g : name-morph(H;K)
14. u : A(h(f(a)))
15. (w H (f o h) u ((f o h)(a);u) g) = (w K ((f o h) o g) (u (f o h)(a) g)) ∈ B(g(((f o h)(a);u)))
16. (f o h)(a) = h(f(a)) ∈ X(H)
17. (f o (h o g)) = ((f o h) o g) ∈ name-morph(I;K)
⊢ True
BY
{ Assert ⌜B(((f o (h o g))(a);(u h(f(a)) g))) = B(g((h(f(a));u))) ∈ Type⌝⋅ }

1
.....assertion..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : X(I)
8. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))
9. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:A(f(a)).
     ((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)) ∈ B(g((f(a);u))))
10. H : Cname List
11. K : Cname List
12. h : name-morph(J;H)
13. g : name-morph(H;K)
14. u : A(h(f(a)))
15. (w H (f o h) u ((f o h)(a);u) g) = (w K ((f o h) o g) (u (f o h)(a) g)) ∈ B(g(((f o h)(a);u)))
16. (f o h)(a) = h(f(a)) ∈ X(H)
17. (f o (h o g)) = ((f o h) o g) ∈ name-morph(I;K)
⊢ B(((f o (h o g))(a);(u h(f(a)) g))) = B(g((h(f(a));u))) ∈ Type

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : X(I)
8. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))
9. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:A(f(a)).
     ((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)) ∈ B(g((f(a);u))))
10. H : Cname List
11. K : Cname List
12. h : name-morph(J;H)
13. g : name-morph(H;K)
14. u : A(h(f(a)))
15. (w H (f o h) u ((f o h)(a);u) g) = (w K ((f o h) o g) (u (f o h)(a) g)) ∈ B(g(((f o h)(a);u)))
16. (f o h)(a) = h(f(a)) ∈ X(H)
17. (f o (h o g)) = ((f o h) o g) ∈ name-morph(I;K)
18. B(((f o (h o g))(a);(u h(f(a)) g))) = B(g((h(f(a));u))) ∈ Type
⊢ True

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  I  :  Cname  List
5.  J  :  Cname  List
6.  f  :  name-morph(I;J)
7.  a  :  X(I)
8.  w  :  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  u:A(f(a))  {}\mrightarrow{}  B((f(a);u))
9.  \mforall{}J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}u:A(f(a)).
          ((w  J  f  u  (f(a);u)  g)  =  (w  K  (f  o  g)  (u  f(a)  g)))
10.  H  :  Cname  List
11.  K  :  Cname  List
12.  h  :  name-morph(J;H)
13.  g  :  name-morph(H;K)
14.  u  :  A(h(f(a)))
15.  (w  H  (f  o  h)  u  ((f  o  h)(a);u)  g)  =  (w  K  ((f  o  h)  o  g)  (u  (f  o  h)(a)  g))
16.  (f  o  h)(a)  =  h(f(a))
17.  (f  o  (h  o  g))  =  ((f  o  h)  o  g)
\mvdash{}  True


By

---

Latex:
Assert  \mkleeneopen{}B(((f  o  (h  o  g))(a);(u  h(f(a))  g)))  =  B(g((h(f(a));u)))\mkleeneclose{}\mcdot{}

---

Home Index