---

Step * of Lemma psc-map-subtype

No Annotations
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)].  (psc_map{j:l}(C; A; B) ⊆r (I:cat-ob(C) ⟶ A(I) ⟶ B(I)))
BY
{ (Intros THEN (D 0 THENA Auto) THEN D -1 THEN Thin (-1)) }

1
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[A,B:ps\_context\{j:l\}(C)].
    (psc\_map\{j:l\}(C;  A;  B)  \msubseteq{}r  (I:cat-ob(C)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)))


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  Thin  (-1))

---

Home Index