---

Step * of Lemma cc-snd_wf

∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}].  (q ∈ {Gamma.A ⊢ _:(A)p})
BY
{ TACTIC:(Auto THEN MemTypeCD) }

1
1. Gamma : CubicalSet
2. A : {Gamma ⊢ _}
⊢ q ∈ I:(Cname List) ⟶ a:Gamma.A(I) ⟶ ((fst((A)p)) I a)

2
.....set predicate..... 
1. Gamma : CubicalSet
2. A : {Gamma ⊢ _}
⊢ ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Gamma.A(I).
    let A@0,F = (A)p 
    in (F I J f a (q I a)) = (q J f(a)) ∈ (A@0 J f(a))

3
.....wf..... 
1. Gamma : CubicalSet
2. A : {Gamma ⊢ _}
3. u : I:(Cname List) ⟶ a:Gamma.A(I) ⟶ ((fst((A)p)) I a)
⊢ istype(∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Gamma.A(I).
           let A@0,F = (A)p 
           in (F I J f a (u I a)) = (u J f(a)) ∈ (A@0 J f(a)))

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto  THEN  MemTypeCD)

---

Home Index