---

Step * 1 1 2 1 2 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
14. omega : A1 [z / I] (s)iota(z)(alpha)
⊢ (omega (s)iota(z)(alpha) (z:=1)) = (omega iota(z)((s)alpha) (z:=1)) ∈ <A1, A2>((s)alpha)
BY
{ Assert ⌜(z:=1)(iota(z)((s)alpha)) = (s)alpha ∈ X(I)⌝⋅ }

1
.....assertion..... 
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)
⊢ (z:=1)(iota(z)((s)alpha)) = (s)alpha ∈ X(I)

2
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)
15. (z:=1)(iota(z)((s)alpha)) = (s)alpha ∈ X(I)
⊢ (omega (s)iota(z)(alpha) (z:=1)) = (omega iota(z)((s)alpha) (z:=1)) ∈ <A1, A2>((s)alpha)

---

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
14.  omega  :  A1  [z  /  I]  (s)iota(z)(alpha)
\mvdash{}  (omega  (s)iota(z)(alpha)  (z:=1))  =  (omega  iota(z)((s)alpha)  (z:=1))


By

---

Latex:
Assert  \mkleeneopen{}(z:=1)(iota(z)((s)alpha))  =  (s)alpha\mkleeneclose{}\mcdot{}

---

Home Index