---

Step * of Lemma psc-map-is

No Annotations
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)].
  (psc_map{j:l}(C; A; B) ~ {trans:I:cat-ob(C) ⟶ A(I) ⟶ B(I)| 
                            ∀I,J:cat-ob(C). ∀g:cat-arrow(C) J I.
                              ((λs.g(trans I s)) = (λs.(trans J g(s))) ∈ (A(I) ⟶ B(J)))} )
BY
{ (Auto
   THEN DCat 1
   THEN RepUR ``I_set psc-restriction psc_map op-cat type-cat nat-trans `` 0
   THEN RepUR ``cat-comp functor-arrow cat-ob cat-arrow compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[A,B:ps\_context\{j:l\}(C)].
    (psc\_map\{j:l\}(C;  A;  B)  \msim{}  \{trans:I:cat-ob(C)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)| 
                                                        \mforall{}I,J:cat-ob(C).  \mforall{}g:cat-arrow(C)  J  I.
                                                            ((\mlambda{}s.g(trans  I  s))  =  (\mlambda{}s.(trans  J  g(s))))\}  )


By

---

Latex:
(Auto
  THEN  DCat  1
  THEN  RepUR  ``I\_set  psc-restriction  psc\_map  op-cat  type-cat  nat-trans  ``  0
  THEN  RepUR  ``cat-comp  functor-arrow  cat-ob  cat-arrow  compose``  0
  THEN  Auto)

---

Home Index