---

Step * of Lemma csm-cubical-pi

∀X,Delta:CubicalSet. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ⟶ X.  ((ΠA B)s = Delta ⊢ Π(A)s (B)(s o p;q) ∈ {Delta ⊢ _})
BY
{ (Auto
   THEN (Assert ⌜(ΠA B)s
                 = Delta ⊢ Π(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
= Delta ⊢ Π(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.
    ((\mPi{}A  B)s  =  Delta  \mvdash{}  \mPi{}(A)s  (B)(s  o  p;q))


By

---

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

---

Home Index