Proof of Nuprl Lemma : csm-cubical-sigma

Step * 1 1 of Lemma csm-cubical-sigma

.....subterm..... T:t
2:n
1. X : CubicalSet
2. Delta : CubicalSet
3. A1 : I:(Cname List) ⟶ X(I) ⟶ Type

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

5. ∀I:Cname List. ∀a:X(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a))
6. ∀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)))
7. A : I:(Cname List) ⟶ X.<A1, A2>(I) ⟶ Type

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

9. ∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A I a.  ((B1 I I 1 a u) = u ∈ (A I a))
10. ∀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)))
11. s : A:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (Delta A) (X A))
12. ∀A,B:cat-ob(NameCat). ∀g:cat-arrow(NameCat) A B.
      ((cat-comp(TypeCat) (Delta A) (X A) (X B) (s A) (X A B g))
      = (cat-comp(TypeCat) (Delta A) (Delta B) (X B) (Delta A B g) (s B))
      ∈ (cat-arrow(TypeCat) (Delta A) (X B)))
13. X ⊢ <A1, A2>
14. X.<A1, A2> ⊢ <A, B1>
15. s ∈ Delta ⟶ X
16. I : Cname List
17. a : Delta(I)
18. u : A1 I (s)a
⊢ ((s)a;u) = <(s o p)(a;u), (q)(a;u)> ∈ X.<A1, A2>(I)
BY
{ TACTIC:RepUR ``csm-adjoin csm-ap cc-fst cc-snd csm-comp trans-comp cat-comp type-cat cc-adjoin-cube`` 0 }

1
1. X : CubicalSet
2. Delta : CubicalSet
3. A1 : I:(Cname List) ⟶ X(I) ⟶ Type

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

8. 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:
.....subterm..... T:t 2:n 1. X : CubicalSet 2. Delta : CubicalSet 3. A1 : I:(Cname List) {}\mrightarrow{} X(I) {}\mrightarrow{} Type 4. 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)) 5. \mforall{}I:Cname List. \mforall{}a:X(I). \mforall{}u:A1 I a. ((A2 I I 1 a u) = u) 6. \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))) 7. A : I:(Cname List) {}\mrightarrow{} X.<A1, A2>(I) {}\mrightarrow{} Type 8. 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)) 9. \mforall{}I:Cname List. \mforall{}a:X.<A1, A2>(I). \mforall{}u:A I a. ((B1 I I 1 a u) = u) 10. \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))) 11. s : A:cat-ob(NameCat) {}\mrightarrow{} (cat-arrow(TypeCat) (Delta A) (X A)) 12. \mforall{}A,B:cat-ob(NameCat). \mforall{}g:cat-arrow(NameCat) A B. ((cat-comp(TypeCat) (Delta A) (X A) (X B) (s A) (X A B g)) = (cat-comp(TypeCat) (Delta A) (Delta B) (X B) (Delta A B g) (s B))) 13. X \mvdash{} <A1, A2> 14. X.<A1, A2> \mvdash{} <A, B1> 15. s \mmember{} Delta {}\mrightarrow{} X 16. I : Cname List 17. a : Delta(I) 18. u : A1 I (s)a \mvdash{} ((s)a;u) = <(s o p)(a;u), (q)(a;u)> By Latex: TACTIC:... Home Index