Step * 1 1 of Lemma cc-fst+-0-type


1. CubicalSet{j}
2. {G.𝕀 ⊢ _}
3. [0(𝕀)] ∈ ij⟶ G.𝕀
4. p ∈ G.𝕀 ij⟶ G
⊢ ((A)[0(𝕀)])p ((A)p+)[0(𝕀)] ∈ {G.𝕀 ⊢ _}
BY
(RW (AddrC [2] CsmCompTypeC) THENA Auto) }

1
1. CubicalSet{j}
2. {G.𝕀 ⊢ _}
3. [0(𝕀)] ∈ ij⟶ G.𝕀
4. p ∈ G.𝕀 ij⟶ G
⊢ (A)[0(𝕀)] ((A)p+)[0(𝕀)] ∈ {G.𝕀 ⊢ _}


Latex:


Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G.\mBbbI{}  \mvdash{}  \_\}
3.  [0(\mBbbI{})]  \mmember{}  G  ij{}\mrightarrow{}  G.\mBbbI{}
4.  p  \mmember{}  G.\mBbbI{}  ij{}\mrightarrow{}  G
\mvdash{}  ((A)[0(\mBbbI{})])p  =  ((A)p+)[0(\mBbbI{})]


By


Latex:
(RW  (AddrC  [2]  CsmCompTypeC)  0  THENA  Auto)




Home Index