Step
*
1
1
of Lemma
csm-I-path
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
⊢ named-path(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) = named-path(X;<A1, A2>;a;b;I\000C;(s)alpha;z) ∈ Type
BY
{ TACTIC:(RepUR ``named-path cubical-type-at`` 0 THEN EqCD) }
1
.....subterm..... T:t
1: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))))
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
⊢ (A1 [z / I] (s)iota(z)(alpha)) = (A1 [z / I] iota(z)((s)alpha)) ∈ Type
2
.....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))))
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)
⊢ 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
Latex:
Latex:
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
\mvdash{} named-path(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) = named-p\000Cath(X;<A1, A2>a;b;I;(s)alpha;z)
By
Latex:
TACTIC:(RepUR ``named-path cubical-type-at`` 0 THEN EqCD)
Home
Index