---

Step * of Lemma cube-context-adjoin_wf

∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}].  (Gamma.A ∈ CubicalSet)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. Gamma : CubicalSet
2. A : {Gamma ⊢ _}
3. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
     ((λp.<(f o g)(fst(p)), (snd(p) fst(p) (f o g))>)
     = ((λp.<g(fst(p)), (snd(p) fst(p) g)>) o (λp.<f(fst(p)), (snd(p) fst(p) f)>))
     ∈ ((alpha:Gamma(I) × A(alpha)) ⟶ (alpha:Gamma(K) × A(alpha))))
4. I : Cname List
⊢ (λp.<1(fst(p)), (snd(p) fst(p) 1)>) = (λx.x) ∈ ((alpha:Gamma(I) × A(alpha)) ⟶ (alpha:Gamma(I) × A(alpha)))

---

Latex:

---

Latex:
\mforall{}[Gamma:CubicalSet].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].    (Gamma.A  \mmember{}  CubicalSet)


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index