---

Step * 1 1 2 1 1 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
14. omega : A1 [z / I] (s)iota(z)(alpha)
15. v : X(I)
16. (s)alpha = v ∈ X(I)
⊢ (iota(z) o (z:=0))(v) = v ∈ X(I)
BY
{ (RestrictionComp THEN (InstLemma `iota-identity` [⌜I⌝;⌜z⌝;⌜0⌝]⋅ THENA 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)
15. v : X(I)
16. (s)alpha = v ∈ X(I)
17. (iota(z) o (z:=0)) = 1 ∈ name-morph(I;I)
⊢ (iota(z) o (z:=0))(v) = v ∈ X(I)

---

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)
15.  v  :  X(I)
16.  (s)alpha  =  v
\mvdash{}  (iota(z)  o  (z:=0))(v)  =  v


By

---

Latex:
(RestrictionComp  THEN  (InstLemma  `iota-identity`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index