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

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

1. X : CubicalSet
2. Delta : CubicalSet
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. s : Delta ⟶ X
6. I : Cname List
7. a : Delta(I)
⊢ cubical-pi-family(X;A;B;I;(s)a) = cubical-pi-family(Delta;(A)s;(B)(s o p;q);I;a) ∈ Type
BY
{ TACTIC:(RepeatFor 2 (DVar `X')
          THEN RepeatFor 2 (DVar `Delta')
          THEN RepeatFor 2 (DVar `A')
          THEN RepeatFor 2 (DVar `B')
          THEN DVar `s'⋅
          THEN All (RepUR ``cat-ob cat-arrow cat-comp type-cat I-cube
                            cube-context-adjoin cubical-pi-family csm-ap
                           csm-comp trans-comp csm-adjoin cc-adjoin-cube
                           cc-fst cc-snd
                            cubical-type-at csm-ap-type cubical-type-ap-morph
                            name-cat functor-ob functor-arrow compose``)⋅
          THEN All Reduce
          THEN Repeat ((EqCD
                        THEN Try (Trivial)
                        THEN Try (Try ((Fold `member` 0 THEN Auto)))
                        THEN Try (Complete (RepeatFor 5 (MemCD)))))
          THEN Try ((Assert f(s I a) = (s J f(a)) ∈ (X1 J) BY
                           ((RepUR ``cube-set-restriction`` 0 THEN Auto)

                            THEN OnMaybeHyp 14 (\h. ((InstHyp [⌜I⌝;⌜J⌝;⌜f⌝] h⋅ THENA Auto)

                                                     THEN ApFunToHypEquands `Z' ⌜Z a⌝ ⌜X1 J⌝ (-1)⋅

                                                     THEN Reduce (-1)

                                                     THEN Complete (Auto)))

                            )))
          THEN Try (Trivial)) }

1
1. X1 : L:(Cname List) ⟶ Type
2. X2 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
      ((X2 I K (f o g)) = (λx.(X2 J K g (X2 I J f x))) ∈ ((X1 I) ⟶ (X1 K))))
∧ (∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I))))
4. X : L:(Cname List) ⟶ Type
5. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
6. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
      ((D1 I K (f o g)) = (λx.(D1 J K g (D1 I J f x))) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
7. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type

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

9. (∀I:Cname List. ∀a:X1 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:X1 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))))
10. A : I:(Cname List) ⟶ (alpha:X1 I × (A1 I alpha)) ⟶ Type

11. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(alpha:X1 I × (A1 I alpha)) ⟶ (A I a) ⟶ (A J f(a))

12. (∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀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:alpha:X1 I × (A1 I alpha). ∀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))))
13. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)

14. ∀A,B:Cname List. ∀g:name-morph(A;B).  ((λx.(X2 A B g (s A x))) = (λx.(s B (D1 A B g x))) ∈ ((X A) ⟶ (X1 B)))

15. I : Cname List
16. a : X I
17. J : Cname List
18. f : name-morph(I;J)
19. u : A1 J f(s I a)
20. alpha : X1 J
21. f(s I a) = (s J f(a)) ∈ (X1 J)
⊢ istype(A1 J alpha)

2
1. X1 : L:(Cname List) ⟶ Type
2. X2 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((X2 I K (f o g)) = (λx.(X2 J K g (X2 I J f x))) ∈ ((X1 I) ⟶ (X1 K))))
∧ (∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I))))
4. X : L:(Cname List) ⟶ Type
5. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
6. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((D1 I K (f o g)) = (λx.(D1 J K g (D1 I J f x))) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
7. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type

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

11. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(alpha:X1 I × (A1 I alpha)) ⟶ (A I a) ⟶ (A J f(a))

12. (∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀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:alpha:X1 I × (A1 I alpha). ∀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))))
13. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)

14. ∀A,B:Cname List. ∀g:name-morph(A;B).  ((λx.(X2 A B g (s A x))) = (λx.(s B (D1 A B g x))) ∈ ((X A) ⟶ (X1 B)))

15. I : Cname List
16. a : X I
17. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:(A1 J f(s I a)) ⟶ (A J <f(s I a), u>)
18. J : Cname List
19. K : Cname List
20. f : name-morph(I;J)
21. g : name-morph(J;K)
22. u : A1 J f(s I a)
23. f(s I a) = (s J f(a)) ∈ (X1 J)
⊢ g(<f(s I a), u>) = <s K (fst(g(<f(a), u>))), snd(g(<f(a), u>))> ∈ (alpha:X1 K × (A1 K alpha))

