---

Step * 3 of Lemma psc-snd_wf

.....wf..... 
1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. A : {Gamma ⊢ _}
4. u : I:cat-ob(C) ⟶ a:Gamma.A(I) ⟶ (A)p(a)
⊢ istype(∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:Gamma.A(I).  ((u I a a f) = (u J f(a)) ∈ (A)p(f(a))))
BY
{ (RepeatFor 2 (DVar `A')
   THEN RepUR ``pscm-ap-type psc-fst pscm-ap`` 0
   THEN All (RepUR ``psc-adjoin I_set functor-ob presheaf-type-at presheaf-type-ap-morph``)
   THEN (Assert Gamma ∈ ps_context{j:l}(C) BY
               Auto)
   THEN RepeatFor 2 (D 2)
   THEN All Reduce) }

1
1. C : SmallCategory
2. F : cat-ob(op-cat(C)) ⟶ cat-ob(type-cat{j':l})
3. G1 : x:cat-ob(op-cat(C))
⟶ y:cat-ob(op-cat(C))
⟶ (cat-arrow(op-cat(C)) x y)
⟶ (cat-arrow(type-cat{j':l}) (F x) (F y))
4. (∀x:cat-ob(op-cat(C))
      ((G1 x x (cat-id(op-cat(C)) x)) = (cat-id(type-cat{j':l}) (F x)) ∈ (cat-arrow(type-cat{j':l}) (F x) (F x))))
∧ (∀x,y,z:cat-ob(op-cat(C)). ∀f:cat-arrow(op-cat(C)) x y. ∀g:cat-arrow(op-cat(C)) y z.
     ((G1 x z (cat-comp(op-cat(C)) x y z f g))
     = (cat-comp(type-cat{j':l}) (F x) (F y) (F z) (G1 x y f) (G1 y z g))
     ∈ (cat-arrow(type-cat{j':l}) (F x) (F z))))
5. A1 : I:cat-ob(C) ⟶ (F I) ⟶ Type
6. A2 : I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ a:(F I) ⟶ (A1 I a) ⟶ (A1 J (G1 I J f a))
7. (∀I:cat-ob(C). ∀a:F I. ∀u:A1 I a.  ((A2 I I (cat-id(C) I) a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:F I. ∀u:A1 I a.
     ((A2 I K (cat-comp(C) K J I g f) a u)
     = (A2 J K g (G1 I J f a) (A2 I J f a u))
     ∈ (A1 K (G1 I K (cat-comp(C) K J I g f) a))))
8. u : I:cat-ob(C) ⟶ a:(alpha:F I × (A1 I alpha)) ⟶ ((fst((<A1, A2>)p)) I a)
9. <F, G1> ∈ ps_context{j:l}(C)
⊢ istype(∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:alpha:F I × (A1 I alpha).
           ((A2 I J f (fst(a)) (u I a))
           = (u J <G1 I J f (fst(a)), A2 I J f (fst(a)) (snd(a))>)
           ∈ (A1 J (G1 I J f (fst(a))))))

---

Latex:

---

Latex:
.....wf..... 
1.  C  :  SmallCategory
2.  Gamma  :  ps\_context\{j:l\}(C)
3.  A  :  \{Gamma  \mvdash{}  \_\}
4.  u  :  I:cat-ob(C)  {}\mrightarrow{}  a:Gamma.A(I)  {}\mrightarrow{}  (A)p(a)
\mvdash{}  istype(\mforall{}I,J:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:Gamma.A(I).    ((u  I  a  a  f)  =  (u  J  f(a))))


By

---

Latex:
(RepeatFor  2  (DVar  `A')
  THEN  RepUR  ``pscm-ap-type  psc-fst  pscm-ap``  0
  THEN  All  (RepUR  ``psc-adjoin  I\_set  functor-ob  presheaf-type-at  presheaf-type-ap-morph``)
  THEN  (Assert  Gamma  \mmember{}  ps\_context\{j:l\}(C)  BY
                          Auto)
  THEN  RepeatFor  2  (D  2)
  THEN  All  Reduce)

---

Home Index