Proof of Nuprl Lemma : csm-I-path

Step * 1 1 2 of Lemma csm-I-path

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

5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))@i'

6. let A,F = <A1, A2>
in (∀I:Cname List. ∀a:X(I). ∀u:A I a. ((F 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(I). ∀u:A I a.

           ((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K (f o g)(a))))

⊢ name-path-endpoints(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;(a)s;(b)s;I;alpha;z;omega) = name-path-en\000Cdpoints(X;<A1, A2>;a;b;I;(s)alpha;z;omega) ∈ Type

{ (Enough to prove ((omega (s)iota(z)(alpha) (z:=0)) = (omega iota(z)((s)alpha) (z:=0)) ∈ <A1, A2>((s)alpha))

   ∧ ((omega (s)iota(z)(alpha) (z:=1)) = (omega iota(z)((s)alpha) (z:=1)) ∈ <A1, A2>((s)alpha))
    Because (D -1
             THEN RepUR ``name-path-endpoints`` 0
             THEN RepeatFor 2 (EqCDA)
             THEN (InstLemma `csm-cubical-type-ap-morph` [⌜X⌝;⌜<A1, A2>⌝] ⋅ THENA Auto)
             THEN RepUR ``csm-ap-type`` -1
             THEN Try ((RWO "-1" 0 THENA Auto))

             THEN (Subst' <λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>(alpha) ~ <A1, A2>((s)alpha) 0 THENA (RepUR \000C``cubical-type-at`` 0 THEN Auto))

THEN Auto)) }

1
1. X : CubicalSet@i'
2. Delta : CubicalSet@i'
3. s : Delta ⟶ X@i'
4. A1 : I:(Cname List) ⟶ X(I) ⟶ Type@i'

5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))@i'

6. let A,F = <A1, A2>
in (∀I:Cname List. ∀a:X(I). ∀u:A I a. ((F 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(I). ∀u:A I a.

           ((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K (f o g)(a))))

7. a : {X ⊢ _:<A1, A2>}@i
8. b : {X ⊢ _:<A1, A2>}@i
9. I : Cname List@i
10. alpha : Delta(I)@i
11. z : {z:Cname| ¬(z ∈ I)}
12. X ⊢ <A1, A2>
13. Delta ⊢ (<A1, A2>)s
14. omega : A1 [z / I] (s)iota(z)(alpha)
⊢ ((omega (s)iota(z)(alpha) (z:=0)) = (omega iota(z)((s)alpha) (z:=0)) ∈ <A1, A2>((s)alpha))
∧ ((omega (s)iota(z)(alpha) (z:=1)) = (omega iota(z)((s)alpha) (z:=1)) ∈ <A1, A2>((s)alpha))

Latex:

Latex:
.....subterm..... T:t 2:n 1. X : CubicalSet@i' 2. Delta : CubicalSet@i' 3. s : Delta {}\mrightarrow{} X@i' 4. A1 : I:(Cname List) {}\mrightarrow{} X(I) {}\mrightarrow{} Type@i' 5. 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))@i' 6. let A,F = <A1, A2> in (\mforall{}I:Cname List. \mforall{}a:X(I). \mforall{}u:A I a. ((F 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:A I a. ((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)))) 7. a : \{X \mvdash{} \_:<A1, A2>\}@i 8. b : \{X \mvdash{} \_:<A1, A2>\}@i 9. I : Cname List@i 10. alpha : Delta(I)@i 11. z : \{z:Cname| \mneg{}(z \mmember{} I)\} 12. X \mvdash{} <A1, A2> 13. Delta \mvdash{} (<A1, A2>)s 14. omega : A1 [z / I] (s)iota(z)(alpha) \mvdash{} name-path-endpoints(Delta;<\mlambda{}I,a. (A1 I (s)a), \mlambda{}I,J,f,a,u. (A2 I J f (s)a u)>(a)s;(b)s;I;alpha;z;o\000Cmega) = name-path-endpoints(X;<A1, A2>a;b;I;(s)alpha;z;omega) By Latex: (Enough to prove ((omega (s)iota(z)(alpha) (z:=0)) = (omega iota(z)((s)alpha) (z:=0))) \mwedge{} ((omega (s)iota(z)(alpha) (z:=1)) = (omega iota(z)((s)alpha) (z:=1))) Because (D -1 THEN RepUR ``name-path-endpoints`` 0 THEN RepeatFor 2 (EqCDA) THEN (InstLemma `csm-cubical-type-ap-morph` [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}<A1, A2>\mkleeneclose{}] \mcdot{} THENA Auto) THEN RepUR ``csm-ap-type`` -1 THEN Try ((RWO "-1" 0 THENA Auto)) THEN (Subst' <\mlambda{}I,a. (A1 I (s)a), \mlambda{}I,J,f,a,u. (A2 I J f (s)a u)>(alpha) \msim{} <A1, A2>((s)alph\000Ca) 0 THENA (RepUR ``cubical-type-at`` 0 THEN Auto)) THEN Auto)) Home Index