---

Step * of Lemma csm-ap-cubical-snd

∀[X,Delta:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}]. ∀[s:Delta ⟶ X].
  ((p.2)s = (p)s.2 ∈ {Delta ⊢ _:((B)[p.1])s})
BY
{ TACTIC:(Auto THEN BLemma `cubical-term-equal` THEN Auto) }

1
.....wf..... 
1. X : CubicalSet
2. Delta : CubicalSet
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. p : {X ⊢ _:Σ A B}
6. s : Delta ⟶ X
⊢ (p)s.2 ∈ I:(Cname List) ⟶ a:Delta(I) ⟶ ((fst(((B)[p.1])s)) I a)

---

Latex:

---

Latex:
\mforall{}[X,Delta:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[p:\{X  \mvdash{}  \_:\mSigma{}  A  B\}].  \mforall{}[s:Delta  {}\mrightarrow{}  X].
    ((p.2)s  =  (p)s.2)


By

---

Latex:
TACTIC:(Auto  THEN  BLemma  `cubical-term-equal`  THEN  Auto)

---

Home Index