3
1. X1 : L:(Cname List) ⟶ Type
2. X2 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((X2 I K (f o g)) = (λx.(X2 J K g (X2 I J f x))) ∈ ((X1 I) ⟶ (X1 K))))
∧ (∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I))))
4. X : L:(Cname List) ⟶ Type
5. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
6. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((D1 I K (f o g)) = (λx.(D1 J K g (D1 I J f x))) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
7. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type

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

11. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(alpha:X1 I × (A1 I alpha)) ⟶ (A I a) ⟶ (A J f(a))

12. (∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀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:alpha:X1 I × (A1 I alpha). ∀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))))
13. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)

14. ∀A,B:Cname List. ∀g:name-morph(A;B).  ((λx.(X2 A B g (s A x))) = (λx.(s B (D1 A B g x))) ∈ ((X A) ⟶ (X1 B)))

15. I : Cname List
16. a : X I
17. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:(A1 J f(s I a)) ⟶ (A J <f(s I a), u>)
18. J : Cname List
19. K : Cname List
20. f : name-morph(I;J)
21. g : name-morph(J;K)
22. u : A1 J f(s I a)
23. alpha : X1 J
24. f(s I a) = (s J f(a)) ∈ (X1 J)
⊢ istype(A1 J alpha)

4
1. X1 : L:(Cname List) ⟶ Type
2. X2 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((X2 I K (f o g)) = (λx.(X2 J K g (X2 I J f x))) ∈ ((X1 I) ⟶ (X1 K))))
∧ (∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I))))
4. X : L:(Cname List) ⟶ Type
5. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
6. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((D1 I K (f o g)) = (λx.(D1 J K g (D1 I J f x))) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
7. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type

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

11. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(alpha:X1 I × (A1 I alpha)) ⟶ (A I a) ⟶ (A J f(a))

12. (∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀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:alpha:X1 I × (A1 I alpha). ∀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))))
13. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)

14. ∀A,B:Cname List. ∀g:name-morph(A;B).  ((λx.(X2 A B g (s A x))) = (λx.(s B (D1 A B g x))) ∈ ((X A) ⟶ (X1 B)))

⊢ (w K (f o g) (A2 J K g f(s I a) u)) = (w K (f o g) (A2 J K g (s J f(a)) u)) ∈ (A K g(<f(s I a), u>))

Latex:

Latex:
1. X : CubicalSet 2. Delta : CubicalSet 3. A : \{X \mvdash{} \_\} 4. B : \{X.A \mvdash{} \_\} 5. s : Delta {}\mrightarrow{} X 6. I : Cname List 7. a : Delta(I) \mvdash{} cubical-pi-family(X;A;B;I;(s)a) = cubical-pi-family(Delta;(A)s;(B)(s o p;q);I;a) By Latex: TACTIC:(RepeatFor 2 (DVar `X') THEN RepeatFor 2 (DVar `Delta') THEN RepeatFor 2 (DVar `A') THEN RepeatFor 2 (DVar `B') THEN DVar `s'\mcdot{} THEN All (RepUR ``cat-ob cat-arrow cat-comp type-cat I-cube cube-context-adjoin cubical-pi-family csm-ap csm-comp trans-comp csm-adjoin cc-adjoin-cube cc-fst cc-snd cubical-type-at csm-ap-type cubical-type-ap-morph name-cat functor-ob functor-arrow compose``)\mcdot{} THEN All Reduce THEN Repeat ((EqCD THEN Try (Trivial) THEN Try (Try ((Fold `member` 0 THEN Auto))) THEN Try (Complete (RepeatFor 5 (MemCD))))) THEN Try ((Assert f(s I a) = (s J f(a)) BY ((RepUR ``cube-set-restriction`` 0 THEN Auto) THEN OnMaybeHyp 14 (\mbackslash{}h. ((InstHyp [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}] h\mcdot{} THENA Auto) THEN ApFunToHypEquands `Z' \mkleeneopen{}Z a\mkleeneclose{} \mkleeneopen{}X1 J\mkleeneclose{} (-1)\mcdot{} THEN Reduce (-1) THEN Complete (Auto))) ))) THEN Try (Trivial)) Home Index