---

Step * of Lemma csm-cubical-sigma

∀X,Delta:CubicalSet. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ⟶ X.  ((Σ A B)s = Σ (A)s (B)(s o p;q) ∈ {Delta ⊢ _})
BY
{ (Auto
   THEN (Assert ⌜(Σ A B)s
                 = Σ (A)s (B)(s o p;q)
                 ∈ (A:I:(Cname List) ⟶ Delta(I) ⟶ Type × (I:(Cname List)
                                                           ⟶ J:(Cname List)
                                                           ⟶ f:name-morph(I;J)
                                                           ⟶ a:Delta(I)
                                                           ⟶ (A I a)
                                                           ⟶ (A J f(a))))⌝⋅
        THENM (BLemma `cubical-type-equal` THEN Try (Complete (Auto)))
        )
   ) }

1
.....assertion..... 
1. X : CubicalSet
2. Delta : CubicalSet
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. s : Delta ⟶ X
⊢ (Σ A B)s
= Σ (A)s (B)(s o p;q)
∈ (A:I:(Cname List) ⟶ Delta(I) ⟶ Type × (I:(Cname List)
                                          ⟶ J:(Cname List)
                                          ⟶ f:name-morph(I;J)
                                          ⟶ a:Delta(I)
                                          ⟶ (A I a)
                                          ⟶ (A J f(a))))

---

Latex:

---

Latex:
\mforall{}X,Delta:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}s:Delta  {}\mrightarrow{}  X.    ((\mSigma{}  A  B)s  =  \mSigma{}  (A)s  (B)(s  o  p;q))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}(\mSigma{}  A  B)s  =  \mSigma{}  (A)s  (B)(s  o  p;q)\mkleeneclose{}\mcdot{}
            THENM  (BLemma  `cubical-type-equal`  THEN  Try  (Complete  (Auto)))
            )
  )

---

Home Index