---

Step * 2 of Lemma cc-snd_wf

.....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))
BY
{ TACTIC:(Auto
          THEN (RepeatFor 2 (D 2) THEN RepeatFor 2 (D 1))
          THEN All (RepUR ``cube-context-adjoin cubical-type-at csm-ap cc-fst cc-snd 
                            cube-set-restriction I-cube functor-ob``)⋅
          THEN D -1
          THEN All Reduce
          THEN Auto) }

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  (RepeatFor  2  (D  2)  THEN  RepeatFor  2  (D  1))
                THEN  All  (RepUR  ``cube-context-adjoin  cubical-type-at  csm-ap  cc-fst  cc-snd 
                                                    cube-set-restriction  I-cube  functor-ob``)\mcdot{}
                THEN  D  -1
                THEN  All  Reduce
                THEN  Auto)

---

Home Index