---

Step * 1 of Lemma cc-fst-comp-csm-m-term


1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
⊢ ((phi)p)m = ((phi)p)p ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
BY
{ (BLemma `cubical-term-equal2` THEN Auto) }

1
.....wf..... 
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
⊢ ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}

2
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. I : fset(ℕ)
4. a : H.𝕀.𝕀(I)
⊢ (((phi)p)m I a) = (((phi)p)p I a) ∈ 𝔽(a)

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  ((phi)p)m  =  ((phi)p)p


By

---

Latex:
(BLemma  `cubical-term-equal2`  THEN  Auto)

---

Home Index