---

Step * of Lemma rep-sub-sheaf_wf

∀[C:SmallCategory]. ∀[X:cat-ob(C)]. ∀[P:U:cat-ob(C) ⟶ (cat-arrow(C) U X) ⟶ ℙ].
  rep-sub-sheaf(C;X;P) ∈ Functor(op-cat(C);TypeCat) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B. ∀b:{b:cat-arrow(C) B X| P B b} .  (P A (cat-comp(C) A B X g b))
BY
{ (Auto
   THEN Unfold `rep-sub-sheaf` 0
   THEN MemTypeCD
   THEN Reduce 0
   THEN ((D 1
          THEN RepeatFor 3 (D (-5))
          THEN All (RepUR  ``cat-ob op-cat cat-arrow cat-comp cat-id type-cat compose``)⋅
          THEN All Reduce
          THEN Auto)
   ORELSE (D -1 THEN Reduce 0 THEN Auto)
   )) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:cat-ob(C)].  \mforall{}[P:U:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  U  X)  {}\mrightarrow{}  \mBbbP{}].
    rep-sub-sheaf(C;X;P)  \mmember{}  Functor(op-cat(C);TypeCat) 
    supposing  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  A  B.  \mforall{}b:\{b:cat-arrow(C)  B  X|  P  B  b\}  .
                            (P  A  (cat-comp(C)  A  B  X  g  b))


By

---

Latex:
(Auto
  THEN  Unfold  `rep-sub-sheaf`  0
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  ((D  1
                THEN  RepeatFor  3  (D  (-5))
                THEN  All  (RepUR    ``cat-ob  op-cat  cat-arrow  cat-comp  cat-id  type-cat  compose``)\mcdot{}
                THEN  All  Reduce
                THEN  Auto)
  ORELSE  (D  -1  THEN  Reduce  0  THEN  Auto)
  ))

---

Home Index