---

Step * 3 of Lemma cc-snd_wf

.....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)))
BY
{ TACTIC:(RepeatFor 2 (DVar `A')
          THEN RepUR ``csm-ap-type cc-fst csm-ap`` 0
          THEN TACTIC:(All (RepUR ``cube-context-adjoin I-cube functor-ob cubical-type-at cubical-type-ap-morph``)
                       THEN (Assert Gamma ∈ CubicalSet BY
                                   Auto)
                       THEN RepeatFor 2 (D 1)
                       THEN All Reduce)) }

1
1. X : L:(Cname List) ⟶ Type
2. G1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
      ((G1 I K (f o g)) = ((G1 J K g) o (G1 I J f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((G1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
4. A1 : I:(Cname List) ⟶ (X I) ⟶ Type
5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(X I) ⟶ (A1 I a) ⟶ (A1 J f(a))
6. (∀I:Cname List. ∀a:X I. ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X I. ∀u:A1 I a.
     ((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a))))
7. u : I:(Cname List) ⟶ a:(alpha:X I × (A1 I alpha)) ⟶ ((fst((<A1, A2>)p)) I a)
8. <X, G1> ∈ CubicalSet
⊢ istype(∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:alpha:X I × (A1 I alpha).
           ((A2 I J f (fst(a)) (u I a)) = (u J f(a)) ∈ (A1 J (fst(f(a))))))

---

Latex:

---

Latex:
.....wf..... 
1.  Gamma  :  CubicalSet
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  u  :  I:(Cname  List)  {}\mrightarrow{}  a:Gamma.A(I)  {}\mrightarrow{}  ((fst((A)p))  I  a)
\mvdash{}  istype(\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  (u  I  a))  =  (u  J  f(a)))


By

---

Latex:
TACTIC:(RepeatFor  2  (DVar  `A')
                THEN  RepUR  ``csm-ap-type  cc-fst  csm-ap``  0
                THEN  TACTIC:(...
                                          THEN  (Assert  Gamma  \mmember{}  CubicalSet  BY
                                                                  Auto)
                                          THEN  RepeatFor  2  (D  1)
                                          THEN  All  Reduce))

---

Home Index