---

Step * 1 1 of Lemma discrete-presheaf-term-is-map


1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : I:cat-ob(C) ⟶ a:X(I) ⟶ discr(T)(a)
5. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((x I a a f) = (x J f(a)) ∈ discr(T)(f(a)))
⊢ x ∈ psc_map{[i | j]:l}(C; X; discrete-set(T))
BY
{ (All (RepUR ``discrete-presheaf-type``)
   THEN MemTypeCD
   THEN (RWO "cat_ob_op_lemma op-cat-arrow" 0 THENA Auto)
   THEN RepUR ``type-cat discrete-set compose`` 0) }

1
1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : I:cat-ob(C) ⟶ a:X(I) ⟶ T
5. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((x I a) = (x J f(a)) ∈ T)
⊢ x ∈ A:cat-ob(C) ⟶ (X A) ⟶ T

2
1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : I:cat-ob(C) ⟶ a:X(I) ⟶ T
5. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((x I a) = (x J f(a)) ∈ T)
⊢ ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B A.  ((λx@0.(x A x@0)) = (λx@0.(x B (X A B g x@0))) ∈ ((X A) ⟶ T))

3
1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : I:cat-ob(C) ⟶ a:X(I) ⟶ T
5. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((x I a) = (x J f(a)) ∈ T)
6. trans : A:cat-ob(op-cat(C)) ⟶ (cat-arrow(type-cat{[i | j]':l}) (X A) (discrete-set(T) A))
⊢ istype(∀A,B:cat-ob(C). ∀g:cat-arrow(C) B A.  ((λx.(trans A x)) = (λx.(trans B (X A B g x))) ∈ ((X A) ⟶ T)))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  T  :  Type
3.  X  :  ps\_context\{j:l\}(C)
4.  x  :  I:cat-ob(C)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  discr(T)(a)
5.  \mforall{}I,J:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:X(I).    ((x  I  a  a  f)  =  (x  J  f(a)))
\mvdash{}  x  \mmember{}  psc\_map\{[i  |  j]:l\}(C;  X;  discrete-set(T))


By

---

Latex:
(All  (RepUR  ``discrete-presheaf-type``)
  THEN  MemTypeCD
  THEN  (RWO  "cat\_ob\_op\_lemma  op-cat-arrow"  0  THENA  Auto)
  THEN  RepUR  ``type-cat  discrete-set  compose``  0)

---

Home Index