---

Step * of Lemma csm-face-forall

No Annotations
∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[phi:{Gamma.𝕀 ⊢ _:𝔽}].
  (((∀ phi))sigma = (Delta ⊢ ∀ (phi)sigma+) ∈ {Delta ⊢ _:𝔽})
BY
{ ((Intros THEN Unhide)
   THEN (Assert ⌜((∀ phi))sigma = (Delta ⊢ ∀ (phi)sigma+) ∈ (I:fset(ℕ) ⟶ a:Delta(I) ⟶ 𝔽(a))⌝⋅
        THENM (BLemma `cubical-term-equal` THEN Auto)
        )
   ) }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. phi : {Gamma.𝕀 ⊢ _:𝔽}
⊢ ((∀ phi))sigma = (Delta ⊢ ∀ (phi)sigma+) ∈ (I:fset(ℕ) ⟶ a:Delta(I) ⟶ 𝔽(a))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[sigma:Delta  j{}\mrightarrow{}  Gamma].  \mforall{}[phi:\{Gamma.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].
    (((\mforall{}  phi))sigma  =  (Delta  \mvdash{}  \mforall{}  (phi)sigma+))


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  (Assert  \mkleeneopen{}((\mforall{}  phi))sigma  =  (Delta  \mvdash{}  \mforall{}  (phi)sigma+)\mkleeneclose{}\mcdot{}
            THENM  (BLemma  `cubical-term-equal`  THEN  Auto)
            )
  )

---

Home Index