---

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


1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : A:cat-ob(op-cat(C)) ⟶ (cat-arrow(type-cat{[i | j]':l}) (X A) (discrete-set(T) A))
5. ∀A,B:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A B.
     ((cat-comp(type-cat{[i | j]':l}) (X A) (discrete-set(T) A) (discrete-set(T) B) (x A) (discrete-set(T) A B g))
     = (cat-comp(type-cat{[i | j]':l}) (X A) (X B) (discrete-set(T) B) (X A B g) (x B))
     ∈ (cat-arrow(type-cat{[i | j]':l}) (X A) (discrete-set(T) B)))
⊢ x ∈ {X ⊢ _:discr(T)}
BY
{ (RepUR ``type-cat discrete-set compose`` -2 THEN RepUR ``type-cat discrete-set compose`` -1) }

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

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  T  :  Type
3.  X  :  ps\_context\{j:l\}(C)
4.  x  :  A:cat-ob(op-cat(C))  {}\mrightarrow{}  (cat-arrow(type-cat\{[i  |  j]':l\})  (X  A)  (discrete-set(T)  A))
5.  \mforall{}A,B:cat-ob(op-cat(C)).  \mforall{}g:cat-arrow(op-cat(C))  A  B.
          ((cat-comp(type-cat\{[i  |  j]':l\})  (X  A)  (discrete-set(T)  A)  (discrete-set(T)  B)  (x  A) 
              (discrete-set(T)  A  B  g))
          =  (cat-comp(type-cat\{[i  |  j]':l\})  (X  A)  (X  B)  (discrete-set(T)  B)  (X  A  B  g)  (x  B)))
\mvdash{}  x  \mmember{}  \{X  \mvdash{}  \_:discr(T)\}


By

---

Latex:
(RepUR  ``type-cat  discrete-set  compose``  -2  THEN  RepUR  ``type-cat  discrete-set  compose``  -1)

---

Home Index