---

Step * of Lemma ps-subset-restriction

No Annotations
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].
  ∀[I,J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[a:Y(I)].  (f(a) = f(a) ∈ X(J)) supposing sub_ps_context{j:l}(C; Y; X)
BY
{ (Intros
   THEN Unfold `sub_ps_context` 4
   THEN (MemTypeHD 4 THENA Auto)
   THEN (Assert C ∈ SmallCategory BY
               Auto)
   THEN DCat 1
   THEN All (RepUR ``cat-ob cat-comp op-cat cat-arrow type-cat functor-arrow``)
   THEN All (RepUR ``compose pscm-id``)
   THEN Fold `psc-restriction` (-6)
   THEN Fold `I_set` (-7)
   THEN Fold `I_set` (-6)) }

1
1. Cob : Type
2. Carrow : Cob ⟶ Cob ⟶ Type
3. Cid : x:Cob ⟶ (Carrow x x)
4. Ccomp : x:Cob ⟶ y:Cob ⟶ z:Cob ⟶ (Carrow x y) ⟶ (Carrow y z) ⟶ (Carrow x z)
5. ∀x,y:Cob. ∀f:Carrow x y.
     (((Ccomp x x y (Cid x) f) = f ∈ (Carrow x y)) ∧ ((Ccomp x y y f (Cid y)) = f ∈ (Carrow x y)))
6. ∀x,y,z,w:Cob. ∀f:Carrow x y. ∀g:Carrow y z. ∀h:Carrow z w.
     ((Ccomp x z w (Ccomp x y z f g) h) = (Ccomp x y w f (Ccomp y z w g h)) ∈ (Carrow x w))
7. X : ps_context{j:l}(<Cob, Carrow, Cid, Ccomp>)
8. Y : ps_context{j:l}(<Cob, Carrow, Cid, Ccomp>)
9. λA,x. x ∈ A:Cob ⟶ Y(A) ⟶ X(A)
10. ∀A,B:Cob. ∀g:Carrow B A.  ((λx.g(x)) = (λx.g(x)) ∈ (Y(A) ⟶ X(B)))
11. I : Cob
12. J : Cob
13. f : Carrow J I
14. a : Y(I)
15. <Cob, Carrow, Cid, Ccomp> ∈ SmallCategory
⊢ f(a) = f(a) ∈ X(J)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X,Y:ps\_context\{j:l\}(C)].
    \mforall{}[I,J:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  J  I].  \mforall{}[a:Y(I)].    (f(a)  =  f(a)) 
    supposing  sub\_ps\_context\{j:l\}(C;  Y;  X)


By

---

Latex:
(Intros
  THEN  Unfold  `sub\_ps\_context`  4
  THEN  (MemTypeHD  4  THENA  Auto)
  THEN  (Assert  C  \mmember{}  SmallCategory  BY
                          Auto)
  THEN  DCat  1
  THEN  All  (RepUR  ``cat-ob  cat-comp  op-cat  cat-arrow  type-cat  functor-arrow``)
  THEN  All  (RepUR  ``compose  pscm-id``)
  THEN  Fold  `psc-restriction`  (-6)
  THEN  Fold  `I\_set`  (-7)
  THEN  Fold  `I\_set`  (-6))

---

Home Index