---

Step * 1 of Lemma psc-map-subtype


1. C : SmallCategory
2. A : ps_context{j:l}(C)
3. B : ps_context{j:l}(C)
4. x : A@0:cat-ob(op-cat(C)) ⟶ (cat-arrow(type-cat{j':l}) (A A@0) (B A@0))
⊢ x ∈ I:cat-ob(C) ⟶ A(I) ⟶ B(I)
BY
{ (DCat 1 THEN (Fold `I_set` (-1) THEN RepUR ``cat-arrow type-cat cat-ob op-cat`` -1) THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  A  :  ps\_context\{j:l\}(C)
3.  B  :  ps\_context\{j:l\}(C)
4.  x  :  A@0:cat-ob(op-cat(C))  {}\mrightarrow{}  (cat-arrow(type-cat\{j':l\})  (A  A@0)  (B  A@0))
\mvdash{}  x  \mmember{}  I:cat-ob(C)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)


By

---

Latex:
(DCat  1  THEN  (Fold  `I\_set`  (-1)  THEN  RepUR  ``cat-arrow  type-cat  cat-ob  op-cat``  -1)  THEN  Auto)

---

Home Index