Proof of Nuprl Lemma : cubical-pi-family-comp

Step * 1 of Lemma cubical-pi-family-comp

1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : Delta(I)
8. A1 : I:(Cname List) ⟶ X(I) ⟶ Type

9. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))

10. (∀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))))
11. A : I:(Cname List) ⟶ X.<A1, A2>(I) ⟶ Type

12. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A I a) ⟶ (A J f(a))

⊢ (B1 H K g ((s)h(f(a));u) (w H (f o h) u)) = (w K (f o (h o g)) (A2 H K g (s)h(f(a)) u)) ∈ <A, B1>(g(((s)h(f(a));u)))

BY
{ xxx((InstHyp [⌜H⌝;⌜K⌝;⌜(f o h)⌝;⌜g⌝;⌜u⌝] (-7)⋅ THENA Auto)
      THEN RepUR ``cubical-type-ap-morph`` -1
      THEN NthHypEq (-1)
      THEN EqCD)xxx }

1
.....subterm..... T:t
1:n
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : Delta(I)
8. A1 : I:(Cname List) ⟶ X(I) ⟶ Type

9. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))

12. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A I a) ⟶ (A J f(a))

13. (∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A I a.  ((B1 I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X.<A1, A2>(I). ∀u:A I a.
     ((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u)) ∈ (A K (f o g)(a))))
14. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:<A1, A2>(f((s)a)) ⟶ <A, B1>((f((s)a);u))
15. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:<A1, A2>(f((s)a)).
      ((w J f u (f((s)a);u) g) = (w K (f o g) (u f((s)a) g)) ∈ <A, B1>(g((f((s)a);u))))
16. H : Cname List
17. K : Cname List
18. h : name-morph(J;H)
19. g : name-morph(H;K)
20. u : <A1, A2>(h((s)f(a)))
21. X ⊢ <A1, A2> ∧ X.<A1, A2> ⊢ <A, B1>
22. (B1 H K g ((f o h)((s)a);u) (w H (f o h) u))
= (w K ((f o h) o g) (A2 H K g (f o h)((s)a) u))
∈ <A, B1>(g(((f o h)((s)a);u)))
⊢ <A, B1>(g(((s)h(f(a));u))) = <A, B1>(g(((f o h)((s)a);u))) ∈ Type

2
.....subterm..... T:t
2:n
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : Delta(I)
8. A1 : I:(Cname List) ⟶ X(I) ⟶ Type

9. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))

12. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A I a) ⟶ (A J f(a))

⊢ (B1 H K g ((s)h(f(a));u) (w H (f o h) u)) = (B1 H K g ((f o h)((s)a);u) (w H (f o h) u)) ∈ <A, B1>(g(((s)h(f(a));u)))

3
.....subterm..... T:t
3:n
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : Delta(I)
8. A1 : I:(Cname List) ⟶ X(I) ⟶ Type

9. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))

12. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A I a) ⟶ (A J f(a))

13. (∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A I a.  ((B1 I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X.<A1, A2>(I). ∀u:A I a.
     ((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u)) ∈ (A K (f o g)(a))))
14. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:<A1, A2>(f((s)a)) ⟶ <A, B1>((f((s)a);u))
15. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:<A1, A2>(f((s)a)).
      ((w J f u (f((s)a);u) g) = (w K (f o g) (u f((s)a) g)) ∈ <A, B1>(g((f((s)a);u))))
16. H : Cname List
17. K : Cname List
18. h : name-morph(J;H)
19. g : name-morph(H;K)
20. u : <A1, A2>(h((s)f(a)))
21. X ⊢ <A1, A2> ∧ X.<A1, A2> ⊢ <A, B1>
22. (B1 H K g ((f o h)((s)a);u) (w H (f o h) u))
= (w K ((f o h) o g) (A2 H K g (f o h)((s)a) u))
∈ <A, B1>(g(((f o h)((s)a);u)))
⊢ (w K (f o (h o g)) (A2 H K g (s)h(f(a)) u))
= (w K ((f o h) o g) (A2 H K g (f o h)((s)a) u))
∈ <A, B1>(g(((s)h(f(a));u)))

4
.....antecedent.....
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : Delta(I)
8. A1 : I:(Cname List) ⟶ X(I) ⟶ Type

9. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))

12. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A I a) ⟶ (A J f(a))

Latex:

Latex:
1. X : CubicalSet 2. Delta : CubicalSet 3. s : Delta {}\mrightarrow{} X 4. I : Cname List 5. J : Cname List 6. f : name-morph(I;J) 7. a : Delta(I) 8. A1 : I:(Cname List) {}\mrightarrow{} X(I) {}\mrightarrow{} Type 9. A2 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} a:X(I) {}\mrightarrow{} (A1 I a) {}\mrightarrow{} (A1 J f(a)) 10. (\mforall{}I:Cname List. \mforall{}a:X(I). \mforall{}u:A1 I a. ((A2 I I 1 a u) = u)) \mwedge{} (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K). \mforall{}a:X(I). \mforall{}u:A1 I a. ((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)))) 11. A : I:(Cname List) {}\mrightarrow{} X.<A1, A2>(I) {}\mrightarrow{} Type 12. B1 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} a:X.<A1, A2>(I) {}\mrightarrow{} (A I a) {}\mrightarrow{} (A J f(a)) 13. (\mforall{}I:Cname List. \mforall{}a:X.<A1, A2>(I). \mforall{}u:A I a. ((B1 I I 1 a u) = u)) \mwedge{} (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K). \mforall{}a:X.<A1, A2>(I). \mforall{}u:A I a. ((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u)))) 14. w : J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} u:<A1, A2>(f((s)a)) {}\mrightarrow{} <A, B1>((f((s)a);u)) 15. \mforall{}J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K). \mforall{}u:<A1, A2>(f((s)a)). ((w J f u (f((s)a);u) g) = (w K (f o g) (u f((s)a) g))) 16. H : Cname List 17. K : Cname List 18. h : name-morph(J;H) 19. g : name-morph(H;K) 20. u : <A1, A2>(h((s)f(a))) 21. X \mvdash{} <A1, A2> \mwedge{} X.<A1, A2> \mvdash{} <A, B1> \mvdash{} (B1 H K g ((s)h(f(a));u) (w H (f o h) u)) = (w K (f o (h o g)) (A2 H K g (s)h(f(a)) u)) By Latex: xxx((InstHyp [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}(f o h)\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}] (-7)\mcdot{} THENA Auto) THEN RepUR ``cubical-type-ap-morph`` -1 THEN NthHypEq (-1) THEN EqCD)xxx Home Index