---

Step * 1 of Lemma cc-snd_wf


1. Gamma : CubicalSet
2. A : {Gamma ⊢ _}
⊢ q ∈ I:(Cname List) ⟶ a:Gamma.A(I) ⟶ ((fst((A)p)) I a)
BY
{ TACTIC:((RepeatFor 2 (D 2) THEN RepeatFor 2 (D 1))
          THEN RepUR ``cube-context-adjoin csm-ap-type cubical-type-at I-cube functor-ob csm-ap cc-snd cc-fst`` 0
          THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  A  :  \{Gamma  \mvdash{}  \_\}
\mvdash{}  q  \mmember{}  I:(Cname  List)  {}\mrightarrow{}  a:Gamma.A(I)  {}\mrightarrow{}  ((fst((A)p))  I  a)


By

---

Latex:
TACTIC:((RepeatFor  2  (D  2)  THEN  RepeatFor  2  (D  1))
                THEN  ...
                THEN  Auto)

---

Home Index