---

Step * 1 of Lemma pscm-presheaf-sigma


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {X ⊢ _}
5. B : {X.A ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
⊢ (Σ A B)s
= Σ (A)s (B)(s o p;q)
∈ (A:I:cat-ob(C) ⟶ Delta(I) ⟶ Type × (I:cat-ob(C)
                                       ⟶ J:cat-ob(C)
                                       ⟶ f:(cat-arrow(C) J I)
                                       ⟶ a:Delta(I)
                                       ⟶ (A I a)
                                       ⟶ (A J f(a))))
BY
{ ((Assert A ∈ X ⊢  BY
          Auto)
   THEN (Assert B ∈ X.A ⊢  BY
               Auto)
   THEN RepeatFor 2 (DVar `A')
   THEN RepeatFor 2 (DVar `B')
   THEN (Assert s ∈ Delta ⟶ X BY
               Auto)
   THEN DVar `s'⋅
   THEN All Reduce
   THEN RepUR ``presheaf-sigma pscm-ap-type presheaf-type-at`` 0
   THEN MemCD
   THEN (RepeatFor 2 ((EqCD THENA Auto)) ORELSE Auto)
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  Delta  :  ps\_context\{j:l\}(C)
4.  A  :  \{X  \mvdash{}  \_\}
5.  B  :  \{X.A  \mvdash{}  \_\}
6.  s  :  psc\_map\{j:l\}(C;  Delta;  X)
\mvdash{}  (\mSigma{}  A  B)s  =  \mSigma{}  (A)s  (B)(s  o  p;q)


By

---

Latex:
((Assert  A  \mmember{}  X  \mvdash{}    BY
                Auto)
  THEN  (Assert  B  \mmember{}  X.A  \mvdash{}    BY
                          Auto)
  THEN  RepeatFor  2  (DVar  `A')
  THEN  RepeatFor  2  (DVar  `B')
  THEN  (Assert  s  \mmember{}  Delta  {}\mrightarrow{}  X  BY
                          Auto)
  THEN  DVar  `s'\mcdot{}
  THEN  All  Reduce
  THEN  RepUR  ``presheaf-sigma  pscm-ap-type  presheaf-type-at``  0
  THEN  MemCD
  THEN  (RepeatFor  2  ((EqCD  THENA  Auto))  ORELSE  Auto)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index